1
0
Fork 0
forked from NixOS/nixpkgs

z3: 4.14.1 → 4.15.0, z3_4_14: drop (#407728)

This commit is contained in:
Morgan Jones 2025-05-22 04:46:07 -07:00 committed by GitHub
commit 1e51989132
Signed by: github
GPG key ID: B5690EEEBB952194
4 changed files with 134 additions and 135 deletions

View file

@ -272,7 +272,7 @@
- `nodePackages.meshcommander` has been removed, as the package was deprecated by Intel.
- The default version of `z3` has been updated from 4.8 to 4.14, and all old versions have been dropped. Note that `fstar` still depends on specific versions, and maintains them as overrides.
- The default version of `z3` has been updated from 4.8 to 4.15, and all old versions have been dropped. Note that `fstar` still depends on specific versions, and maintains them as overrides.
- `prometheus` has been updated from 2.55.0 to 3.1.0.
Read the [release blog post](https://prometheus.io/blog/2024/11/14/prometheus-3-0/) and

View file

@ -1,6 +1,129 @@
{
z3_4_14,
...
}@args:
lib,
stdenv,
fetchFromGitHub,
python3,
fixDarwinDylibNames,
nix-update-script,
versionCheckHook,
z3_4_14.override args
javaBindings ? false,
ocamlBindings ? false,
pythonBindings ? true,
jdk ? null,
ocaml ? null,
findlib ? null,
zarith ? null,
...
}:
assert javaBindings -> jdk != null;
assert ocamlBindings -> ocaml != null && findlib != null && zarith != null;
stdenv.mkDerivation (finalAttrs: {
pname = "z3";
version = "4.15.0";
src = fetchFromGitHub {
owner = "Z3Prover";
repo = "z3";
rev = "z3-${finalAttrs.version}";
hash = "sha256-fk3NyV6vIDXivhiNOW2Y0i5c+kzc7oBqaeBWj/JjpTM=";
};
strictDeps = true;
nativeBuildInputs =
[ python3 ]
++ lib.optionals stdenv.hostPlatform.isDarwin [ fixDarwinDylibNames ]
++ lib.optionals javaBindings [ jdk ]
++ lib.optionals ocamlBindings [
ocaml
findlib
];
propagatedBuildInputs = [ python3.pkgs.setuptools ] ++ lib.optionals ocamlBindings [ zarith ];
enableParallelBuilding = true;
postPatch = lib.optionalString ocamlBindings ''
export OCAMLFIND_DESTDIR=$ocaml/lib/ocaml/${ocaml.version}/site-lib
mkdir -p $OCAMLFIND_DESTDIR/stublibs
'';
configurePhase = ''
runHook preConfigure
${python3.pythonOnBuildForHost.interpreter} \
scripts/mk_make.py \
--prefix=$out \
${lib.optionalString javaBindings "--java"} \
${lib.optionalString ocamlBindings "--ml"} \
${lib.optionalString pythonBindings "--python --pypkgdir=$out/${python3.sitePackages}"}
cd build
runHook postConfigure
'';
doCheck = true;
checkPhase = ''
runHook preCheck
make -j $NIX_BUILD_CORES test
./test-z3 -a
runHook postCheck
'';
postInstall =
''
mkdir -p $dev $lib
mv $out/lib $lib/lib
mv $out/include $dev/include
''
+ lib.optionalString pythonBindings ''
mkdir -p $python/lib
mv $lib/lib/python* $python/lib/
ln -sf $lib/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary} $python/${python3.sitePackages}/z3/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary}
''
+ lib.optionalString javaBindings ''
mkdir -p $java/share/java
mv com.microsoft.z3.jar $java/share/java
moveToOutput "lib/libz3java.${stdenv.hostPlatform.extensions.sharedLibrary}" "$java"
'';
doInstallCheck = true;
nativeInstallCheckInputs = [ versionCheckHook ];
outputs =
[
"out"
"lib"
"dev"
"python"
]
++ lib.optionals javaBindings [ "java" ]
++ lib.optionals ocamlBindings [ "ocaml" ];
passthru = {
updateScript = nix-update-script {
extraArgs = [
"--version-regex"
"^z3-([0-9]+\\.[0-9]+\\.[0-9]+)$"
];
};
};
meta = {
description = "High-performance theorem prover and SMT solver";
mainProgram = "z3";
homepage = "https://github.com/Z3Prover/z3";
changelog = "https://github.com/Z3Prover/z3/releases/tag/z3-${finalAttrs.version}";
license = lib.licenses.mit;
platforms = lib.platforms.unix;
maintainers = with lib.maintainers; [
thoughtpolice
ttuegel
numinit
];
};
})

View file

