diff --git a/pkgs/by-name/is/isabelle/package.nix b/pkgs/by-name/is/isabelle/package.nix index 1a5f04256fab..edb814d0e537 100644 --- a/pkgs/by-name/is/isabelle/package.nix +++ b/pkgs/by-name/is/isabelle/package.nix @@ -56,9 +56,9 @@ let vampire' = (vampire.override { stdenv = vampireStdenv; - z3' = null; + enableZ3 = false; }).overrideAttrs - (_: { + (old: { pname = "vampire-for-isabelle"; version = "4.8"; @@ -75,9 +75,8 @@ let mv $out/bin/vampire_rel $out/bin/vampire ''; - cmakeFlags = [ + cmakeFlags = old.cmakeFlags ++ [ (lib.cmakeFeature "CMAKE_BUILD_HOL" "On") - (lib.cmakeFeature "CMAKE_DISABLE_FIND_PACKAGE_Z3" "On") ]; }); diff --git a/pkgs/by-name/va/vampire/package.nix b/pkgs/by-name/va/vampire/package.nix index f0324e379638..55601ae57f04 100644 --- a/pkgs/by-name/va/vampire/package.nix +++ b/pkgs/by-name/va/vampire/package.nix @@ -4,6 +4,8 @@ fetchFromGitHub, cmake, z3, + # We use an older version of z3 because upstream pins this older version as a submodule + # And doesn't recommend using different versions unless you know specfically what you are doing z3' ? z3.overrideAttrs rec { version = "4.14.0"; src = fetchFromGitHub { @@ -13,34 +15,56 @@ hash = "sha256-Bv7+0J7ilJNFM5feYJqDpYsOjj7h7t1Bx/4OIar43EI="; }; }, + enableZ3 ? z3' != null, nix-update-script, }: stdenv.mkDerivation (finalAttrs: { pname = "vampire"; - version = "5.0.1"; + version = "5.1.0"; + + __structuredAttrs = true; + strictDeps = true; src = fetchFromGitHub { owner = "vprover"; repo = "vampire"; tag = "v${finalAttrs.version}"; - hash = "sha256-Ka9HmicIf7b5VN9nbiCW604ZZrGpJuP57RPTzOnwJbU="; + hash = "sha256-zPE2GmaHupBhyPEZFcoRADzClPKYydlJ74dNkyQpJa8="; fetchSubmodules = true; }; nativeBuildInputs = [ cmake ]; - buildInputs = [ - z3' + buildInputs = [ z3' ]; + + # Needed so we can case on it's value + cmakeBuildType = "Release"; + buildFlags = lib.optionals (finalAttrs.doCheck) [ + "all" + "vtest" ]; - cmakeFlags = [ (lib.cmakeFeature "Z3_DIR" "${z3'.dev}/lib/cmake") ]; - - enableParallelBuilding = true; + cmakeFlags = [ + (lib.cmakeBool "CMAKE_DISABLE_FIND_PACKAGE_Z3" (!enableZ3)) + ] + ++ lib.optionals enableZ3 [ + (lib.cmakeFeature "Z3_DIR" "${z3'.dev}/lib/cmake") + ]; prePatch = '' rm -rf z3 ''; - passthru.updateScript = nix-update-script { }; + # The tests only are able to be built in Debug builds, otherwise the `vtest` + # binary doesn't exist as a target + doCheck = finalAttrs.cmakeBuildType == "Debug"; + + passthru = { + updateScript = nix-update-script { }; + z3 = z3'; + tests.debug-build-with-tests = finalAttrs.finalPackage.overrideAttrs { + cmakeBuildType = "Debug"; + }; + }; meta = { homepage = "https://vprover.github.io/";