diff --git a/pkgs/applications/science/logic/z3/4-8-5-typos.diff b/pkgs/applications/science/logic/z3/4-8-5-typos.diff deleted file mode 100644 index 64a4887e0ef4..000000000000 --- a/pkgs/applications/science/logic/z3/4-8-5-typos.diff +++ /dev/null @@ -1,26 +0,0 @@ -diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h -index 4c17df2..4c3c311 100644 ---- a/src/util/lp/lp_core_solver_base.h -+++ b/src/util/lp/lp_core_solver_base.h -@@ -600,8 +600,6 @@ public: - out << " \n"; - } - -- bool column_is_free(unsigned j) const { return this->m_column_type[j] == free; } -- - bool column_has_upper_bound(unsigned j) const { - switch(m_column_types[j]) { - case column_type::free_column: -diff --git a/src/util/lp/static_matrix_def.h b/src/util/lp/static_matrix_def.h -index 7949573..2f1cb42 100644 ---- a/src/util/lp/static_matrix_def.h -+++ b/src/util/lp/static_matrix_def.h -@@ -86,7 +86,7 @@ static_matrix::static_matrix(static_matrix const &A, unsigned * /* basis * - init_row_columns(m, m); - while (m--) { - for (auto & col : A.m_columns[m]){ -- set(col.var(), m, A.get_value_of_column_cell(col)); -+ set(col.var(), m, A.get_column_cell(col)); - } - } - } diff --git a/pkgs/applications/science/logic/z3/default.nix b/pkgs/applications/science/logic/z3/default.nix deleted file mode 100644 index 2152f68fe270..000000000000 --- a/pkgs/applications/science/logic/z3/default.nix +++ /dev/null @@ -1,216 +0,0 @@ -{ - lib, - stdenv, - fetchFromGitHub, - fetchpatch, - python, - fixDarwinDylibNames, - javaBindings ? false, - ocamlBindings ? false, - pythonBindings ? true, - jdk ? null, - ocaml ? null, - findlib ? null, - zarith ? null, - writeScript, - replaceVars, -}: - -assert javaBindings -> jdk != null; -assert ocamlBindings -> ocaml != null && findlib != null && zarith != null; - -let - common = - { - version, - sha256, - patches ? [ ], - tag ? "z3", - doCheck ? true, - }: - stdenv.mkDerivation rec { - pname = "z3"; - inherit version sha256 patches; - src = fetchFromGitHub { - owner = "Z3Prover"; - repo = "z3"; - rev = "${tag}-${version}"; - sha256 = sha256; - }; - - strictDeps = true; - - nativeBuildInputs = - [ python ] - ++ lib.optional stdenv.hostPlatform.isDarwin fixDarwinDylibNames - ++ lib.optional javaBindings jdk - ++ lib.optionals ocamlBindings [ - ocaml - findlib - ]; - propagatedBuildInputs = [ python.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 - '' - + - lib.optionalString - ((lib.versionAtLeast python.version "3.12") && (lib.versionOlder version "4.8.14")) - '' - # See https://github.com/Z3Prover/z3/pull/5729. This is a specialization of this patch for 4.8.5. - for file in scripts/mk_util.py src/api/python/CMakeLists.txt; do - substituteInPlace "$file" \ - --replace-fail "distutils.sysconfig.get_python_lib()" "sysconfig.get_path('purelib')" \ - --replace-fail "distutils.sysconfig" "sysconfig" - done - ''; - - configurePhase = - lib.concatStringsSep " " ( - [ "${python.pythonOnBuildForHost.interpreter} scripts/mk_make.py --prefix=$out" ] - ++ lib.optional javaBindings "--java" - ++ lib.optional ocamlBindings "--ml" - ++ lib.optional pythonBindings "--python --pypkgdir=$out/${python.sitePackages}" - ) - + "\n" - + "cd build"; - - inherit doCheck; - 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/${python.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"; - - meta = with lib; { - 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-${version}"; - license = licenses.mit; - platforms = platforms.unix; - maintainers = with maintainers; [ - thoughtpolice - ttuegel - numinit - ]; - }; - }; - - static-matrix-def-patch = fetchpatch { - # clang / gcc fixes. fixes typos in some member names - name = "gcc-15-fixes.patch"; - url = "https://github.com/Z3Prover/z3/commit/2ce89e5f491fa817d02d8fdce8c62798beab258b.patch"; - includes = [ "src/math/lp/static_matrix_def.h" ]; - hash = "sha256-rEH+UzylzyhBdtx65uf8QYj5xwuXOyG6bV/4jgKkXGo="; - }; - - static-matrix-patch = fetchpatch { - # clang / gcc fixes. fixes typos in some member names - name = "gcc-15-fixes.patch"; - url = "https://github.com/Z3Prover/z3/commit/2ce89e5f491fa817d02d8fdce8c62798beab258b.patch"; - includes = [ "src/@dir@/lp/static_matrix.h" ]; - stripLen = 3; - extraPrefix = "src/@dir@/"; - hash = "sha256-+H1/VJPyI0yq4M/61ay8SRCa6OaoJ/5i+I3zVTAPUVo="; - }; - - # replace @dir@ in the path of the given list of patches - fixupPatches = dir: map (patch: replaceVars patch { inherit dir; }); -in -{ - z3_4_14 = common { - version = "4.14.1"; - sha256 = "sha256-pTsDzf6Frk4mYAgF81wlR5Kb1x56joFggO5Fa3G2s70="; - }; - z3_4_13 = common { - version = "4.13.4"; - sha256 = "sha256-8hWXCr6IuNVKkOegEmWooo5jkdmln9nU7wI8T882BSE="; - }; - z3_4_12 = common { - version = "4.12.6"; - sha256 = "sha256-X4wfPWVSswENV0zXJp/5u9SQwGJWocLKJ/CNv57Bt+E="; - patches = - fixupPatches "math" [ - ./lower-bound-typo.diff - static-matrix-patch - ] - ++ [ - static-matrix-def-patch - ]; - }; - z3_4_11 = common { - version = "4.11.2"; - sha256 = "sha256-OO0wtCvSKwGxnKvu+AfXe4mEzv4nofa7A00BjX+KVjc="; - patches = - fixupPatches "math" [ - ./lower-bound-typo.diff - static-matrix-patch - ./tail-matrix.diff - ] - ++ [ - static-matrix-def-patch - ]; - }; - z3_4_8 = common { - version = "4.8.17"; - sha256 = "sha256-BSwjgOU9EgCcm18Zx0P9mnoPc9ZeYsJwEu0ffnACa+8="; - patches = - fixupPatches "math" [ - ./lower-bound-typo.diff - static-matrix-patch - ./tail-matrix.diff - ] - ++ [ - static-matrix-def-patch - ]; - }; - z3_4_8_5 = common { - tag = "Z3"; - version = "4.8.5"; - sha256 = "sha256-ytG5O9HczbIVJAiIGZfUXC/MuYH7d7yLApaeTRlKXoc="; - patches = - fixupPatches "util" [ - ./lower-bound-typo.diff - static-matrix-patch - ./tail-matrix.diff - ] - ++ [ - ./4-8-5-typos.diff - ]; - }; -} diff --git a/pkgs/applications/science/logic/z3/lower-bound-typo.diff b/pkgs/applications/science/logic/z3/lower-bound-typo.diff deleted file mode 100644 index 254c35be5369..000000000000 --- a/pkgs/applications/science/logic/z3/lower-bound-typo.diff +++ /dev/null @@ -1,13 +0,0 @@ -diff --git a/src/@dir@/lp/column_info.h b/src/@dir@/lp/column_info.h -index 1dc0c60..9cbeea6 100644 ---- a/src/@dir@/lp/column_info.h -+++ b/src/@dir@/lp/column_info.h -@@ -47,7 +47,7 @@ public: - m_lower_bound_is_strict == c.m_lower_bound_is_strict && - m_upper_bound_is_set == c.m_upper_bound_is_set&& - m_upper_bound_is_strict == c.m_upper_bound_is_strict&& -- (!m_lower_bound_is_set || m_lower_bound == c.m_low_bound) && -+ (!m_lower_bound_is_set || m_lower_bound == c.m_lower_bound) && - (!m_upper_bound_is_set || m_upper_bound == c.m_upper_bound) && - m_cost == c.m_cost && - m_is_fixed == c.m_is_fixed && diff --git a/pkgs/applications/science/logic/z3/tail-matrix.diff b/pkgs/applications/science/logic/z3/tail-matrix.diff deleted file mode 100644 index 4f680e7617d2..000000000000 --- a/pkgs/applications/science/logic/z3/tail-matrix.diff +++ /dev/null @@ -1,12 +0,0 @@ -diff --git a/src/@dir@/lp/tail_matrix.h b/src/@dir@/lp/tail_matrix.h -index 2047e8c..c84340e 100644 ---- a/src/@dir@/lp/tail_matrix.h -+++ b/src/@dir@/lp/tail_matrix.h -@@ -43,7 +43,6 @@ public: - const tail_matrix & m_A; - unsigned m_row; - ref_row(const tail_matrix& m, unsigned row): m_A(m), m_row(row) {} -- T operator[](unsigned j) const { return m_A.get_elem(m_row, j);} - }; - ref_row operator[](unsigned i) const { return ref_row(*this, i);} - }; diff --git a/pkgs/applications/science/logic/z3/tptp.nix b/pkgs/by-name/z3/z3-tptp/package.nix similarity index 90% rename from pkgs/applications/science/logic/z3/tptp.nix rename to pkgs/by-name/z3/z3-tptp/package.nix index 8e1da19c6008..b7ab814255b3 100644 --- a/pkgs/applications/science/logic/z3/tptp.nix +++ b/pkgs/by-name/z3/z3-tptp/package.nix @@ -30,6 +30,6 @@ stdenv.mkDerivation rec { meta = { inherit (z3.meta) license homepage platforms; description = "TPTP wrapper for Z3 prover"; - maintainers = [ lib.maintainers.raskin ]; + maintainers = z3.meta.maintainers ++ [ lib.maintainers.raskin ]; }; } diff --git a/pkgs/by-name/z3/z3/package.nix b/pkgs/by-name/z3/z3/package.nix new file mode 100644 index 000000000000..cc80e0151581 --- /dev/null +++ b/pkgs/by-name/z3/z3/package.nix @@ -0,0 +1,6 @@ +{ + z3_4_14, + ... +}@args: + +z3_4_14.override args diff --git a/pkgs/by-name/z3/z3_4_14/package.nix b/pkgs/by-name/z3/z3_4_14/package.nix new file mode 100644 index 000000000000..60339b94e30f --- /dev/null +++ b/pkgs/by-name/z3/z3_4_14/package.nix @@ -0,0 +1,130 @@ +{ + 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 + ]; + }; +}) diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index b6d147cebaa3..8a849090ac98 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -18133,17 +18133,6 @@ with pkgs; gmp-static = gmp.override { withStatic = true; }; }; - inherit (callPackages ../applications/science/logic/z3 { python = python3; }) - z3_4_14 - z3_4_13 - z3_4_12 - z3_4_11 - z3_4_8 - z3_4_8_5 - ; - z3 = z3_4_13; - z3-tptp = callPackage ../applications/science/logic/z3/tptp.nix { }; - tlaplus = callPackage ../applications/science/logic/tlaplus { jre = jre8; # TODO: remove override https://github.com/NixOS/nixpkgs/pull/89731 }; diff --git a/pkgs/top-level/python-packages.nix b/pkgs/top-level/python-packages.nix index 2fc8a1aaa565..23bce3243eca 100644 --- a/pkgs/top-level/python-packages.nix +++ b/pkgs/top-level/python-packages.nix @@ -19224,12 +19224,7 @@ self: super: with self; { yubico-client = callPackage ../development/python-modules/yubico-client { }; - z3-solver = - (toPythonModule ( - (pkgs.z3.override { inherit python; }).overrideAttrs (_: { - pname = "z3-solver"; - }) - )).python; + z3-solver = (toPythonModule (pkgs.z3.override { python3 = python; })).python; z3c-checkversions = callPackage ../development/python-modules/z3c-checkversions { };