Merge pull request #1041 from pq-code-package/nix25.05

hanno-becker · web-flow · commit 70d8d8932711 · 2025-05-24T08:23:56.000+01:00
Update to nixpkgs 25.05
diff --git a/.github/workflows/all.yml b/.github/workflows/all.yml
@@ -40,7 +40,7 @@ jobs:
     permissions:
       contents: 'read'
       id-token: 'write'
-    needs: [ base ]
+    needs: [ base, nix ]
     uses: ./.github/workflows/cbmc.yml
     secrets: inherit
   oqs_integration:
@@ -76,14 +76,14 @@ jobs:
     permissions:
       contents: 'read'
       id-token: 'write'
-    needs: [ base ]
+    needs: [ base, nix ]
     uses: ./.github/workflows/ct-tests.yml
     secrets: inherit
   slothy:
     name: SLOTHY
     permissions:
       contents: 'read'
       id-token: 'write'
-    needs: [ base ]
+    needs: [ base, nix ]
     uses: ./.github/workflows/slothy.yml
     secrets: inherit
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -252,6 +252,13 @@ jobs:
            c23: False
            examples: False
            opt: no_opt
+         - name: zig-0.14
+           shell: ci_zig0_14
+           darwin: True
+           c17: True
+           c23: True
+           examples: False
+           opt: no_opt
     runs-on: ${{ matrix.target.runner }}
     steps:
       - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -5,7 +5,7 @@
 
   inputs = {
     nixpkgs-2405.url = "github:NixOS/nixpkgs/nixos-24.05";
-    nixpkgs.url = "github:NixOS/nixpkgs/nixos-24.11";
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-25.05";
     nixpkgs-unstable.url = "github:NixOS/nixpkgs/nixos-unstable";
 
     flake-parts = {
@@ -23,9 +23,10 @@
           pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.${system};
           pkgs-2405 = inputs.nixpkgs-2405.legacyPackages.${system};
           util = pkgs.callPackage ./nix/util.nix {
+            # Keep those around in case we want to switch to unstable versions
             cbmc = pkgs.cbmc;
-            bitwuzla = pkgs-unstable.bitwuzla;
-            z3 = pkgs-unstable.z3_4_14;
+            bitwuzla = pkgs.bitwuzla;
+            z3 = pkgs.z3;
           };
           zigWrapCC = zig: pkgs.symlinkJoin {
             name = "zig-wrappers";
@@ -48,8 +49,9 @@
               (_:_: {
                 gcc48 = pkgs-2405.gcc48;
                 gcc49 = pkgs-2405.gcc49;
-                qemu = pkgs-unstable.qemu; # 9.2.2
-                clang_20 = pkgs-unstable.clang_20;
+                gcc7 = pkgs-2405.gcc7;
+                zig_0_10 = pkgs-2405.zig_0_10;
+                zig_0_11 = pkgs-2405.zig_0_11;
               })
             ];
           };
@@ -109,6 +111,7 @@
           devShells.ci_zig0_11 = util.mkShellWithCC' (zigWrapCC pkgs.zig_0_11);
           devShells.ci_zig0_12 = util.mkShellWithCC' (zigWrapCC pkgs.zig_0_12);
           devShells.ci_zig0_13 = util.mkShellWithCC' (zigWrapCC pkgs.zig_0_13);
+          devShells.ci_zig0_14 = util.mkShellWithCC' (zigWrapCC pkgs.zig);
 
           devShells.ci_gcc48 = util.mkShellWithCC' pkgs.gcc48;
           devShells.ci_gcc49 = util.mkShellWithCC' pkgs.gcc49;
@@ -142,8 +145,8 @@
             util = pkgs.callPackage ./nix/util.nix {
               inherit pkgs;
               cbmc = pkgs.cbmc;
-              bitwuzla = pkgs-unstable.bitwuzla;
-              z3 = pkgs-unstable.z3_4_14;
+              bitwuzla = pkgs.bitwuzla;
+              z3 = pkgs.z3;
             };
           in
           util.mkShell {
diff --git a/nix/cbmc/0001-Do-not-download-sources-in-cmake.patch b/nix/cbmc/0001-Do-not-download-sources-in-cmake.patch
@@ -1,30 +1,27 @@
-# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
-diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt
-index 003a0d957b..79751ef8b2 100644
---- a/src/solvers/CMakeLists.txt
-+++ b/src/solvers/CMakeLists.txt
-@@ -120,16 +120,6 @@ foreach(SOLVER ${sat_impl})
-     elseif("${SOLVER}" STREQUAL "cadical")
-         message(STATUS "Building solvers with cadical")
+# SPDX-License-Identifier: MIT
+From 7b49a436bd5cc903b86b01f1a0f046ab8ec99fdb Mon Sep 17 00:00:00 2001
+From: wxt <3264117476@qq.com>
+Date: Mon, 11 Nov 2024 11:07:37 +0800
+Subject: [PATCH] Do not download sources in cmake
 
--        download_project(PROJ cadical
--            URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz
--            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch
--            COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/cadical_CMakeLists.txt CMakeLists.txt
--            COMMAND ./configure
--            URL_MD5 9fc2a66196b86adceb822a583318cc35
--        )
--
--        add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR})
--
-         target_compile_definitions(solvers PUBLIC
-             SATCHECK_CADICAL HAVE_CADICAL
-         )
-@@ -137,6 +127,7 @@ foreach(SOLVER ${sat_impl})
-         target_include_directories(solvers
-             PUBLIC
-             ${cadical_SOURCE_DIR}/src
-+            ${cadical_INCLUDE_DIR}
-         )
+---
+ CMakeLists.txt | 3 +--
+ 1 file changed, 1 insertion(+), 2 deletions(-)
+
+diff --git a/CMakeLists.txt b/CMakeLists.txt
+index 2c1289a..8128362 100644
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -116,8 +116,7 @@ if(DEFINED CMAKE_USE_CUDD)
+     include("${CMAKE_CURRENT_SOURCE_DIR}/cmake/DownloadProject.cmake")
+     message(STATUS "Downloading Cudd-3.0.0")
+     download_project(PROJ cudd
+-            URL https://sourceforge.net/projects/cudd-mirror/files/cudd-3.0.0.tar.gz/download
+-            URL_MD5 4fdafe4924b81648b908881c81fe6c30
++            SOURCE_DIR @cudd@
+             )
+ 
+     if(NOT EXISTS ${cudd_SOURCE_DIR}/Makefile)
+-- 
+2.47.0
 
