Skip to content

Commit 13bc4a4

Browse files
mkannwischermkannwischer
committed
Update to nixpkgs 25.05
Notable changes are: - Default clang/llvm is now 19; we switch to the default in the core shells - Default gcc is now 14; we switch to it in the core shells - gcc 7, zig_0_10, zig_0_11 are not longer supported in 25.05; we instead take it from nixpkgs 24.05 - zig_0_14 has been added; we test in CI now as well - Unicorn and protobuf versions are now compatible with SLOTHY simpliying the build - z3 has been updated to 4.15.0; we take it from 25.05 - clang_20, bitwuzla, qemu now have suitable versions in 25.05; we no longer need to take them from unstable. - The upstream CBMC nixpkgs build (6.4.1) uses 3 patches instead of 2 used before. Since we are using 6.6.0, we do not require the third patch. We, hence, have to overwrite the patches here locally and use on the the first two. This slighty complicates our flake. - A few dependency updates for which we do not require specific versions Signed-off-by: Matthias J. Kannwischer <[email protected]> .
1 parent a1ad592 commit 13bc4a4

8 files changed

+126
-86
lines changed

‎.github/workflows/ci.yml

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -405,6 +405,13 @@ jobs:
405405
c23: False
406406
examples: False
407407
opt: no_opt
408+
- name: zig-0.14
409+
shell: ci_zig0_14
410+
darwin: True
411+
c17: True
412+
c23: True
413+
examples: False
414+
opt: no_opt
408415
runs-on: ${{ matrix.target.runner }}
409416
steps:
410417
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2

‎flake.lock

Lines changed: 4 additions & 4 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎flake.nix

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77

