Merge pull request #38589 from badi/tlatools

Add TLAPS and TLA+ Toolbox

2 files changed, 133 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 000000000000..9a78c1df8b17
--- /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 ];
+  };
+
+}
diff --git a/pkgs/applications/science/logic/tlaplus/toolbox.nix b/pkgs/applications/science/logic/tlaplus/toolbox.nix
new file mode 100644
index 000000000000..5ce359dea0ec
--- /dev/null
+++ b/pkgs/applications/science/logic/tlaplus/toolbox.nix
@@ -0,0 +1,77 @@
+{ lib, fetchzip, makeWrapper, makeDesktopItem, stdenv
+, jre, swt, gtk, libXtst, glib
+}:
+
+let
+  version = "1.5.6";
+  arch = "x86_64";
+
+  desktopItem = makeDesktopItem rec {
+    name = "TLA+Toolbox";
+    exec = "tla-toolbox";
+    icon = "tla-toolbox";
+    comment = "IDE for TLA+";
+    desktopName = name;
+    genericName = comment;
+    categories = "Application;Development";
+    extraEntries = ''
+      StartupWMClass=TLA+ Toolbox
+    '';
+  };
+
+
+in stdenv.mkDerivation {
+  name = "tla-toolbox-${version}";
+  src = fetchzip {
+    url = "https://tla.msr-inria.inria.fr/tlatoolbox/products/TLAToolbox-${version}-linux.gtk.${arch}.zip";
+    sha256 = "1h63mcbrkf4jcg6qncpqffdi0x665z0wlfdq43d67p411xcqmbw9";
+  };
+
+  buildInputs = [ makeWrapper  ];
+
+  phases = [ "installPhase" ];
+
+  installPhase = ''
+    mkdir -p "$out/bin"
+    cp -r "$src" "$out/toolbox"
+    chmod +w "$out/toolbox" "$out/toolbox/toolbox"
+
+    patchelf \
+      --set-interpreter $(cat $NIX_CC/nix-support/dynamic-linker) \
+      "$out/toolbox/toolbox"
+
+    makeWrapper $out/toolbox/toolbox $out/bin/tla-toolbox \
+      --run "set -x; cd $out/toolbox" \
+      --add-flags "-data ~/.tla-toolbox" \
+      --prefix PATH : "${jre}/bin" \
+      --prefix LD_LIBRARY_PATH : "${swt}/lib:${gtk}/lib:${libXtst}/lib:${glib}/lib"
+
+    echo -e "\nCreating TLA Toolbox icons..."
+    pushd "$src"
+    for icon_in in $(find . -path "./plugins/*/icons/full/etool16/tla_launch_check_wiz_*.png")
+    do
+      icon_size=$(echo $icon_in | grep -Po "wiz_\K[0-9]+")
+      icon_out="$out/share/icons/hicolor/$icon_size""x$icon_size/apps/tla-toolbox.png"
+      mkdir -p "$(dirname $icon_out)"
+      cp "$icon_in" "$icon_out"
+    done
+    popd
+
+    echo -e "\nCreating TLA Toolbox desktop entry..."
+    cp -r "${desktopItem}/share/applications"* "$out/share/applications"
+  '';
+
+  meta = {
+    homepage = http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html;
+    description = "IDE for the TLA+ tools";
+    longDescription = ''
+      Integrated development environment for the TLA+ tools, based on Eclipse. You can use it
+      to create and edit your specs, run the PlusCal translator, view the pretty-printed
+      versions of your modules, run the TLC model checker, and run TLAPS, the TLA+ proof system.
+    '';
+    # http://lamport.azurewebsites.net/tla/license.html
+    license = with lib.licenses; [ mit ];
+    platforms = stdenv.lib.platforms.linux;
+    maintainers = [ stdenv.lib.maintainers.badi ];
+  };
+}