diff --git a/nixos/doc/manual/release-notes/rl-2411.section.md b/nixos/doc/manual/release-notes/rl-2411.section.md index cefcb14e1bbb8..49942e8e5f1b2 100644 --- a/nixos/doc/manual/release-notes/rl-2411.section.md +++ b/nixos/doc/manual/release-notes/rl-2411.section.md @@ -928,6 +928,8 @@ - `buildNimSbom` was added as an alternative to `buildNimPackage`. `buildNimSbom` uses [SBOMs](https://cyclonedx.org/) to generate packages whereas `buildNimPackage` uses a custom JSON lockfile format. +- The default version of `z3` has been updated from 4.8 to 4.13. There are still a few packages that need specific 4.8 versions; those will continue to be maintained. + ## Detailed Migration Information {#sec-release-24.11-migration} ### `sound` options removal {#sec-release-24.11-migration-sound} diff --git a/pkgs/applications/science/logic/z3/4-8-5-typos.diff b/pkgs/applications/science/logic/z3/4-8-5-typos.diff new file mode 100644 index 0000000000000..64a4887e0ef4a --- /dev/null +++ b/pkgs/applications/science/logic/z3/4-8-5-typos.diff @@ -0,0 +1,26 @@ +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 index a17cc5561cf21..1c874934adbd0 100644 --- a/pkgs/applications/science/logic/z3/default.nix +++ b/pkgs/applications/science/logic/z3/default.nix @@ -1,107 +1,212 @@ -{ lib -, stdenv -, fetchFromGitHub -, python -, fixDarwinDylibNames -, javaBindings ? false -, ocamlBindings ? false -, pythonBindings ? true -, jdk ? null -, ocaml ? null -, findlib ? null -, zarith ? null -, writeScript +{ + 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" }: - stdenv.mkDerivation rec { - pname = "z3"; - inherit version sha256 patches; - src = fetchFromGitHub { - owner = "Z3Prover"; - repo = "z3"; - rev = "${tag}-${version}"; - sha256 = sha256; - }; +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; + 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; + 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 - ''; + 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" ] + 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"; + ) + + "\n" + + "cd build"; - doCheck = true; - checkPhase = '' - make test - ./test-z3 -a - ''; + 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" - ''; + 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" + ''; - outputs = [ "out" "lib" "dev" "python" ] - ++ lib.optional javaBindings "java" - ++ lib.optional ocamlBindings "ocaml"; + doInstallCheck = true; + installCheckPhase = '' + $out/bin/z3 -version 2>&1 | grep -F "Z3 version $version" + ''; - 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 ]; + 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 { dir = dir; }); in { + z3_4_13 = common { + version = "4.13.4"; + sha256 = "sha256-8hWXCr6IuNVKkOegEmWooo5jkdmln9nU7wI8T882BSE="; + }; z3_4_12 = common { - version = "4.12.5"; - sha256 = "sha256-Qj9w5s02OSMQ2qA7HG7xNqQGaUacA1d4zbOHynq5k+A="; + 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 new file mode 100644 index 0000000000000..254c35be53694 --- /dev/null +++ b/pkgs/applications/science/logic/z3/lower-bound-typo.diff @@ -0,0 +1,13 @@ +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 new file mode 100644 index 0000000000000..4f680e7617d2c --- /dev/null +++ b/pkgs/applications/science/logic/z3/tail-matrix.diff @@ -0,0 +1,12 @@ +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/development/haskell-modules/configuration-common.nix b/pkgs/development/haskell-modules/configuration-common.nix index a62b2f5bc784d..e7c2539c1d32c 100644 --- a/pkgs/development/haskell-modules/configuration-common.nix +++ b/pkgs/development/haskell-modules/configuration-common.nix @@ -1196,6 +1196,21 @@ self: super: { ''; }) super.cryptol; + # Z3 removed aliases for boolean types in 4.12 + inherit ( + let + fixZ3 = appendConfigureFlags [ + "--hsc2hs-option=-DZ3_Bool=bool" + "--hsc2hs-option=-DZ3_TRUE=true" + "--hsc2hs-option=-DZ3_FALSE=false" + ]; + in + { + z3 = fixZ3 super.z3; + hz3 = fixZ3 super.hz3; + } + ) z3 hz3; + # Tests try to invoke external process and process == 1.4 grakn = dontCheck (doJailbreak super.grakn); diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index af8b9319566e4..c2cdaa5b9cdc1 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -17303,12 +17303,12 @@ with pkgs; }; inherit (callPackages ../applications/science/logic/z3 { python = python3; }) + z3_4_13 z3_4_12 z3_4_11 - z3_4_8; - inherit (callPackages ../applications/science/logic/z3 { python = python311; }) + z3_4_8 z3_4_8_5; - z3 = z3_4_8; + z3 = z3_4_13; z3-tptp = callPackage ../applications/science/logic/z3/tptp.nix { }; tlaplus = callPackage ../applications/science/logic/tlaplus {