-         target_link_libraries(solvers cadical)
diff --git a/nix/cbmc/0002-Do-not-download-sources-in-cmake.patch b/nix/cbmc/0002-Do-not-download-sources-in-cmake.patch
@@ -0,0 +1,54 @@
+# SPDX-License-Identifier: MIT
+From c6b6438d3c87ce000b4e80b2eda2389e9473d24c Mon Sep 17 00:00:00 2001
+From: wxt <3264117476@qq.com>
+Date: Mon, 11 Nov 2024 11:35:03 +0800
+Subject: [PATCH] Do not download sources in cmake
+
+---
+ src/solvers/CMakeLists.txt | 9 +++------
+ 1 file changed, 3 insertions(+), 6 deletions(-)
+
+diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt
+index ab8d111..d7165e2 100644
+--- a/src/solvers/CMakeLists.txt
++++ b/src/solvers/CMakeLists.txt
+@@ -102,10 +102,9 @@ foreach(SOLVER ${sat_impl})
+         message(STATUS "Building solvers with glucose")
+ 
+         download_project(PROJ glucose
+-            URL https://github.com/BrunoDutertre/glucose-syrup/archive/0bb2afd3b9baace6981cbb8b4a1c7683c44968b7.tar.gz
++            SOURCE_DIR @srcglucose@
+             PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/glucose-syrup-patch
+             COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/glucose_CMakeLists.txt CMakeLists.txt
+-            URL_MD5 7c539c62c248b74210aef7414787323a
+         )
+ 
+         add_subdirectory(${glucose_SOURCE_DIR} ${glucose_BINARY_DIR})
+@@ -121,11 +120,10 @@ foreach(SOLVER ${sat_impl})
+         message(STATUS "Building solvers with cadical")
+ 
+         download_project(PROJ cadical
+-            URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz
++            SOURCE_DIR @srccadical@
+             PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch
+             COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/cadical_CMakeLists.txt CMakeLists.txt
+             COMMAND ./configure
+-            URL_MD5 9fc2a66196b86adceb822a583318cc35
+         )
+ 
+         add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR})
+@@ -144,10 +142,9 @@ foreach(SOLVER ${sat_impl})
+         message(STATUS "Building with IPASIR solver linking against: CaDiCaL")
+ 
+         download_project(PROJ cadical
+-            URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz
++            SOURCE_DIR @srccadical@
+             PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch
+             COMMAND ./configure
+-            URL_MD5 9fc2a66196b86adceb822a583318cc35
+         )
+ 
+         message(STATUS "Building CaDiCaL")
+-- 
+2.47.0
+
diff --git a/nix/cbmc/default.nix b/nix/cbmc/default.nix
@@ -7,6 +7,8 @@
 , ninja
 , cadical
 , z3
