diff options
author | Badi Abdul-Wahid <abdulwahidc@gmail.com> | 2018-04-07 20:27:58 -0400 |
---|---|---|
committer | Badi Abdul-Wahid <abdulwahidc@gmail.com> | 2018-04-16 21:18:42 -0400 |
commit | d14a4760541d59f37ea6397e7616a2e6f9697779 (patch) | |
tree | 892c4e9bcb7791d1877aeec02cf534d6e2341514 /pkgs/applications/science/logic/tlaplus/tlaps.nix | |
parent | d307ab5ca3bff5609db8c942a40961278371bea4 (diff) | |
download | nixpkgs-d14a4760541d59f37ea6397e7616a2e6f9697779.tar nixpkgs-d14a4760541d59f37ea6397e7616a2e6f9697779.tar.gz nixpkgs-d14a4760541d59f37ea6397e7616a2e6f9697779.tar.bz2 nixpkgs-d14a4760541d59f37ea6397e7616a2e6f9697779.tar.lz nixpkgs-d14a4760541d59f37ea6397e7616a2e6f9697779.tar.xz nixpkgs-d14a4760541d59f37ea6397e7616a2e6f9697779.tar.zst nixpkgs-d14a4760541d59f37ea6397e7616a2e6f9697779.zip |
tlaps: init at 1.4.3
Diffstat (limited to 'pkgs/applications/science/logic/tlaplus/tlaps.nix')
-rw-r--r-- | pkgs/applications/science/logic/tlaplus/tlaps.nix | 56 |
1 files changed, 56 insertions, 0 deletions
diff --git a/pkgs/applications/science/logic/tlaplus/tlaps.nix b/pkgs/applications/science/logic/tlaplus/tlaps.nix new file mode 100644 index 00000000000..9a78c1df8b1 --- /dev/null +++ b/pkgs/applications/science/logic/tlaplus/tlaps.nix @@ -0,0 +1,56 @@ +{ lib +, fetchurl +, makeWrapper +, stdenv +, ocaml, gawk, isabelle, cvc3, perl, wget, which +}: + +stdenv.mkDerivation rec { + name = "tlaps-${version}"; + 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 ]; + }; + +} |