From b54e5a841b2118a51397eefaab2408daaa5e99e5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Sat, 1 Jan 2022 22:13:11 +0100 Subject: [PATCH 1/4] vampire: 4.5.1 -> 4.6.1 --- pkgs/applications/science/logic/vampire/default.nix | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/pkgs/applications/science/logic/vampire/default.nix b/pkgs/applications/science/logic/vampire/default.nix index b88544544462..307c75b272bc 100644 --- a/pkgs/applications/science/logic/vampire/default.nix +++ b/pkgs/applications/science/logic/vampire/default.nix @@ -2,13 +2,13 @@ stdenv.mkDerivation rec { pname = "vampire"; - version = "4.5.1"; + version = "4.6.1"; src = fetchFromGitHub { owner = "vprover"; repo = "vampire"; - rev = version; - sha256 = "0q9gqyq96amdnhxgwjyv0r2sxakikp3jvmizgj2h0spfz643p8db"; + rev = "v${version}"; + sha256 = "0z71nxjak3ibp842r8iv37w1x3cbkrmjs88lpvxqb4sgrbyk38zd"; }; buildInputs = [ z3 zlib ]; @@ -50,7 +50,7 @@ stdenv.mkDerivation rec { homepage = "https://vprover.github.io/"; description = "The Vampire Theorem Prover"; platforms = platforms.unix; - license = licenses.unfree; + license = licenses.bsd3; maintainers = with maintainers; [ gebner ]; }; } From 63e9fb044878be5d2eace2802739e9b4547d50be Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Sun, 2 Jan 2022 10:51:58 +0100 Subject: [PATCH 2/4] isabelle: Use openjdk17 This is the same openjdk version that is used in upstream isabelle. --- pkgs/top-level/all-packages.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 4ec320af5a2f..b55a618f44d6 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -31998,7 +31998,7 @@ with pkgs; configureFlags = [ "--enable-intinf-as-int" "--with-gmp" "--disable-shared" ]; }); - java = openjdk11; + java = openjdk17; z3 = z3_4_4_0; }; From f79b811f2dd62f5ae46fc460164ebbd865cf9c44 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Sun, 2 Jan 2022 11:16:27 +0100 Subject: [PATCH 3/4] eprover: Add option to enable LFHOL reasoning Using eprover as automated theorem prover for sledgehammer requires this option. --- pkgs/applications/science/logic/eprover/default.nix | 4 +++- pkgs/top-level/all-packages.nix | 2 ++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/pkgs/applications/science/logic/eprover/default.nix b/pkgs/applications/science/logic/eprover/default.nix index 3b757d40a694..400d636346c5 100644 --- a/pkgs/applications/science/logic/eprover/default.nix +++ b/pkgs/applications/science/logic/eprover/default.nix @@ -1,4 +1,4 @@ -{ lib, stdenv, fetchurl, which }: +{ lib, stdenv, fetchurl, which, enableHO ? false }: stdenv.mkDerivation rec { pname = "eprover"; @@ -17,6 +17,8 @@ stdenv.mkDerivation rec { configureFlags = [ "--exec-prefix=$(out)" "--man-prefix=$(out)/share/man" + ] ++ lib.optionals enableHO [ + "--enable-ho" ]; meta = with lib; { diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index b55a618f44d6..d798645eb60d 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -31965,6 +31965,8 @@ with pkgs; eprover = callPackage ../applications/science/logic/eprover { }; + eprover-ho = callPackage ../applications/science/logic/eprover { enableHO = true; }; + gappa = callPackage ../applications/science/logic/gappa { }; gfan = callPackage ../applications/science/math/gfan {}; From c601134af8e58ec26401c8b19e96d1a599fcf90e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Sun, 2 Jan 2022 10:49:38 +0100 Subject: [PATCH 4/4] isabelle: Use vampire and eprover from nixpkgs It also removes the unused perl input --- .../science/logic/isabelle/default.nix | 20 ++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix index e69c76352b90..32d89d7e22ae 100644 --- a/pkgs/applications/science/logic/isabelle/default.nix +++ b/pkgs/applications/science/logic/isabelle/default.nix @@ -1,4 +1,4 @@ -{ lib, stdenv, fetchurl, perl, perlPackages, makeWrapper, nettools, java, polyml, z3, veriT, rlwrap, makeDesktopItem }: +{ lib, stdenv, fetchurl, nettools, java, polyml, z3, veriT, vampire, eprover-ho, rlwrap, makeDesktopItem }: # nettools needed for hostname stdenv.mkDerivation rec { @@ -17,8 +17,7 @@ stdenv.mkDerivation rec { sha256 = "0jfaqckhg388jh9b4msrpkv6wrd6xzlw18m0bngbby8k8ywalp9i"; }; - nativeBuildInputs = [ makeWrapper ]; - buildInputs = [ perl polyml z3 veriT ] + buildInputs = [ polyml z3 veriT vampire eprover-ho ] ++ lib.optionals (!stdenv.isDarwin) [ nettools java ]; sourceRoot = dirname; @@ -37,6 +36,17 @@ stdenv.mkDerivation rec { ISABELLE_VERIT=${veriT}/bin/veriT EOF + cat >contrib/e-*/etc/settings <contrib/vampire-*/etc/settings <contrib/polyml-*/etc/settings <>etc/settings - for comp in contrib/jdk* contrib/polyml-* contrib/z3-* contrib/verit-*; do + for comp in contrib/jdk* contrib/polyml-* contrib/z3-* contrib/verit-* contrib/vampire-* contrib/e-*; do rm -rf $comp/x86* done '' + (if ! stdenv.isLinux then "" else '' arch=${if stdenv.hostPlatform.system == "x86_64-linux" then "x86_64-linux" else "x86-linux"} - for f in contrib/*/$arch/{bash_process,epclextract,eprover,nunchaku,SPASS}; do + for f in contrib/*/$arch/{bash_process,epclextract,nunchaku,SPASS}; do patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) "$f" done '');