blob: 7c8389688d95d602cbb7a97a506753bb30dc3ea3 (
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
|
{ fetchurl
, stdenv
, ocaml, isabelle, cvc3, perl, wget, which
}:
stdenv.mkDerivation rec {
pname = "tlaps";
version = "1.4.3";
src = fetchurl {
url = "https://tla.msr-inria.inria.fr/tlaps/dist/current/tlaps-${version}.tar.gz";
sha256 = "1w5z3ns5xxmhmp8r4x2kjmy3clqam935gmvx82imyxrr1bamx6gf";
};
buildInputs = [ ocaml isabelle cvc3 perl wget which ];
phases = [ "unpackPhase" "installPhase" ];
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 = stdenv.lib.licenses.bsd2;
platforms = stdenv.lib.platforms.unix;
maintainers = [ stdenv.lib.maintainers.badi ];
};
}
|