z3: refactor

This commit is contained in:
Tom van Dijk 2025-05-21 20:20:40 +02:00
parent 4b9c17e546
commit 13c6d411e7
No known key found for this signature in database
GPG key ID: 7A984C8207ADBA51

View file

@ -5,6 +5,8 @@
python3, python3,
fixDarwinDylibNames, fixDarwinDylibNames,
nix-update-script, nix-update-script,
versionCheckHook,
javaBindings ? false, javaBindings ? false,
ocamlBindings ? false, ocamlBindings ? false,
pythonBindings ? true, pythonBindings ? true,
@ -12,11 +14,6 @@
ocaml ? null, ocaml ? null,
findlib ? null, findlib ? null,
zarith ? null, zarith ? null,
versionInfo ? {
regex = "^z3-(4\\.[0-9]+\\.[0-9]+)$";
version = "4.15.0";
hash = "sha256-fk3NyV6vIDXivhiNOW2Y0i5c+kzc7oBqaeBWj/JjpTM=";
},
... ...
}: }:
@ -25,21 +22,21 @@ assert ocamlBindings -> ocaml != null && findlib != null && zarith != null;
stdenv.mkDerivation (finalAttrs: { stdenv.mkDerivation (finalAttrs: {
pname = "z3"; pname = "z3";
inherit (versionInfo) version; version = "4.15.0";
src = fetchFromGitHub { src = fetchFromGitHub {
owner = "Z3Prover"; owner = "Z3Prover";
repo = "z3"; repo = "z3";
rev = "z3-${finalAttrs.version}"; rev = "z3-${finalAttrs.version}";
inherit (versionInfo) hash; hash = "sha256-fk3NyV6vIDXivhiNOW2Y0i5c+kzc7oBqaeBWj/JjpTM=";
}; };
strictDeps = true; strictDeps = true;
nativeBuildInputs = nativeBuildInputs =
[ python3 ] [ python3 ]
++ lib.optional stdenv.hostPlatform.isDarwin fixDarwinDylibNames ++ lib.optionals stdenv.hostPlatform.isDarwin [ fixDarwinDylibNames ]
++ lib.optional javaBindings jdk ++ lib.optionals javaBindings [ jdk ]
++ lib.optionals ocamlBindings [ ++ lib.optionals ocamlBindings [
ocaml ocaml
findlib findlib
@ -52,20 +49,29 @@ stdenv.mkDerivation (finalAttrs: {
mkdir -p $OCAMLFIND_DESTDIR/stublibs mkdir -p $OCAMLFIND_DESTDIR/stublibs
''; '';
configurePhase = configurePhase = ''
lib.concatStringsSep " " ( runHook preConfigure
[ "${python3.pythonOnBuildForHost.interpreter} scripts/mk_make.py --prefix=$out" ]
++ lib.optional javaBindings "--java" ${python3.pythonOnBuildForHost.interpreter} \
++ lib.optional ocamlBindings "--ml" scripts/mk_make.py \
++ lib.optional pythonBindings "--python --pypkgdir=$out/${python3.sitePackages}" --prefix=$out \
) ${lib.optionalString javaBindings "--java"} \
+ "\n" ${lib.optionalString ocamlBindings "--ml"} \
+ "cd build"; ${lib.optionalString pythonBindings "--python --pypkgdir=$out/${python3.sitePackages}"}
cd build
runHook postConfigure
'';
doCheck = true; doCheck = true;
checkPhase = '' checkPhase = ''
runHook preCheck
make -j $NIX_BUILD_CORES test make -j $NIX_BUILD_CORES test
./test-z3 -a ./test-z3 -a
runHook postCheck
''; '';
postInstall = postInstall =
@ -86,9 +92,7 @@ stdenv.mkDerivation (finalAttrs: {
''; '';
doInstallCheck = true; doInstallCheck = true;
installCheckPhase = '' nativeInstallCheckInputs = [ versionCheckHook ];
$out/bin/z3 -version 2>&1 | grep -F "Z3 version $version"
'';
outputs = outputs =
[ [
@ -97,20 +101,15 @@ stdenv.mkDerivation (finalAttrs: {
"dev" "dev"
"python" "python"
] ]
++ lib.optional javaBindings "java" ++ lib.optionals javaBindings [ "java" ]
++ lib.optional ocamlBindings "ocaml"; ++ lib.optionals ocamlBindings [ "ocaml" ];
passthru = { passthru = {
updateScript = nix-update-script { updateScript = nix-update-script {
extraArgs = extraArgs = [
[ "--version-regex"
"--version-regex" "^z3-([0-9]+\\.[0-9]+\\.[0-9]+)$"
versionInfo.regex ];
]
++ lib.optionals (versionInfo.autoUpdate or null != null) [
"--override-filename"
versionInfo.autoUpdate
];
}; };
}; };