From f9d66c36aaf338217f325797578a52b28dd464f8 Mon Sep 17 00:00:00 2001
From: Tom van Dijk <18gatenmaker6@gmail.com>
Date: Fri, 16 May 2025 22:59:25 +0200
Subject: [PATCH 1/5] =?UTF-8?q?z3:=204.14.1=20=E2=86=92=204.15.0,=20z3=5F4?=
 =?UTF-8?q?=5F14:=20drop,=20z3=5F4=5F15:=20init=20at=204.15.0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 pkgs/by-name/z3/z3/package.nix                   | 4 ++--
 pkgs/by-name/z3/{z3_4_14 => z3_4_15}/package.nix | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)
 rename pkgs/by-name/z3/{z3_4_14 => z3_4_15}/package.nix (96%)

diff --git a/pkgs/by-name/z3/z3/package.nix b/pkgs/by-name/z3/z3/package.nix
index cc80e0151581..62432394bb0b 100644
--- a/pkgs/by-name/z3/z3/package.nix
+++ b/pkgs/by-name/z3/z3/package.nix
@@ -1,6 +1,6 @@
 {
-  z3_4_14,
+  z3_4_15,
   ...
 }@args:
 
-z3_4_14.override args
+z3_4_15.override args
diff --git a/pkgs/by-name/z3/z3_4_14/package.nix b/pkgs/by-name/z3/z3_4_15/package.nix
similarity index 96%
rename from pkgs/by-name/z3/z3_4_14/package.nix
rename to pkgs/by-name/z3/z3_4_15/package.nix
index 60339b94e30f..d080b8247720 100644
--- a/pkgs/by-name/z3/z3_4_14/package.nix
+++ b/pkgs/by-name/z3/z3_4_15/package.nix
@@ -13,9 +13,9 @@
   findlib ? null,
   zarith ? null,
   versionInfo ? {
-    regex = "^v(4\\.14\\.[0-9]+)$";
-    version = "4.14.1";
-    hash = "sha256-pTsDzf6Frk4mYAgF81wlR5Kb1x56joFggO5Fa3G2s70=";
+    regex = "^z3-(4\\.[0-9]+\\.[0-9]+)$";
+    version = "4.15.0";
+    hash = "sha256-fk3NyV6vIDXivhiNOW2Y0i5c+kzc7oBqaeBWj/JjpTM=";
   },
   ...
 }:

From 60cbd815539f8aa7b3d7f96ff41f8ee8d2f328e8 Mon Sep 17 00:00:00 2001
From: Tom van Dijk <18gatenmaker6@gmail.com>
Date: Sat, 17 May 2025 15:31:18 +0200
Subject: [PATCH 2/5] z3: add aliases for older versions

---
 pkgs/by-name/z3/z3/package.nix | 2 ++
 pkgs/top-level/aliases.nix     | 6 ++++++
 2 files changed, 8 insertions(+)

diff --git a/pkgs/by-name/z3/z3/package.nix b/pkgs/by-name/z3/z3/package.nix
index 62432394bb0b..035f1fe926bd 100644
--- a/pkgs/by-name/z3/z3/package.nix
+++ b/pkgs/by-name/z3/z3/package.nix
@@ -1,3 +1,5 @@
+# Note: when updating to a new major version (for now), add an alias to
+# pkgs/top-level/aliases.nix
 {
   z3_4_15,
   ...
diff --git a/pkgs/top-level/aliases.nix b/pkgs/top-level/aliases.nix
index 3a439c5a67c6..7a7516ccff61 100644
--- a/pkgs/top-level/aliases.nix
+++ b/pkgs/top-level/aliases.nix
@@ -2032,6 +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
   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 {

From 4b9c17e546a18eeffb0182e95c6d1fbf80cf8720 Mon Sep 17 00:00:00 2001
From: Tom van Dijk <18gatenmaker6@gmail.com>
Date: Sun, 18 May 2025 12:58:39 +0200
Subject: [PATCH 3/5] z3_4_15: rename to z3

---
 pkgs/by-name/z3/z3/package.nix      | 132 ++++++++++++++++++++++++++--
 pkgs/by-name/z3/z3_4_15/package.nix | 130 ---------------------------
 pkgs/top-level/aliases.nix          |  12 +--
 3 files changed, 133 insertions(+), 141 deletions(-)
 delete mode 100644 pkgs/by-name/z3/z3_4_15/package.nix

diff --git a/pkgs/by-name/z3/z3/package.nix b/pkgs/by-name/z3/z3/package.nix
index 035f1fe926bd..d080b8247720 100644
--- a/pkgs/by-name/z3/z3/package.nix
+++ b/pkgs/by-name/z3/z3/package.nix
@@ -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
+    ];
+  };
+})
diff --git a/pkgs/by-name/z3/z3_4_15/package.nix b/pkgs/by-name/z3/z3_4_15/package.nix
deleted file mode 100644
index d080b8247720..000000000000
--- a/pkgs/by-name/z3/z3_4_15/package.nix
+++ /dev/null
@@ -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
-    ];
-  };
-})
diff --git a/pkgs/top-level/aliases.nix b/pkgs/top-level/aliases.nix
index 7a7516ccff61..2cd7990ed623 100644
--- a/pkgs/top-level/aliases.nix
+++ b/pkgs/top-level/aliases.nix
@@ -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 {

From 13c6d411e70ec7f7e17d4ab37c121cdb8187ef71 Mon Sep 17 00:00:00 2001
From: Tom van Dijk <18gatenmaker6@gmail.com>
Date: Wed, 21 May 2025 20:20:40 +0200
Subject: [PATCH 4/5] z3: refactor

---
 pkgs/by-name/z3/z3/package.nix | 63 +++++++++++++++++-----------------
 1 file changed, 31 insertions(+), 32 deletions(-)

diff --git a/pkgs/by-name/z3/z3/package.nix b/pkgs/by-name/z3/z3/package.nix
index d080b8247720..3883b4d3840e 100644
--- a/pkgs/by-name/z3/z3/package.nix
+++ b/pkgs/by-name/z3/z3/package.nix
@@ -5,6 +5,8 @@
   python3,
   fixDarwinDylibNames,
   nix-update-script,
+  versionCheckHook,
+
   javaBindings ? false,
   ocamlBindings ? false,
   pythonBindings ? true,
@@ -12,11 +14,6 @@
   ocaml ? null,
   findlib ? null,
   zarith ? null,
-  versionInfo ? {
-    regex = "^z3-(4\\.[0-9]+\\.[0-9]+)$";
-    version = "4.15.0";
-    hash = "sha256-fk3NyV6vIDXivhiNOW2Y0i5c+kzc7oBqaeBWj/JjpTM=";
-  },
   ...
 }:
 
