1 files changed, 54 insertions, 0 deletions
diff --git a/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix b/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix
new file mode 100644
index 000000000000..7d35f5f91df3
--- /dev/null
+++ b/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix
@@ -0,0 +1,54 @@
+{ fetchurl
+, stdenv
+, ocaml, 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 ];
+  };
+
+}