Unverified Commit 6793c66b authored by @mjones's avatar @mjones Committed by GitHub
Browse files

vampire: allow z3 override and add update script (#487238)

parents b667c25e ee06439c

pkgs/by-name/is/isabelle/package.nix

+27 −22
Original line number Diff line number Diff line
@@ -51,7 +51,12 @@ let 
  # Isabelle uses a branch of vampire that is not in the normal release line

  # that adds support for higher order goals

  vampireStdenv = if stdenv.hostPlatform.isLinux then gcc14Stdenv else stdenv;

  vampire' = (vampire.override { stdenv = vampireStdenv; }).overrideAttrs (_: {

  vampire' =

    (vampire.override {

      stdenv = vampireStdenv;

      z3' = null;

    }).overrideAttrs

      (_: {

        pname = "vampire-for-isabelle";

        version = "4.8";

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

+8 −8
Original line number Diff line number Diff line
@@ -4,10 +4,7 @@ 
  fetchFromGitHub,

  cmake,

  z3,

}:



let

  z3_4_14_0 = z3.overrideAttrs rec {

  z3' ? z3.overrideAttrs rec {

    version = "4.14.0";

    src = fetchFromGitHub {

      owner = "Z3Prover";
@@ -15,8 +12,9 @@ let 
      rev = "z3-${version}";

      hash = "sha256-Bv7+0J7ilJNFM5feYJqDpYsOjj7h7t1Bx/4OIar43EI=";

    };

  };

in

  },

  nix-update-script,

}:

stdenv.mkDerivation (finalAttrs: {

  pname = "vampire";

  version = "5.0.1";
@@ -31,10 +29,10 @@ stdenv.mkDerivation (finalAttrs: { 


  nativeBuildInputs = [ cmake ];

  buildInputs = [

    z3_4_14_0

    z3'

  ];



  cmakeFlags = [ (lib.cmakeFeature "Z3_DIR" "${z3_4_14_0.dev}/lib/cmake") ];

  cmakeFlags = [ (lib.cmakeFeature "Z3_DIR" "${z3'.dev}/lib/cmake") ];



  enableParallelBuilding = true;
@@ -42,6 +40,8 @@ stdenv.mkDerivation (finalAttrs: { 
    rm -rf z3

  '';



  passthru.updateScript = nix-update-script { };



  meta = {

    homepage = "https://vprover.github.io/";

    description = "Vampire Theorem Prover";

pkgs/by-name/z3/z3/package.nix

+25 −22
Original line number Diff line number Diff line
@@ -38,8 +38,11 @@ stdenv.mkDerivation (finalAttrs: { 
    hash = "sha256-eyF3ELv81xEgh9Km0Ehwos87e4VJ82cfsp53RCAtuTo=";

  };



  patches = lib.optionals useCmakeBuild [

  patches =

    lib.optionals useCmakeBuild [

      ./fix-pkg-config-paths.patch

    ]

    ++ lib.optionals (lib.versionAtLeast finalAttrs.version "4.15.4") [

      # fix Segmentation fault. See https://github.com/Z3Prover/z3/pull/8264 and

      # https://github.com/NixOS/nixpkgs/issues/486491

      (fetchpatch2 {