z3: 4.8.17 -> 4.13.4; z3_4_12: 4.12.5 -> 4.12.6 (#327052)

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}

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<T, X>::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));
+         }
+     }
+ }

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
+      ];
   };
 }

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 &&

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);}
+ };

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);
 

pkgs/top-level/all-packages.nix

@@ -17266,12 +17266,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 {