762faa21a2
This updates tlaps to the most recent stable version and fixes the template for the url from which the sources are fetched. Previously, the tarball was fetched from the "current" remote directory from which old versions are eventually removed. The package was therefore broken. It also adds myself (florentc) as a maintainer.
58 lines
1.3 KiB
Nix
58 lines
1.3 KiB
Nix
{ 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";
|
|
};
|
|
|
|
buildInputs = [ 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 ];
|
|
};
|
|
|
|
}
|