tlaps: init at 1.4.3

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 ];
+  };
+
+}

pkgs/top-level/all-packages.nix

@@ -20029,6 +20029,8 @@ with pkgs;
   z3 = callPackage ../applications/science/logic/z3 { python = python2; };
 
   tlaplus = callPackage ../applications/science/logic/tlaplus {};
+  tlaps = callPackage ../applications/science/logic/tlaplus/tlaps.nix {};
+
 
   aiger = callPackage ../applications/science/logic/aiger {};