1 files changed, 60 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..59afbc094e40
--- /dev/null
+++ b/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix
@@ -0,0 +1,60 @@
+{ 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";
+  };
+
+  strictDeps = true;
+
+  nativeBuildInputs = [ 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 ];
+  };
+
+}