vampire: 4.9 -> 5.0.0 (#475823)

maintainers/maintainer-list.nix

@@ -23801,6 +23801,11 @@
     githubId = 33031;
     name = "Greg Pfeil";
   };
+  sempiternal-aurora = {
+    github = "sempiternal-aurora";
+    githubId = 78790545;
+    name = "Myria Sarvay";
+  };
   semtexerror = {
     email = "github@spampert.com";
     github = "SemtexError";

pkgs/by-name/va/vampire/minisat-fenv.patch

@@ -1,57 +0,0 @@
-diff --git a/core/Main.cc b/core/Main.cc
-index 2b0d97b..9ba985d 100644
---- a/core/Main.cc
-+++ b/core/Main.cc
-@@ -77,9 +77,13 @@ int main(int argc, char** argv)
-         setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
-         // printf("This is MiniSat 2.0 beta\n");
-         
--#if defined(__linux__)
--        fpu_control_t oldcw, newcw;
--        _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
-+#if defined(__linux__) && defined(__x86_64__)
-+        fenv_t fenv;
-+
-+        fegetenv(&fenv);
-+        fenv.__control_word &= ~0x300; /* _FPU_EXTENDED */
-+        fenv.__control_word |= 0x200; /* _FPU_DOUBLE */
-+        fesetenv(&fenv);
-         printf("WARNING: for repeatability, setting FPU to use double precision\n");
- #endif
-         // Extra options:
-diff --git a/simp/Main.cc b/simp/Main.cc
-index 2804d7f..7fbdb33 100644
---- a/simp/Main.cc
-+++ b/simp/Main.cc
-@@ -78,9 +78,13 @@ int main(int argc, char** argv)
-         setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
-         // printf("This is MiniSat 2.0 beta\n");
-         
--#if defined(__linux__)
--        fpu_control_t oldcw, newcw;
--        _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
-+#if defined(__linux__) && defined(__x86_64__)
-+        fenv_t fenv;
-+
-+        fegetenv(&fenv);
-+        fenv.__control_word &= ~0x300; /* _FPU_EXTENDED */
-+        fenv.__control_word |= 0x200; /* _FPU_DOUBLE */
-+        fesetenv(&fenv);
-         printf("WARNING: for repeatability, setting FPU to use double precision\n");
- #endif
-         // Extra options:
-diff --git a/utils/System.h b/utils/System.h
-index 1758192..840bee5 100644
---- a/utils/System.h
-+++ b/utils/System.h
-@@ -21,8 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
- #ifndef Minisat_System_h
- #define Minisat_System_h
- 
--#if defined(__linux__)
--#include <fpu_control.h>
-+#if defined(__linux__) && defined(__x86_64__)
-+#include <fenv.h>
- #endif
- 
- #include "mtl/IntTypes.h"

pkgs/by-name/va/vampire/package.nix

@@ -2,50 +2,56 @@
   lib,
   stdenv,
   fetchFromGitHub,
+  cmake,
   z3,
-  zlib,
 }:
 
-stdenv.mkDerivation rec {
+let
+  z3_4_14_0 = z3.overrideAttrs rec {
+    version = "4.14.0";
+    src = fetchFromGitHub {
+      owner = "Z3Prover";
+      repo = "z3";
+      rev = "z3-${version}";
+      hash = "sha256-Bv7+0J7ilJNFM5feYJqDpYsOjj7h7t1Bx/4OIar43EI=";
+    };
+  };
+in
+stdenv.mkDerivation (finalAttrs: {
   pname = "vampire";
-  version = "4.9";
+  version = "5.0.0";
 
   src = fetchFromGitHub {
     owner = "vprover";
     repo = "vampire";
-    tag = "v${version}casc2024";
-    hash = "sha256-NHAlPIy33u+TRmTuFoLRlPCvi3g62ilTfJ0wleboMNU=";
+    tag = "v${finalAttrs.version}";
+    hash = "sha256-jRzVh1KirWi9GpOkzSGoIBUExDN1rV0b3AGwa6gWb3I=";
+    fetchSubmodules = true;
   };
 
+  nativeBuildInputs = [ cmake ];
   buildInputs = [
-    z3
-    zlib
+    z3_4_14_0
   ];
 
-  makeFlags = [
-    "vampire_z3_rel"
-    "CC:=$(CC)"
-    "CXX:=$(CXX)"
-  ];
-
-  postPatch = ''
-    patch -p1 -i ${./minisat-fenv.patch} -d Minisat || true
-  '';
+  cmakeFlags = [ (lib.cmakeFeature "Z3_DIR" "${z3_4_14_0.dev}/lib/cmake") ];
 
   enableParallelBuilding = true;
 
-  fixupPhase = ''
-    runHook preFixup
-
+  prePatch = ''
     rm -rf z3
-
-    runHook postFixup
   '';
 
   installPhase = ''
     runHook preInstall
 
-    install -m0755 -D vampire_z3_rel* $out/bin/vampire
+    # some versions place the binary at ./ while others at bin/
+    if test -n "$(find . -maxdepth 1 -name 'vampire*' -print -quit)"
+    then
+      install -m0755 -D vampire* $out/bin/vampire
+    else
+      install -m0755 -D bin/vampire* $out/bin/vampire
+    fi
 
     runHook postInstall
   '';
@@ -56,6 +62,6 @@ stdenv.mkDerivation rec {
     mainProgram = "vampire";
     platforms = lib.platforms.unix;
     license = lib.licenses.bsd3;
-    maintainers = [ ];
+    maintainers = with lib.maintainers; [ sempiternal-aurora ];
   };
-}
+})