pkgs/applications/science/logic/tlaplus/tlaps.nix

   1 { fetchurl
   2 , lib
   3 , stdenv
   4 , ocaml
   5 , isabelle
   6 , cvc3
   7 , perl
   8 , wget
   9 , which
  10 }:
  11
  12 stdenv.mkDerivation rec {
  13   pname = "tlaps";
  14   version = "1.4.5";
  15   src = fetchurl {
  16     url = "https://tla.msr-inria.inria.fr/tlaps/dist/${version}/tlaps-${version}.tar.gz";
  17     sha256 = "c296998acd14d5b93a8d5be7ee178007ef179957465966576bda26944b1b7fca";
  18   };
  19
  20   strictDeps = true;
  21
  22   nativeBuildInputs = [ ocaml isabelle cvc3 perl wget which ];
  23
  24   installPhase = ''
  25     mkdir -pv "$out"
  26     export HOME="$out"
  27     export PATH=$out/bin:$PATH
  28
  29     pushd zenon
  30     ./configure --prefix $out
  31     make
  32     make install
  33     popd
  34
  35     pushd isabelle
  36     isabelle build -b Pure
  37     popd
  38
  39     pushd tlapm
  40     ./configure --prefix $out
  41     make all
  42     make install
  43   '';
  44
  45   meta = {
  46     description = "Mechanically check TLA+ proofs";
  47     longDescription = ''
  48       TLA+ is a general-purpose formal specification language that is
  49       particularly useful for describing concurrent and distributed
  50       systems. The TLA+ proof language is declarative, hierarchical,
  51       and scalable to large system specifications. It provides a
  52       consistent abstraction over the various “backend” verifiers.
  53     '';
  54     homepage = "https://tla.msr-inria.inria.fr/tlaps/content/Home.html";
  55     license = lib.licenses.bsd2;
  56     platforms = lib.platforms.unix;
  57     maintainers = with lib.maintainers; [ florentc ];
  58   };
  59
  60 }