diff options
author | Jan van Brügge <supermanitu@gmail.com> | 2022-12-03 17:03:20 +0000 |
---|---|---|
committer | Jan van Brügge <supermanitu@gmail.com> | 2022-12-03 18:34:13 +0000 |
commit | 26c369214e6f76216ac3ef6ed7dddfaad486ab3e (patch) | |
tree | 2ff8b31cf8a76c4af51fb9fb4f5febbe2c07fe62 /pkgs/applications/science | |
parent | d5299641bb35b3ead5db880a02a27d1665587f5e (diff) |
isabelle: use prebuilt z3
Isabelle requires this specific version of z3 which is being removed from nixpkgs due to requiring python2 for its build. We can work around this by patching the distributed binary
Diffstat (limited to 'pkgs/applications/science')
-rw-r--r-- | pkgs/applications/science/logic/isabelle/default.nix | 22 |
1 files changed, 8 insertions, 14 deletions
diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix index 7a796cefe4411..dce3695723961 100644 --- a/pkgs/applications/science/logic/isabelle/default.nix +++ b/pkgs/applications/science/logic/isabelle/default.nix @@ -6,7 +6,6 @@ , java , scala_3 , polyml -, z3 , veriT , vampire , eprover-ho @@ -67,11 +66,14 @@ in stdenv.mkDerivation (finalAttrs: rec { nativeBuildInputs = [ java ]; - buildInputs = [ polyml z3 veriT vampire eprover-ho nettools ] + buildInputs = [ polyml veriT vampire eprover-ho nettools ] ++ lib.optionals (!stdenv.isDarwin) [ java ]; sourceRoot = dirname; + doCheck = true; + checkPhase = "bin/isabelle build -v HOL-SMT_Examples"; + postUnpack = lib.optionalString stdenv.isDarwin '' mv $sourceRoot.app $sourceRoot ''; @@ -79,13 +81,6 @@ in stdenv.mkDerivation (finalAttrs: rec { postPatch = '' patchShebangs lib/Tools/ bin/ - cat >contrib/z3*/etc/settings <<EOF - Z3_HOME=${z3} - Z3_VERSION=${z3.version} - Z3_SOLVER=${z3}/bin/z3 - Z3_INSTALLED=yes - EOF - cat >contrib/verit-*/etc/settings <<EOF ISABELLE_VERIT=${veriT}/bin/veriT EOF @@ -121,7 +116,7 @@ in stdenv.mkDerivation (finalAttrs: rec { echo ISABELLE_LINE_EDITOR=${rlwrap}/bin/rlwrap >>etc/settings - for comp in contrib/jdk* contrib/polyml-* contrib/z3-* contrib/verit-* contrib/vampire-* contrib/e-*; do + for comp in contrib/jdk* contrib/polyml-* contrib/verit-* contrib/vampire-* contrib/e-*; do rm -rf $comp/x86* done @@ -142,15 +137,14 @@ in stdenv.mkDerivation (finalAttrs: rec { --replace 'ISABELLE_APPLE_PLATFORM64=arm64-darwin' "" '' + lib.optionalString stdenv.isLinux '' arch=${if stdenv.hostPlatform.system == "x86_64-linux" then "x86_64-linux" else "x86-linux"} - for f in contrib/*/$arch/{bash_process,epclextract,nunchaku,SPASS,zipperposition}; do - patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) "$f" - done - for f in contrib/*/platform_$arch/{bash_process,epclextract,nunchaku,SPASS,zipperposition}; do + for f in contrib/*/$arch/{z3,epclextract,nunchaku,SPASS,zipperposition}; do patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) "$f" done + patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) contrib/bash_process-*/platform_$arch/bash_process for d in contrib/kodkodi-*/jni/$arch; do patchelf --set-rpath "${lib.concatStringsSep ":" [ "${java}/lib/openjdk/lib/server" "${stdenv.cc.cc.lib}/lib" ]}" $d/*.so done + patchelf --set-rpath "${stdenv.cc.cc.lib}/lib" contrib/z3-*/$arch/z3 ''; buildPhase = '' |