@ -1,130 +0,0 @@
{
lib,
stdenv,
fetchFromGitHub,
python3,
fixDarwinDylibNames,
nix-update-script,
javaBindings ? false,
ocamlBindings ? false,
pythonBindings ? true,
jdk ? null,
ocaml ? null,
findlib ? null,
zarith ? null,
versionInfo ? {
regex = "^v(4\\.14\\.[0-9]+)$";
version = "4.14.1";
hash = "sha256-pTsDzf6Frk4mYAgF81wlR5Kb1x56joFggO5Fa3G2s70=";
},
...
}:
assert javaBindings -> jdk != null;
assert ocamlBindings -> ocaml != null && findlib != null && zarith != null;
stdenv.mkDerivation (finalAttrs: {
pname = "z3";
inherit (versionInfo) version;
src = fetchFromGitHub {
owner = "Z3Prover";
repo = "z3";
rev = "z3-${finalAttrs.version}";
inherit (versionInfo) hash;
};
strictDeps = true;
nativeBuildInputs =
[ python3 ]
++ lib.optional stdenv.hostPlatform.isDarwin fixDarwinDylibNames
++ lib.optional javaBindings jdk
++ lib.optionals ocamlBindings [
ocaml
findlib
];
propagatedBuildInputs = [ python3.pkgs.setuptools ] ++ lib.optionals ocamlBindings [ zarith ];
enableParallelBuilding = true;
postPatch = lib.optionalString ocamlBindings ''
export OCAMLFIND_DESTDIR=$ocaml/lib/ocaml/${ocaml.version}/site-lib
mkdir -p $OCAMLFIND_DESTDIR/stublibs
'';
configurePhase =
lib.concatStringsSep " " (
[ "${python3.pythonOnBuildForHost.interpreter} scripts/mk_make.py --prefix=$out" ]
++ lib.optional javaBindings "--java"
++ lib.optional ocamlBindings "--ml"
++ lib.optional pythonBindings "--python --pypkgdir=$out/${python3.sitePackages}"
)
+ "\n"
+ "cd build";
doCheck = true;
checkPhase = ''
make -j $NIX_BUILD_CORES test
./test-z3 -a
'';
postInstall =
''
mkdir -p $dev $lib
mv $out/lib $lib/lib
mv $out/include $dev/include
''
+ lib.optionalString pythonBindings ''
mkdir -p $python/lib
mv $lib/lib/python* $python/lib/
ln -sf $lib/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary} $python/${python3.sitePackages}/z3/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary}
''
+ lib.optionalString javaBindings ''
mkdir -p $java/share/java
mv com.microsoft.z3.jar $java/share/java
moveToOutput "lib/libz3java.${stdenv.hostPlatform.extensions.sharedLibrary}" "$java"
'';
doInstallCheck = true;
installCheckPhase = ''
$out/bin/z3 -version 2>&1 | grep -F "Z3 version $version"
'';
outputs =
[
"out"
"lib"
"dev"
"python"
]
++ lib.optional javaBindings "java"
++ lib.optional ocamlBindings "ocaml";
passthru = {
updateScript = nix-update-script {
extraArgs =
[
"--version-regex"
versionInfo.regex
]
++ lib.optionals (versionInfo.autoUpdate or null != null) [
"--override-filename"
versionInfo.autoUpdate
];
};
};
meta = {
description = "High-performance theorem prover and SMT solver";
mainProgram = "z3";
homepage = "https://github.com/Z3Prover/z3";
changelog = "https://github.com/Z3Prover/z3/releases/tag/z3-${finalAttrs.version}";
license = lib.licenses.mit;
platforms = lib.platforms.unix;
maintainers = with lib.maintainers; [
thoughtpolice
ttuegel
numinit
];
};
})

View file

@ -2092,6 +2092,12 @@ mapAliases {
### Z ###
z3_4_11 = throw "'z3_4_11' has been removed in favour of the latest version. Use 'z3'."; # Added 2025-05-18
z3_4_12 = throw "'z3_4_12' has been removed in favour of the latest version. Use 'z3'."; # Added 2025-05-18
z3_4_13 = throw "'z3_4_13' has been removed in favour of the latest version. Use 'z3'."; # Added 2025-05-18
z3_4_14 = throw "'z3_4_14' has been removed in favour of the latest version. Use 'z3'."; # Added 2025-05-18
z3_4_8_5 = throw "'z3_4_8_5' has been removed in favour of the latest version. Use 'z3'."; # Added 2025-05-18
z3_4_8 = throw "'z3_4_8' has been removed in favour of the latest version. Use 'z3'."; # Added 2025-05-18
zabbix50 = throw "'zabbix50' has been removed, it would have reached its End of Life a few days after the release of NixOS 25.05. Consider upgrading to 'zabbix60' or 'zabbix70'.";
zabbix64 = throw "'zabbix64' has been removed because it reached its End of Life. Consider upgrading to 'zabbix70'.";
zeroadPackages = recurseIntoAttrs {