diff options
Diffstat (limited to 'pkgs/applications/science/logic')
5 files changed, 35 insertions, 13 deletions
diff --git a/pkgs/applications/science/logic/abc/default.nix b/pkgs/applications/science/logic/abc/default.nix index fe73f4f4d6e..60454ca9ce9 100644 --- a/pkgs/applications/science/logic/abc/default.nix +++ b/pkgs/applications/science/logic/abc/default.nix @@ -4,13 +4,13 @@ stdenv.mkDerivation rec { pname = "abc-verifier"; - version = "2021.11.12"; + version = "2022.03.04"; src = fetchFromGitHub { owner = "yosyshq"; repo = "abc"; - rev = "f6fa2ddcfc89099726d60386befba874c7ac1e0d"; - hash = "sha256-0rvMPZ+kL0m/GjlCLx3eXYQ0osQ2wQiS3+csqPl3U9s="; + rev = "d7ecb23eeee9c9b4924182ce570c2e33eb18abff"; + hash = "sha256-aufWRTggJNOaUFsjh5+HFDqEur+nuM0hZSsTfGptbks="; }; nativeBuildInputs = [ cmake ]; diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix index 96e8da059a4..aaac288b615 100644 --- a/pkgs/applications/science/logic/isabelle/default.nix +++ b/pkgs/applications/science/logic/isabelle/default.nix @@ -1,4 +1,4 @@ -{ lib, stdenv, fetchurl, coreutils, nettools, java, polyml, z3, veriT, vampire, eprover-ho, rlwrap, makeDesktopItem }: +{ lib, stdenv, fetchurl, coreutils, nettools, java, scala, polyml, z3, veriT, vampire, eprover-ho, rlwrap, perl, makeDesktopItem }: # nettools needed for hostname stdenv.mkDerivation rec { @@ -77,6 +77,10 @@ stdenv.mkDerivation rec { substituteInPlace lib/Tools/env \ --replace /usr/bin/env ${coreutils}/bin/env + substituteInPlace src/Tools/Setup/src/Environment.java \ + --replace 'cmd.add("/usr/bin/env");' "" \ + --replace 'cmd.add("bash");' "cmd.add(\"$SHELL\");" + rm -r heaps '' + (if ! stdenv.isLinux then "" else '' arch=${if stdenv.hostPlatform.system == "x86_64-linux" then "x86_64-linux" else "x86-linux"} @@ -90,6 +94,24 @@ stdenv.mkDerivation rec { buildPhase = '' export HOME=$TMP # The build fails if home is not set + setup_name=$(basename contrib/isabelle_setup*) + + #The following is adapted from https://isabelle.sketis.net/repos/isabelle/file/Isabelle2021-1/Admin/lib/Tools/build_setup + TARGET_DIR="contrib/$setup_name/lib" + rm -rf "$TARGET_DIR" + mkdir -p "$TARGET_DIR/isabelle/setup" + declare -a ARGS=("-Xlint:unchecked") + + SOURCES="$(${perl}/bin/perl -e 'while (<>) { if (m/(\S+\.java)/) { print "$1 "; } }' "src/Tools/Setup/etc/build.props")" + for SRC in $SOURCES + do + ARGS["''${#ARGS[@]}"]="src/Tools/Setup/$SRC" + done + ${java}/bin/javac -d "$TARGET_DIR" -classpath ${scala}/lib/scala-compiler.jar "''${ARGS[@]}" + ${java}/bin/jar -c -f "$TARGET_DIR/isabelle_setup.jar" -e "isabelle.setup.Setup" -C "$TARGET_DIR" isabelle + rm -rf "$TARGET_DIR/isabelle" + + # Prebuild HOL Session bin/isabelle build -v -o system_heaps -b HOL ''; diff --git a/pkgs/applications/science/logic/lean/default.nix b/pkgs/applications/science/logic/lean/default.nix index 22e755bd852..1eea97a0fd2 100644 --- a/pkgs/applications/science/logic/lean/default.nix +++ b/pkgs/applications/science/logic/lean/default.nix @@ -2,7 +2,7 @@ stdenv.mkDerivation rec { pname = "lean"; - version = "3.39.2"; + version = "3.41.0"; src = fetchFromGitHub { owner = "leanprover-community"; @@ -11,8 +11,8 @@ stdenv.mkDerivation rec { # from. this is then used to check whether an olean file should be # rebuilt. don't use a tag as rev because this will get replaced into # src/githash.h.in in preConfigure. - rev = "402f41cdedbd46a368fb7807bebe83550d887631"; - sha256 = "0jddakr07ixspw19xblpj1882vxxaljg3fflhn4myvigwzkav334"; + rev = "154ac72f4ff674bc4486ac611f926a3d6b999f9f"; + sha256 = "0mpxlfjq460x1vi3v6qzgjv74asg0qlhykd51pj347795x5b1hf1"; }; nativeBuildInputs = [ cmake ]; diff --git a/pkgs/applications/science/logic/opensmt/default.nix b/pkgs/applications/science/logic/opensmt/default.nix index e701fb2711f..ef6f9b157d2 100644 --- a/pkgs/applications/science/logic/opensmt/default.nix +++ b/pkgs/applications/science/logic/opensmt/default.nix @@ -6,13 +6,13 @@ stdenv.mkDerivation rec { pname = "opensmt"; - version = "2.2.0"; + version = "2.3.0"; src = fetchFromGitHub { owner = "usi-verification-and-security"; repo = "opensmt"; rev = "v${version}"; - sha256 = "sha256-6VkBGDzqG3mplpvFh5DIR0I1I2/J0Pi7xYk/yVn04Kg="; + sha256 = "sha256-5Gw9+J+3LHNUNbcHxsQR/ivWndL2P7yBt/Q35fBMg58="; }; nativeBuildInputs = [ cmake bison flex ]; diff --git a/pkgs/applications/science/logic/tlaplus/tlaps.nix b/pkgs/applications/science/logic/tlaplus/tlaps.nix index 90a4aeb4f8a..14b3055ab36 100644 --- a/pkgs/applications/science/logic/tlaplus/tlaps.nix +++ b/pkgs/applications/science/logic/tlaplus/tlaps.nix @@ -11,10 +11,10 @@ stdenv.mkDerivation rec { pname = "tlaps"; - version = "1.4.3"; + version = "1.4.5"; src = fetchurl { - url = "https://tla.msr-inria.inria.fr/tlaps/dist/current/tlaps-${version}.tar.gz"; - sha256 = "1w5z3ns5xxmhmp8r4x2kjmy3clqam935gmvx82imyxrr1bamx6gf"; + url = "https://tla.msr-inria.inria.fr/tlaps/dist/${version}/tlaps-${version}.tar.gz"; + sha256 = "c296998acd14d5b93a8d5be7ee178007ef179957465966576bda26944b1b7fca"; }; buildInputs = [ ocaml isabelle cvc3 perl wget which ]; @@ -52,7 +52,7 @@ stdenv.mkDerivation rec { homepage = "https://tla.msr-inria.inria.fr/tlaps/content/Home.html"; license = lib.licenses.bsd2; platforms = lib.platforms.unix; - maintainers = [ ]; + maintainers = with lib.maintainers; [ florentc ]; }; } |