+, cudd
+, replaceVars
 }:
 
 buildEnv {
@@ -18,17 +20,24 @@ buildEnv {
         src = fetchFromGitHub {
           owner = "diffblue";
           repo = "cbmc";
-          rev = "3c915ebe35448a20555c1ef55d51540b52c5c34a";
           hash = "sha256-ot0vVBgiSVru/RE7KeyTsXzDfs0CSa5vaFsON+PCZZo=";
+          tag = "cbmc-6.6.0";
         };
+        # TODO: Remove those once upstream has removed the third patch
+        patches = [
+          (replaceVars ./0001-Do-not-download-sources-in-cmake.patch {
+            cudd = cudd.src;
+          })
+          ./0002-Do-not-download-sources-in-cmake.patch
+        ];
       });
       litani = callPackage ./litani.nix { }; # 1.29.0
       cbmc-viewer = callPackage ./cbmc-viewer.nix { }; # 3.11
 
       inherit
-        cadical#1.9.5
+        cadical#2.1.3
         bitwuzla# 0.7.0
-        z3# 4.14.1
-        ninja; # 1.11.1
+        z3# 4.15.0
+        ninja; # 1.12.1
     };
 }
diff --git a/nix/slothy/default.nix b/nix/slothy/default.nix
@@ -15,35 +15,10 @@
 
 
 let
-  # TODO: switch to protobuf from nixpkgs
-  # ortools 9.12 requires protobuf >= 5.29.3 - currently nixpkgs 24.11 has
-  # protobuf 5.28.3
-  protobuf_6_30_1 = python312Packages.buildPythonPackage rec {
-    pname = "protobuf";
-    version = "5.29.3";
-
-    propagatedBuildInputs = [
-      python312Packages.setuptools
-    ];
-
-    build-system = with python312Packages; [
-      setuptools
-    ];
-
-    dontConfigure = true;
-    nativeBuildInputs =
-      [
-        cmake
-        pkg-config
-      ];
-
-    src = fetchPypi {
-      inherit pname version;
-      hash = "sha256-XaD0HtrxF73jFkBLrRpIbLTt7fjkpUiRKW9kjo4HZiA=";
-    };
-  };
-
 