88
inputs = {
99
nixpkgs-2405.url = "github:NixOS/nixpkgs/nixos-24.05";
10-
nixpkgs.url = "github:NixOS/nixpkgs/nixos-24.11";
10+
nixpkgs.url = "github:NixOS/nixpkgs/nixos-25.05";
1111
nixpkgs-unstable.url = "github:NixOS/nixpkgs/nixos-unstable";
1212

1313
flake-parts = {
@@ -25,9 +25,10 @@
2525
pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.${system};
2626
pkgs-2405 = inputs.nixpkgs-2405.legacyPackages.${system};
2727
util = pkgs.callPackage ./nix/util.nix {
28+
# Keep those around in case we want to switch to unstable versions
2829
cbmc = pkgs.cbmc;
29-
bitwuzla = pkgs-unstable.bitwuzla;
30-
z3 = pkgs-unstable.z3_4_14;
30+
bitwuzla = pkgs.bitwuzla;
31+
z3 = pkgs.z3;
3132
};
3233
zigWrapCC = zig: pkgs.symlinkJoin {
3334
name = "zig-wrappers";
@@ -50,8 +51,9 @@
5051
(_:_: {
5152
gcc48 = pkgs-2405.gcc48;
5253
gcc49 = pkgs-2405.gcc49;
53-
qemu = pkgs-unstable.qemu; # 9.2.2
54-
clang_20 = pkgs-unstable.clang_20;
54+
gcc7 = pkgs-2405.gcc7;
55+
zig_0_10 = pkgs-2405.zig_0_10;
56+
zig_0_11 = pkgs-2405.zig_0_11;
5557
})
5658
];
5759
};
@@ -111,6 +113,7 @@
111113
devShells.ci_zig0_11 = util.mkShellWithCC' (zigWrapCC pkgs.zig_0_11);
112114
devShells.ci_zig0_12 = util.mkShellWithCC' (zigWrapCC pkgs.zig_0_12);
113115
devShells.ci_zig0_13 = util.mkShellWithCC' (zigWrapCC pkgs.zig_0_13);
116+
devShells.ci_zig0_14 = util.mkShellWithCC' (zigWrapCC pkgs.zig);
114117

115118
devShells.ci_gcc48 = util.mkShellWithCC' pkgs.gcc48;
116119
devShells.ci_gcc49 = util.mkShellWithCC' pkgs.gcc49;
@@ -144,8 +147,8 @@
144147
util = pkgs.callPackage ./nix/util.nix {
145148
inherit pkgs;
146149
cbmc = pkgs.cbmc;
147-
bitwuzla = pkgs-unstable.bitwuzla;
148-
z3 = pkgs-unstable.z3_4_14;
150+
bitwuzla = pkgs.bitwuzla;
151+
z3 = pkgs.z3;
149152
};
150153
in
151154
util.mkShell {

‎nix/cbmc/0001-Do-not-download-sources-in-cmake.patch

Lines changed: 27 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,27 @@
1-
# Copyright (c) The mlkem-native project authors
2-
# Copyright (c) The mldsa-native project authors
3-
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4-
diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt
5-
index 003a0d957b..79751ef8b2 100644
6-
--- a/src/solvers/CMakeLists.txt
7-
+++ b/src/solvers/CMakeLists.txt
1+
# SPDX-License-Identifier: MIT
2+
From 7b49a436bd5cc903b86b01f1a0f046ab8ec99fdb Mon Sep 17 00:00:00 2001
3+
From: wxt <[email protected]>
4+
Date: Mon, 11 Nov 2024 11:07:37 +0800
5+
Subject: [PATCH] Do not download sources in cmake
6+
7+
---
8+
CMakeLists.txt | 3 +--
9+
1 file changed, 1 insertion(+), 2 deletions(-)
10+
11+
diff --git a/CMakeLists.txt b/CMakeLists.txt
12+
index 2c1289a..8128362 100644
13+
--- a/CMakeLists.txt
14+
+++ b/CMakeLists.txt
15+
@@ -116,8 +116,7 @@ if(DEFINED CMAKE_USE_CUDD)
16+
include("${CMAKE_CURRENT_SOURCE_DIR}/cmake/DownloadProject.cmake")
17+
message(STATUS "Downloading Cudd-3.0.0")
18+
download_project(PROJ cudd
19+
- URL https://sourceforge.net/projects/cudd-mirror/files/cudd-3.0.0.tar.gz/download
20+
- URL_MD5 4fdafe4924b81648b908881c81fe6c30
21+
+ SOURCE_DIR @cudd@
22+
)
23+
24+
if(NOT EXISTS ${cudd_SOURCE_DIR}/Makefile)
25+
--
26+
2.47.0
27+

‎nix/cbmc/0002-Do-not-download-sources-in-cmake.patch

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
# SPDX-License-Identifier: MIT
2+
From c6b6438d3c87ce000b4e80b2eda2389e9473d24c Mon Sep 17 00:00:00 2001
3+
From: wxt <[email protected]>
4+
Date: Mon, 11 Nov 2024 11:35:03 +0800
5+
Subject: [PATCH] Do not download sources in cmake
6+
7+
---
8+
src/solvers/CMakeLists.txt | 9 +++------
9+
1 file changed, 3 insertions(+), 6 deletions(-)
10+
11+
diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt
12+
index ab8d111..d7165e2 100644
13+
--- a/src/solvers/CMakeLists.txt
14+
+++ b/src/solvers/CMakeLists.txt
15+
@@ -102,10 +102,9 @@ foreach(SOLVER ${sat_impl})
16+
message(STATUS "Building solvers with glucose")
17+
18+
download_project(PROJ glucose
19+
- URL https://github.com/BrunoDutertre/glucose-syrup/archive/0bb2afd3b9baace6981cbb8b4a1c7683c44968b7.tar.gz
20+
+ SOURCE_DIR @srcglucose@
21+
PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/glucose-syrup-patch
22+
COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/glucose_CMakeLists.txt CMakeLists.txt
23+
- URL_MD5 7c539c62c248b74210aef7414787323a
24+
)
25+
26+
add_subdirectory(${glucose_SOURCE_DIR} ${glucose_BINARY_DIR})
27+
@@ -121,11 +120,10 @@ foreach(SOLVER ${sat_impl})
28+
message(STATUS "Building solvers with cadical")
29+
30+
download_project(PROJ cadical
31+
- URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz
32+
+ SOURCE_DIR @srccadical@
33+
PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch
34+
COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/cadical_CMakeLists.txt CMakeLists.txt
35+
COMMAND ./configure
36+
- URL_MD5 9fc2a66196b86adceb822a583318cc35
37+
)
38+
39+
add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR})
40+
@@ -144,10 +142,9 @@ foreach(SOLVER ${sat_impl})
41+
message(STATUS "Building with IPASIR solver linking against: CaDiCaL")
42+
43+
download_project(PROJ cadical
44+
- URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz
45+
+ SOURCE_DIR @srccadical@
46+
PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch
47+
COMMAND ./configure
48+
- URL_MD5 9fc2a66196b86adceb822a583318cc35
49+
)
50+
51+
message(STATUS "Building CaDiCaL")
52+
--
53+
2.47.0
54+

‎nix/cbmc/default.nix

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,8 @@
99
, ninja
1010
, cadical
1111
, z3
12+
, cudd
13+
, replaceVars
1214
}:
1315

1416
buildEnv {
@@ -20,17 +22,24 @@ buildEnv {
2022
src = fetchFromGitHub {
2123
owner = "diffblue";
2224
repo = "cbmc";
23-
rev = "3c915ebe35448a20555c1ef55d51540b52c5c34a";
2425
hash = "sha256-ot0vVBgiSVru/RE7KeyTsXzDfs0CSa5vaFsON+PCZZo=";
26+
tag = "cbmc-6.6.0";
2527
};
28+
# TODO: Remove those once upstream has removed the third patch
29+
patches = [
30+
(replaceVars ./0001-Do-not-download-sources-in-cmake.patch {
31+
cudd = cudd.src;
32+
})
33+
./0002-Do-not-download-sources-in-cmake.patch
34+
];
2635
});
2736
litani = callPackage ./litani.nix { }; # 1.29.0
2837
cbmc-viewer = callPackage ./cbmc-viewer.nix { }; # 3.11
2938

3039
inherit
31-
cadical#1.9.5
40+
cadical#2.1.3
3241
bitwuzla# 0.7.0
33-
z3# 4.14.1
34-
ninja; # 1.11.1
42+
z3# 4.15.0
43+
ninja; # 1.12.1
3544
};
3645
}

‎nix/slothy/default.nix

Lines changed: 5 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -17,35 +17,10 @@
1717

1818

1919
let
20-
# TODO: switch to protobuf from nixpkgs
21-
# ortools 9.12 requires protobuf >= 5.29.3 - currently nixpkgs 24.11 has
22-
# protobuf 5.28.3
23-
protobuf_6_30_1 = python312Packages.buildPythonPackage rec {
24-
pname = "protobuf";
25-
version = "5.29.3";
26-
27-
propagatedBuildInputs = [
28-
python312Packages.setuptools
29-
];
30-
31-
build-system = with python312Packages; [
32-
setuptools
33-
];
34-
35-
dontConfigure = true;
36-
nativeBuildInputs =
37-
[
38-
cmake
39-
pkg-config
40-
];
41-
42-
src = fetchPypi {
43-
inherit pname version;
44-
hash = "sha256-XaD0HtrxF73jFkBLrRpIbLTt7fjkpUiRKW9kjo4HZiA=";
45-
};
46-
};
47-
4820

21+
# I have experimented with the ortools (9.12) that is packaged in nixpkgs.
22+
# However, it results in _much_ poorer SLOTHY performance and, we hence,
23+
# instead stick to the pre-built ones from pypi.
4924
ortools912 = python312Packages.buildPythonPackage rec {
5025
pname = "ortools";
5126
version = "9.12.4544";
@@ -80,44 +55,15 @@ let
8055
propagatedBuildInputs = with python312Packages; [
8156
numpy
8257
pandas
83-
protobuf_6_30_1
58+
protobuf
8459
];
8560

8661
};
8762

88-
# TODO: switch to unicorn from nixpkgs
89-
# nixpkgs 24.11 currently has 2.1.1 - we are experiencing some issues with
90-
# that version on MacOS. 2.1.2/2.1.3 (and also some older versions) don't
91-
# have that problem
92-
unicorn_2_1_3 = python312Packages.buildPythonPackage rec {
93-
pname = "unicorn";
94-
version = "2.1.3";
95-
96-
propagatedBuildInputs = [
97-
python312Packages.setuptools
98-
];
99-
100-
build-system = with python312Packages; [
101-
setuptools
102-
];
103-
104-
dontConfigure = true;
105-
nativeBuildInputs =
106-
[
107-
cmake
108-
pkg-config
109-
];
110-
111-
src = fetchPypi {
112-
inherit pname version;
113-
hash = "sha256-DAZFbPVQwijyADzHA2avpK7OLm5+TDLY9LIscXumtyk=";
114-
};
115-
};
116-
11763
pythonEnv = python312.withPackages (ps: with ps; [
11864
ortools912
11965
sympy
120-
unicorn_2_1_3
66+
unicorn
12167
]);
12268

12369
in

‎nix/util.nix

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ rec {
1010
};
1111

1212
wrap-gcc = p: p.buildPackages.wrapCCWith {
13-
cc = p.buildPackages.gcc14.cc;
13+
cc = p.buildPackages.gcc.cc;
1414
bintools = p.buildPackages.wrapBintoolsWith {
1515
bintools = p.buildPackages.binutils-unwrapped;
1616
libc = glibc-join p;
@@ -19,7 +19,7 @@ rec {
1919

2020
native-gcc =
2121
if pkgs.stdenv.isDarwin
22-
then pkgs.clang_16
22+
then pkgs.clang
2323
else wrap-gcc pkgs;
2424

2525
# cross is for determining whether to install the cross toolchain dependencies or not
@@ -41,7 +41,8 @@ rec {
4141
pkgs.lib.optionals cross [ pkgs.qemu x86_64-gcc aarch64-gcc riscv64-gcc ppc64le-gcc ]
4242
++ pkgs.lib.optionals (cross && pkgs.stdenv.isLinux && pkgs.stdenv.isx86_64) [ aarch64_be-gcc ]
4343
++ pkgs.lib.optionals cross [ native-gcc ]
44-
# 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.
44+
# git is not available in the nix shell on Darwin. As a workaround we add git as a dependency here.
45+
# Initially, we expected this to be fixed by https://github.com/NixOS/nixpkgs/pull/353893, but that does not seem to be the case.
4546
++ pkgs.lib.optionals (pkgs.stdenv.isDarwin) [ pkgs.git ]
4647
++ builtins.attrValues {
4748
inherit (pkgs.python3Packages) sympy pyyaml;
@@ -77,10 +78,10 @@ rec {
7778
name = "pqcp-linters";
7879
paths = builtins.attrValues {
7980
clang-tools = pkgs.clang-tools.overrideAttrs {
80-
unwrapped = pkgs.llvmPackages_18.clang-unwrapped;
81+
unwrapped = pkgs.llvmPackages.clang-unwrapped;
8182
};
8283

83-
inherit (pkgs.llvmPackages_18)
84+
inherit (pkgs.llvmPackages)
8485
bintools;
8586

8687
inherit (pkgs)

0 commit comments

Comments
 (0)