Unverified Commit 64ac770c authored by Morgan Jones's avatar Morgan Jones Committed by GitHub
Browse files

[Backport release-25.05] z3: 4.14.1 → 4.15.0, z3_4_14: drop (#409741)

parents cd4df48f c8c8dadc

doc/release-notes/rl-2505.section.md

+1 −1
Original line number Diff line number Diff line
@@ -272,7 +272,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

pkgs/by-name/z3/z3/package.nix

+126 −3
Original line number Diff line number Diff line 
{

  z3_4_14,

  lib,

  stdenv,

  fetchFromGitHub,

  python3,

  fixDarwinDylibNames,

  nix-update-script,

  versionCheckHook,



  javaBindings ? false,

  ocamlBindings ? false,

  pythonBindings ? true,

  jdk ? null,

  ocaml ? null,

  findlib ? null,

  zarith ? null,

  ...

}@args:

}:



assert javaBindings -> jdk != null;

assert ocamlBindings -> ocaml != null && findlib != null && zarith != null;



stdenv.mkDerivation (finalAttrs: {

  pname = "z3";

  version = "4.15.0";



  src = fetchFromGitHub {

    owner = "Z3Prover";

    repo = "z3";

    rev = "z3-${finalAttrs.version}";

    hash = "sha256-fk3NyV6vIDXivhiNOW2Y0i5c+kzc7oBqaeBWj/JjpTM=";

  };



  strictDeps = true;



  nativeBuildInputs =

    [ python3 ]

    ++ lib.optionals stdenv.hostPlatform.isDarwin [ fixDarwinDylibNames ]

    ++ lib.optionals 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 = ''

    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 =

    ''

      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;

  nativeInstallCheckInputs = [ versionCheckHook ];



  outputs =

    [

      "out"

      "lib"

      "dev"

      "python"

    ]

    ++ lib.optionals javaBindings [ "java" ]

    ++ lib.optionals ocamlBindings [ "ocaml" ];



  passthru = {

    updateScript = nix-update-script {

      extraArgs = [

        "--version-regex"

        "^z3-([0-9]+\\.[0-9]+\\.[0-9]+)$"

      ];

    };

  };



z3_4_14.override args
 
  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

    ];

  };

})

pkgs/by-name/z3/z3_4_14/package.nix

deleted100644 → 0
+0 −130
Original line number Diff line number Diff line 
{

  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

    ];

  };

})

pkgs/top-level/aliases.nix

+6 −0
Original line number Diff line number Diff line
@@ -2058,6 +2058,12 @@ mapAliases { 


  ### Z ###



  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 {