diff options
Diffstat (limited to 'nixpkgs/pkgs/applications/science/logic')
6 files changed, 43 insertions, 32 deletions
diff --git a/nixpkgs/pkgs/applications/science/logic/beluga/default.nix b/nixpkgs/pkgs/applications/science/logic/beluga/default.nix index 55cee9b7e17..44478a032b3 100644 --- a/nixpkgs/pkgs/applications/science/logic/beluga/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/beluga/default.nix @@ -1,34 +1,40 @@ -{ stdenv, fetchFromGitHub, ocamlPackages, omake }: +{ lib, fetchFromGitHub, ocamlPackages, rsync }: -stdenv.mkDerivation { - name = "beluga-20180403"; +ocamlPackages.buildDunePackage { + pname = "beluga"; + version = "unstable-2020-03-11"; src = fetchFromGitHub { owner = "Beluga-lang"; repo = "Beluga"; - rev = "046aa59f008be70a7c4700b723bed0214ea8b687"; - sha256 = "0m68y0r0wdw3mg2jks68bihaww7sg305zdfnic1rkndq2cxv0mld"; + rev = "6133b2f572219333f304bb4f77c177592324c55b"; + sha256 = "0sy6mi50z3mvs5z7dx38piydapk89all81rh038x3559b5fsk68q"; }; - nativeBuildInputs = with ocamlPackages; [ findlib ocamlbuild omake ]; - buildInputs = with ocamlPackages; [ ocaml ulex ocaml_extlib ]; + useDune2 = true; - installPhase = '' - mkdir -p $out - cp -r bin $out/ + buildInputs = with ocamlPackages; [ + gen sedlex_2 ocaml_extlib dune-build-info linenoise + ]; - mkdir -p $out/share/beluga - cp -r tools/ examples/ $out/share/beluga + postPatch = '' + patchShebangs ./TEST ./run_harpoon_test.sh + ''; + + checkPhase = "./TEST"; + checkInputs = [ rsync ]; + doCheck = true; + postInstall = '' mkdir -p $out/share/emacs/site-lisp/beluga/ cp -r tools/beluga-mode.el $out/share/emacs/site-lisp/beluga ''; - meta = { + meta = with lib; { description = "A functional language for reasoning about formal systems"; homepage = "http://complogic.cs.mcgill.ca/beluga/"; - license = stdenv.lib.licenses.gpl3Plus; - maintainers = [ stdenv.lib.maintainers.bcdarwin ]; - platforms = stdenv.lib.platforms.unix; + license = licenses.gpl3Plus; + maintainers = [ maintainers.bcdarwin ]; + platforms = platforms.unix; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix b/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix index 113c6307c40..8c1b3bd0369 100644 --- a/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix @@ -2,13 +2,13 @@ stdenv.mkDerivation rec { pname = "cryptominisat"; - version = "5.6.8"; + version = "5.7.0"; src = fetchFromGitHub { owner = "msoos"; repo = "cryptominisat"; rev = version; - sha256 = "0csimmy1nvkfcsxjra9bm4mlcyxa3ac8zarm88zfb7640ca0d0wv"; + sha256 = "0ny5ln8fc0irprs04qw01c9mppps8q27lkx01a549zazwhj4b5rm"; }; buildInputs = [ python3 boost ]; diff --git a/nixpkgs/pkgs/applications/science/logic/elan/default.nix b/nixpkgs/pkgs/applications/science/logic/elan/default.nix index ea3b0585099..743bbf163c2 100644 --- a/nixpkgs/pkgs/applications/science/logic/elan/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/elan/default.nix @@ -2,16 +2,16 @@ rustPlatform.buildRustPackage rec { pname = "elan"; - version = "0.8.0"; + version = "0.10.0"; src = fetchFromGitHub { owner = "kha"; repo = "elan"; rev = "v${version}"; - sha256 = "0n2ncssjcmp3x5kbnci7xbq5fgcihlr3vaglyhhwzrxkjy2vpmpd"; + sha256 = "0aw538shvpfbk481y0gw3z97nsazdnk8qh8fwsb6ji62p2r51v6f"; }; - cargoSha256 = "1pkg0n7kxckr0zhr8dr12b9fxg5q185kj3r9k2rmnkj2dpa2mxh3"; + cargoSha256 = "0zg3q31z516049v9fhli4yxldx9fg31k2qfx4ag8rmyvpgy9xh6c"; nativeBuildInputs = [ pkgconfig ]; @@ -22,7 +22,7 @@ rustPlatform.buildRustPackage rec { postInstall = '' pushd $out/bin mv elan-init elan - for link in lean leanpkg leanchecker leanc; do + for link in lean leanpkg leanchecker leanc leanmake; do ln -s elan $link done popd diff --git a/nixpkgs/pkgs/applications/science/logic/lean/default.nix b/nixpkgs/pkgs/applications/science/logic/lean/default.nix index 594f596b5ef..ed077b03908 100644 --- a/nixpkgs/pkgs/applications/science/logic/lean/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/lean/default.nix @@ -1,14 +1,14 @@ -{ stdenv, fetchFromGitHub, cmake, gmp }: +{ stdenv, fetchFromGitHub, cmake, gmp, coreutils }: stdenv.mkDerivation rec { pname = "lean"; - version = "3.8.0"; + version = "3.13.1"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "lean"; rev = "v${version}"; - sha256 = "0frs2vhxlzdliyydb462c1886dn585zd7yp7hdxzsri2v6gdh89g"; + sha256 = "1ak5l40h5yjlbzz92l724l6bm5q341cg6k1yk13sbwn42l8szsar"; }; nativeBuildInputs = [ cmake ]; @@ -19,6 +19,11 @@ stdenv.mkDerivation rec { cd src ''; + postInstall = stdenv.lib.optionalString stdenv.isDarwin '' + substituteInPlace $out/bin/leanpkg \ + --replace "greadlink" "${coreutils}/bin/readlink" + ''; + meta = with stdenv.lib; { description = "Automatic and interactive theorem prover"; homepage = "https://leanprover.github.io/"; diff --git a/nixpkgs/pkgs/applications/science/logic/tlaplus/default.nix b/nixpkgs/pkgs/applications/science/logic/tlaplus/default.nix index 3476b5ea9d9..14944f5e19b 100644 --- a/nixpkgs/pkgs/applications/science/logic/tlaplus/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/tlaplus/default.nix @@ -1,24 +1,24 @@ { stdenv, fetchFromGitHub, makeWrapper -, jdk, jre, ant +, adoptopenjdk-bin, jre, ant }: stdenv.mkDerivation rec { pname = "tlaplus"; - version = "1.5.6"; + version = "1.7.0"; src = fetchFromGitHub { owner = "tlaplus"; repo = "tlaplus"; rev = "refs/tags/v${version}"; - sha256 = "0966mvgxamknj4hsp980qbxwda886w1dv309kn7isxn0420lfv4f"; + sha256 = "1mm6r9bq79zks50yk0agcpdkw9yy994m38ibmgpb3bi3wkpq9891"; }; - buildInputs = [ makeWrapper jdk ant ]; + buildInputs = [ makeWrapper adoptopenjdk-bin ant ]; - buildPhase = "ant -f tlatools/customBuild.xml compile dist"; + buildPhase = "ant -f tlatools/org.lamport.tlatools/customBuild.xml compile dist"; installPhase = '' mkdir -p $out/share/java $out/bin - cp tlatools/dist/*.jar $out/share/java + cp tlatools/org.lamport.tlatools/dist/*.jar $out/share/java makeWrapper ${jre}/bin/java $out/bin/tlc2 \ --add-flags "-cp $out/share/java/tla2tools.jar tlc2.TLC" diff --git a/nixpkgs/pkgs/applications/science/logic/verifast/default.nix b/nixpkgs/pkgs/applications/science/logic/verifast/default.nix index c5e8078eff2..49618d2586b 100644 --- a/nixpkgs/pkgs/applications/science/logic/verifast/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/verifast/default.nix @@ -43,7 +43,7 @@ stdenv.mkDerivation rec { meta = { description = "Verification for C and Java programs via separation logic"; homepage = "http://people.cs.kuleuven.be/~bart.jacobs/verifast/"; - license = stdenv.lib.licenses.msrla; + license = stdenv.lib.licenses.mit; platforms = [ "x86_64-linux" ]; maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; }; |