tjh.dev
1{
2 fetchurl,
3 lib,
4 stdenv,
5 ocaml,
6 isabelle,
7 cvc3,
8 perl,
9 wget,
10 which,
11}:
12
13stdenv.mkDerivation rec {
14 pname = "tlaps";
15 version = "1.4.5";
16 src = fetchurl {
17 url = "https://tla.msr-inria.inria.fr/tlaps/dist/${version}/tlaps-${version}.tar.gz";
18 sha256 = "c296998acd14d5b93a8d5be7ee178007ef179957465966576bda26944b1b7fca";
19 };
20
21 strictDeps = true;
22
23 nativeBuildInputs = [
24 ocaml
25 isabelle
26 cvc3
27 perl
28 wget
29 which
30 ];
31
32 installPhase = ''
33 mkdir -pv "$out"
34 export HOME="$out"
35 export PATH=$out/bin:$PATH
36
37 pushd zenon
38 ./configure --prefix $out
39 make
40 make install
41 popd
42
43 pushd isabelle
44 isabelle build -b Pure
45 popd
46
47 pushd tlapm
48 ./configure --prefix $out
49 make all
50 make install
51 '';
52
53 meta = {
54 description = "Mechanically check TLA+ proofs";
55 longDescription = ''
56 TLA+ is a general-purpose formal specification language that is
57 particularly useful for describing concurrent and distributed
58 systems. The TLA+ proof language is declarative, hierarchical,
59 and scalable to large system specifications. It provides a
60 consistent abstraction over the various “backend” verifiers.
61 '';
62 homepage = "https://tla.msr-inria.inria.fr/tlaps/content/Home.html";
63 license = lib.licenses.bsd2;
64 platforms = lib.platforms.unix;
65 maintainers = with lib.maintainers; [ florentc ];
66 };
67
68}