@@ -25,21 +22,21 @@ assert ocamlBindings -> ocaml != null && findlib != null && zarith != null;
 
 stdenv.mkDerivation (finalAttrs: {
   pname = "z3";
-  inherit (versionInfo) version;
+  version = "4.15.0";
 
   src = fetchFromGitHub {
     owner = "Z3Prover";
     repo = "z3";
     rev = "z3-${finalAttrs.version}";
-    inherit (versionInfo) hash;
+    hash = "sha256-fk3NyV6vIDXivhiNOW2Y0i5c+kzc7oBqaeBWj/JjpTM=";
   };
 
   strictDeps = true;
 
   nativeBuildInputs =
     [ python3 ]
-    ++ lib.optional stdenv.hostPlatform.isDarwin fixDarwinDylibNames
-    ++ lib.optional javaBindings jdk
+    ++ lib.optionals stdenv.hostPlatform.isDarwin [ fixDarwinDylibNames ]
+    ++ lib.optionals javaBindings [ jdk ]
     ++ lib.optionals ocamlBindings [
       ocaml
       findlib
@@ -52,20 +49,29 @@ stdenv.mkDerivation (finalAttrs: {
     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";
+  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 =
@@ -86,9 +92,7 @@ stdenv.mkDerivation (finalAttrs: {
     '';
 
   doInstallCheck = true;
-  installCheckPhase = ''
-    $out/bin/z3 -version 2>&1 | grep -F "Z3 version $version"
-  '';
+  nativeInstallCheckInputs = [ versionCheckHook ];
 
   outputs =
     [
@@ -97,20 +101,15 @@ stdenv.mkDerivation (finalAttrs: {
       "dev"
       "python"
     ]
-    ++ lib.optional javaBindings "java"
-    ++ lib.optional ocamlBindings "ocaml";
+    ++ lib.optionals javaBindings [ "java" ]
+    ++ lib.optionals ocamlBindings [ "ocaml" ];
 
   passthru = {
     updateScript = nix-update-script {
-      extraArgs =
-        [
-          "--version-regex"
-          versionInfo.regex
-        ]
-        ++ lib.optionals (versionInfo.autoUpdate or null != null) [
-          "--override-filename"
-          versionInfo.autoUpdate
-        ];
+      extraArgs = [
+        "--version-regex"
+        "^z3-([0-9]+\\.[0-9]+\\.[0-9]+)$"
+      ];
     };
   };
 

From fa2bee6de36a6da85b23907a0b1d4f89cc90116b Mon Sep 17 00:00:00 2001
From: Tom van Dijk <18gatenmaker6@gmail.com>
Date: Wed, 21 May 2025 20:27:34 +0200
Subject: [PATCH 5/5] doc: rl-2505: z3 4.14 -> 4.15

---
 doc/release-notes/rl-2505.section.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/release-notes/rl-2505.section.md b/doc/release-notes/rl-2505.section.md
index afa4d0e3474e..6c3ac618e5e4 100644
--- a/doc/release-notes/rl-2505.section.md
+++ b/doc/release-notes/rl-2505.section.md
@@ -270,7 +270,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