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

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 = ''