mirror of
https://github.com/NixOS/nixpkgs.git
synced 2025-06-09 19:13:26 +03:00
z3_4_15: rename to z3
This commit is contained in:
Tom van Dijk
parent
60cbd81553
commit
4b9c17e546
3 changed files with 133 additions and 141 deletions
|
|
@ -1,8 +1,130 @@
|
|||
# Note: when updating to a new major version (for now), add an alias to
|
||||
# pkgs/top-level/aliases.nix
|
||||
{
|
||||
z3_4_15,
|
||||
lib,
|
||||
stdenv,
|
||||
fetchFromGitHub,
|
||||
python3,
|
||||
fixDarwinDylibNames,
|
||||
nix-update-script,
|
||||
javaBindings ? false,
|
||||
ocamlBindings ? false,
|
||||
pythonBindings ? true,
|
||||
jdk ? null,
|
||||
ocaml ? null,
|
||||
findlib ? null,
|
||||
zarith ? null,
|
||||
versionInfo ? {
|
||||
regex = "^z3-(4\\.[0-9]+\\.[0-9]+)$";
|
||||
version = "4.15.0";
|
||||
hash = "sha256-fk3NyV6vIDXivhiNOW2Y0i5c+kzc7oBqaeBWj/JjpTM=";
|
||||
},
|
||||
...
|
||||
}@args:
|
||||
}:
|
||||
|
||||
z3_4_15.override args
|
||||
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
|
||||
];
|
||||
};
|
||||
})
|
||||
|
|
|
|||
|
|
@ -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 = "^z3-(4\\.[0-9]+\\.[0-9]+)$";
|
||||
version = "4.15.0";
|
||||
hash = "sha256-fk3NyV6vIDXivhiNOW2Y0i5c+kzc7oBqaeBWj/JjpTM=";
|
||||
},
|
||||
...
|
||||
}:
|
||||
|
||||
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
|
||||
];
|
||||
};
|
||||
})
|
||||
|
|
@ -2032,12 +2032,12 @@ mapAliases {
|
|||
|
||||
### Z ###
|
||||
|
||||
z3_4_11 = throw "'z3_4_11' has been removed in favour of the latest version. Consider using 'z3' or 'z3_4_15'."; # Added 2025-05-17
|
||||
z3_4_12 = throw "'z3_4_12' has been removed in favour of the latest version. Consider using 'z3' or 'z3_4_15'."; # Added 2025-05-17
|
||||
z3_4_13 = throw "'z3_4_13' has been removed in favour of the latest version. Consider using 'z3' or 'z3_4_15'."; # Added 2025-05-17
|
||||
z3_4_14 = throw "'z3_4_14' has been removed in favour of the latest version. Consider using 'z3' or 'z3_4_15'."; # Added 2025-05-17
|
||||
z3_4_8_5 = throw "'z3_4_8_5' has been removed in favour of the latest version. Consider using 'z3' or 'z3_4_15'."; # Added 2025-05-17
|
||||
z3_4_8 = throw "'z3_4_8' has been removed in favour of the latest version. Consider using 'z3' or 'z3_4_15'."; # Added 2025-05-17
|
||||
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 {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue