JakeHillion/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

isabelle: use prebuilt z3

Browse Source 
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
This commit is contained in:
Jan van Brügge 2022-12-03 17:03:20 +00:00
parent d5299641bb
commit 26c369214e
No known key found for this signature in database
GPG Key ID: 88E0BF7B7A546481
2 changed files with 8 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
pkgs/applications/science/logic/isabelle/default.nix
View File

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

8
pkgs/top-level/all-packages.nix
View File

@ -35911,14 +35911,6 @@ with pkgs;
});
java = openjdk17;
z3 = z3_4_4_0.overrideAttrs (_: {
src = fetchFromGitHub {
owner = "Z3Prover";
repo = "z3";
rev = "0482e7fe727c75e259ac55a932b28cf1842c530e";
sha256 = "1m53avlljxqd2p8w266ksmjywjycsd23h224yn786qsnf36dr63x";
};
});
};
isabelle-components = recurseIntoAttrs (callPackage ../applications/science/logic/isabelle/components { });