nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix
2021-01-16 17:58:11 +07:00

55 lines
1.3 KiB
Nix

{ fetchurl
, lib, 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 = lib.licenses.bsd2;
platforms = lib.platforms.unix;
maintainers = [ ];
};
}