Merge pull request #153190 from jvanbruegge/isabelle-vampire

isabelle: Use vampire and eprover from nixpkgs

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; {

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 <<EOF
+      E_HOME=${eprover-ho}/bin
+      E_VERSION=${eprover-ho.version}
+    EOF
+
+    cat >contrib/vampire-*/etc/settings <<EOF
+      VAMPIRE_HOME=${vampire}/bin
+      VAMPIRE_VERSION=${vampire.version}
+      VAMPIRE_EXTRA_OPTIONS="--mode casc"
+    EOF
+
     cat >contrib/polyml-*/etc/settings <<EOF
       ML_SYSTEM_64=true
       ML_SYSTEM=${polyml.name}
@@ -56,12 +66,12 @@ stdenv.mkDerivation rec {
 
     echo ISABELLE_LINE_EDITOR=${rlwrap}/bin/rlwrap >>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
     '');

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 ];
   };
 }

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 {};
@@ -31998,7 +32000,7 @@ with pkgs;
       configureFlags = [ "--enable-intinf-as-int" "--with-gmp" "--disable-shared" ];
     });
 
-    java = openjdk11;
+    java = openjdk17;
     z3 = z3_4_4_0;
   };