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