From bc38aa55f5d7bdbbdae658b576da0890217067d0 Mon Sep 17 00:00:00 2001 From: sempiternal-aurora <78790545+sempiternal-aurora@users.noreply.github.com> Date: Thu, 1 Jan 2026 15:53:03 +0800 Subject: [PATCH 1/2] maintainers: add sempiternal-aurora --- maintainers/maintainer-list.nix | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/maintainers/maintainer-list.nix b/maintainers/maintainer-list.nix index 161b48e0498b..a8ba10826ef5 100644 --- a/maintainers/maintainer-list.nix +++ b/maintainers/maintainer-list.nix @@ -23803,6 +23803,11 @@ githubId = 33031; name = "Greg Pfeil"; }; + sempiternal-aurora = { + github = "sempiternal-aurora"; + githubId = 78790545; + name = "Myria Sarvay"; + }; semtexerror = { email = "github@spampert.com"; github = "SemtexError"; From ddd80ed2c7433b20735ba7ef0af57898d1e3d3e4 Mon Sep 17 00:00:00 2001 From: sempiternal-aurora <78790545+sempiternal-aurora@users.noreply.github.com> Date: Thu, 1 Jan 2026 15:54:04 +0800 Subject: [PATCH 2/2] vampire: 4.9 -> 5.0.0 Release notes: https://github.com/vprover/vampire/releases/tag/v5.0.0 Fixes gcc15 build, changes to recommended cmake build, and removes old dependencies and patches --- pkgs/by-name/va/vampire/minisat-fenv.patch | 57 ---------------------- pkgs/by-name/va/vampire/package.nix | 54 +++++++++++--------- 2 files changed, 30 insertions(+), 81 deletions(-) delete mode 100644 pkgs/by-name/va/vampire/minisat-fenv.patch diff --git a/pkgs/by-name/va/vampire/minisat-fenv.patch b/pkgs/by-name/va/vampire/minisat-fenv.patch deleted file mode 100644 index 31e481bd6696..000000000000 --- a/pkgs/by-name/va/vampire/minisat-fenv.patch +++ /dev/null @@ -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] \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] \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 -+#if defined(__linux__) && defined(__x86_64__) -+#include - #endif - - #include "mtl/IntTypes.h" diff --git a/pkgs/by-name/va/vampire/package.nix b/pkgs/by-name/va/vampire/package.nix index adfb8ea0ffbc..ee354e8af38e 100644 --- a/pkgs/by-name/va/vampire/package.nix +++ b/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 ]; }; -} +})