+  # I have experimented with the ortools (9.12) that is packaged in nixpkgs.
+  # However, it results in _much_ poorer SLOTHY performance and, we hence,
+  # instead stick to the pre-built ones from pypi.
   ortools912 = python312Packages.buildPythonPackage rec {
     pname = "ortools";
     version = "9.12.4544";
@@ -78,44 +53,15 @@ let
     propagatedBuildInputs = with python312Packages; [
       numpy
       pandas
-      protobuf_6_30_1
+      protobuf
     ];
 
   };
 
-  # TODO: switch to unicorn from nixpkgs
-  # nixpkgs 24.11 currently has 2.1.1 - we are experiencing some issues with
-  # that version on MacOS. 2.1.2/2.1.3 (and also some older versions) don't
-  # have that problem
-  unicorn_2_1_3 = python312Packages.buildPythonPackage rec {
-    pname = "unicorn";
-    version = "2.1.3";
-
-    propagatedBuildInputs = [
-      python312Packages.setuptools
-    ];
-
-    build-system = with python312Packages; [
-      setuptools
-    ];
-
-    dontConfigure = true;
-    nativeBuildInputs =
-      [
-        cmake
-        pkg-config
-      ];
-
-    src = fetchPypi {
-      inherit pname version;
-      hash = "sha256-DAZFbPVQwijyADzHA2avpK7OLm5+TDLY9LIscXumtyk=";
-    };
-  };
-
   pythonEnv = python312.withPackages (ps: with ps; [
     ortools912
     sympy
-    unicorn_2_1_3
+    unicorn
   ]);
 
 in
diff --git a/nix/util.nix b/nix/util.nix
@@ -8,7 +8,7 @@ rec {
   };
 
   wrap-gcc = p: p.buildPackages.wrapCCWith {
-    cc = p.buildPackages.gcc14.cc;
+    cc = p.buildPackages.gcc.cc;
     bintools = p.buildPackages.wrapBintoolsWith {
       bintools = p.buildPackages.binutils-unwrapped;
       libc = glibc-join p;
@@ -17,7 +17,7 @@ rec {
 
   native-gcc =
     if pkgs.stdenv.isDarwin
-    then pkgs.clang_16
+    then pkgs.clang
     else wrap-gcc pkgs;
 
   # cross is for determining whether to install the cross toolchain dependencies or not
@@ -39,7 +39,8 @@ rec {
     pkgs.lib.optionals cross [ pkgs.qemu x86_64-gcc aarch64-gcc riscv64-gcc ppc64le-gcc ]
     ++ pkgs.lib.optionals (cross && pkgs.stdenv.isLinux && pkgs.stdenv.isx86_64) [ aarch64_be-gcc ]
     ++ pkgs.lib.optionals cross [ native-gcc ]
-    # NOTE: Tools in /Library/Developer/CommandLineTools/usr/bin on macOS are inaccessible in the Nix shell. This issue is addressed in https://github.com/NixOS/nixpkgs/pull/353893 but hasn’t been merged into the 24.11 channel yet. As a workaround, we include this dependency for macOS temporary.
+    # git is not available in the nix shell on Darwin. As a workaround we add git as a dependency here.
+    # Initially, we expected this to be fixed by https://github.com/NixOS/nixpkgs/pull/353893, but that does not seem to be the case.
     ++ pkgs.lib.optionals (pkgs.stdenv.isDarwin) [ pkgs.git ]
     ++ builtins.attrValues {
       inherit (pkgs.python3Packages) sympy pyyaml;
@@ -75,10 +76,10 @@ rec {
     name = "pqcp-linters";
     paths = builtins.attrValues {
       clang-tools = pkgs.clang-tools.overrideAttrs {
-        unwrapped = pkgs.llvmPackages_18.clang-unwrapped;
+        unwrapped = pkgs.llvmPackages.clang-unwrapped;
       };
 
-      inherit (pkgs.llvmPackages_18)
+      inherit (pkgs.llvmPackages)
         bintools;
 
       inherit (pkgs)
