From 065037f03dc547c2a506fc8224c8704ae889740b Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Thu, 4 Jun 2026 18:21:19 +0800 Subject: [PATCH] nix: bump to nixpkgs 26.05 Update the nixpkgs input from nixos-25.11 to nixos-26.05 and adjust the flake to the new package set: - Default gcc changed from 14.3.0 to 15.2.0 - slothy: use the new pkgs.slothy from nixpkgs instead of the custom build; nix/slothy/default.nix now just re-exports it with a commented override for pinning a specific upstream revision. Drops the python3-for-slothy (unstable ortools) workaround. - hol_light: hol_light is now taken directly from nixpkgs, as I have upstreamed a recent version and made the necessary adjustments to make it directly usable. Similar as for slothy, we keep a separate package to make it easier to overwrite the version in the future. - python: provide script dependencies (pyparsing, sympy, ...) via python3.withPackages instead of bare python3Packages entries in a symlinkJoin, which no longer reach sys.path. Fixes autogen's "No module named 'pyparsing'". - autogen: use the snake_case pyparsing API (parse_string/parse_all) to silence the deprecation warning from the newer pyparsing. - cbmc: bitwuzla version 0.8.2 -> 0.9.0. - autogen: Reformatted with newer ruff version - platform tests: Increase disk on x86 from 20 GiB to 30 GiB as nix derivation does not fit anymore otherwise. - clang 18: Clang 18 from 26.05 no longer compiles on MacOS - take it from the 24.05 channel instead. Ports https://github.com/pq-code-package/mlkem-native/pull/1711 Resolves https://github.com/pq-code-package/mldsa-native/issues/1147 Signed-off-by: Matthias J. Kannwischer --- .github/workflows/ci.yml | 5 +- flake.lock | 8 +-- flake.nix | 52 ++++++++-------- nix/cbmc/default.nix | 2 +- ...05-Configure-hol-sh-for-mldsa-native.patch | 36 ----------- .../0006-Add-findlib-to-ocaml-hol.patch | 13 ---- nix/hol_light/default.nix | 48 ++++++--------- nix/legacy/default.nix | 1 + nix/slothy/default.nix | 59 +++++-------------- nix/util.nix | 52 ++++++++-------- scripts/autogen | 9 ++- 11 files changed, 97 insertions(+), 188 deletions(-) delete mode 100644 nix/hol_light/0005-Configure-hol-sh-for-mldsa-native.patch delete mode 100644 nix/hol_light/0006-Add-findlib-to-ocaml-hol.patch diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9b18bbca8..005f02fb3 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -561,14 +561,14 @@ jobs: - name: AMD EPYC 4th gen (t3a) ec2_instance_type: t3a.small ec2_ami: ubuntu-latest (x86_64) - ec2_volume_size: 20 + ec2_volume_size: 30 compile_mode: native opt: all config_variations: 'native-cap-CPUID_AVX2' - name: Intel Xeon 4th gen (t3) ec2_instance_type: t3.small ec2_ami: ubuntu-latest (x86_64) - ec2_volume_size: 20 + ec2_volume_size: 30 compile_mode: native opt: all config_variations: 'native-cap-CPUID_AVX2' @@ -596,6 +596,7 @@ jobs: name: ${{ matrix.target.name }} ec2_instance_type: ${{ matrix.target.ec2_instance_type }} ec2_ami: ${{ matrix.target.ec2_ami }} + ec2_volume_size: ${{ matrix.target.ec2_volume_size }} compile_mode: ${{ matrix.target.compile_mode }} opt: ${{ matrix.target.opt }} config_variations: ${{ matrix.target.config_variations || '' }} diff --git a/flake.lock b/flake.lock index 0a6ccebf6..d09c4b3be 100644 --- a/flake.lock +++ b/flake.lock @@ -22,16 +22,16 @@ }, "nixpkgs": { "locked": { - "lastModified": 1770464364, - "narHash": "sha256-z5NJPSBwsLf/OfD8WTmh79tlSU8XgIbwmk6qB1/TFzY=", + "lastModified": 1780453794, + "narHash": "sha256-bXMRa9VTsHSPXL4Cw8R6JJLQeY3Y/IP4+YJCYVmQ7FY=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "23d72dabcb3b12469f57b37170fcbc1789bd7457", + "rev": "6b316287bae2ee04c9b93c8c858d930fd07d7338", "type": "github" }, "original": { "owner": "NixOS", - "ref": "nixos-25.11", + "ref": "nixos-26.05", "repo": "nixpkgs", "type": "github" } diff --git a/flake.nix b/flake.nix index c298ea9f4..2c1dbc64b 100644 --- a/flake.nix +++ b/flake.nix @@ -6,7 +6,7 @@ description = "mldsa-native"; inputs = { - nixpkgs.url = "github:NixOS/nixpkgs/nixos-25.11"; + nixpkgs.url = "github:NixOS/nixpkgs/nixos-26.05"; nixpkgs-unstable.url = "github:NixOS/nixpkgs/nixos-unstable"; flake-parts = { @@ -22,11 +22,10 @@ perSystem = { config, pkgs, system, ... }: let pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.${system}; - util = pkgs.callPackage ./nix/util.nix { - inherit (pkgs) bitwuzla z3; - inherit (pkgs-unstable) cbmc; - # TODO: switch back to stable python3 for slothy once ortools is fixed in 25.11 - python3-for-slothy = pkgs-unstable.python3; + util = pkgs.callPackage ./nix/util.nix { }; + holLightToolchain = builtins.attrValues { + inherit (pkgs) ocaml ledit; + inherit (pkgs.ocamlPackages) findlib camlp5 zarith; }; zigWrapCC = zig: pkgs.symlinkJoin { name = "zig-wrappers"; @@ -55,6 +54,8 @@ mkdir -p "$IMPORTS_DIR" ln -sfn "$S2N_BIGNUM_DIR" "$IMPORTS_DIR/s2n_bignum" ln -sfn "$PROOF_DIR" "$IMPORTS_DIR/mldsa_native" + export HOLLIGHT_LOAD_PATH="$IMPORTS_DIR:$S2N_BIGNUM_DIR''${HOLLIGHT_LOAD_PATH:+:$HOLLIGHT_LOAD_PATH}" + export HOLDIR="$HOLLIGHT_DIR" ''; in { @@ -62,10 +63,7 @@ inherit system; overlays = [ (_:_: { - clang_22 = pkgs-unstable.clang_22; - gcc16 = pkgs-unstable.gcc16; - zig_0_16 = pkgs-unstable.zig; - isabelle = pkgs-unstable.isabelle; + # Add pkgs-unstable overlays here when needed }) ]; }; @@ -96,21 +94,22 @@ direnv nix-direnv zig_0_13; - } ++ pkgs.lib.optionals (!pkgs.stdenv.isDarwin) [ config.packages.valgrind_varlat ]; + } ++ holLightToolchain + ++ pkgs.lib.optionals (!pkgs.stdenv.isDarwin) [ config.packages.valgrind_varlat ]; }).overrideAttrs (old: { shellHook = holLightShellHook; }); packages.hol_server = util.hol_server.hol_server_start; devShells.hol_light = (util.mkShell { - packages = builtins.attrValues { inherit (config.packages) linters hol_light s2n_bignum hol_server; }; + packages = builtins.attrValues { inherit (config.packages) linters hol_light s2n_bignum hol_server; } ++ holLightToolchain; }).overrideAttrs (old: { shellHook = holLightShellHook; }); devShells.hol_light-cross = (util.mkShell { - packages = builtins.attrValues { inherit (config.packages) linters toolchains hol_light s2n_bignum gcc-arm-embedded hol_server; }; + packages = builtins.attrValues { inherit (config.packages) linters toolchains hol_light s2n_bignum gcc-arm-embedded hol_server; } ++ holLightToolchain; }).overrideAttrs (old: { shellHook = holLightShellHook; }); devShells.hol_light-cross-aarch64 = (util.mkShell { - packages = builtins.attrValues { inherit (config.packages) linters toolchain_aarch64 hol_light s2n_bignum gcc-arm-embedded hol_server; }; + packages = builtins.attrValues { inherit (config.packages) linters toolchain_aarch64 hol_light s2n_bignum gcc-arm-embedded hol_server; } ++ holLightToolchain; }).overrideAttrs (old: { shellHook = holLightShellHook; }); devShells.hol_light-cross-x86_64 = (util.mkShell { - packages = builtins.attrValues { inherit (config.packages) linters toolchain_x86_64 hol_light s2n_bignum gcc-arm-embedded hol_server; }; + packages = builtins.attrValues { inherit (config.packages) linters toolchain_x86_64 hol_light s2n_bignum gcc-arm-embedded hol_server; } ++ holLightToolchain; }).overrideAttrs (old: { shellHook = holLightShellHook; }); devShells.ci = util.mkShell { packages = builtins.attrValues { inherit (config.packages) linters toolchains_native; }; @@ -178,15 +177,16 @@ { inherit (util) pqmx; inherit (config.packages) linters; - inherit (pkgs) gcc-arm-embedded qemu coreutils python3 git; + inherit (pkgs) gcc-arm-embedded qemu coreutils git; }; }; devShells.cross-aarch64-embedded = util.mkShell { packages = builtins.attrValues { - inherit (pkgs) qemu coreutils python3 git; + inherit (pkgs) qemu coreutils git; } ++ [ - pkgs-unstable.pkgsCross.aarch64-embedded.stdenv.cc + util.pythonEnv + pkgs.pkgsCross.aarch64-embedded.stdenv.cc ]; }; @@ -198,7 +198,6 @@ devShells.linter = util.mkShellNoCC { packages = builtins.attrValues { inherit (config.packages) linters; }; }; - devShells.clang18 = util.mkShellWithCC' pkgs.clang_18; devShells.clang19 = util.mkShellWithCC' pkgs.clang_19; devShells.clang20 = util.mkShellWithCC' pkgs.clang_20; devShells.clang21 = util.mkShellWithCC' pkgs.clang_21; @@ -206,7 +205,7 @@ devShells.zig0_13 = util.mkShellWithCC' (zigWrapCC pkgs.zig_0_13); devShells.zig0_14 = util.mkShellWithCC' (zigWrapCC pkgs.zig_0_14); - devShells.zig0_15 = util.mkShellWithCC' (zigWrapCC pkgs.zig); + devShells.zig0_15 = util.mkShellWithCC' (zigWrapCC pkgs.zig_0_15); devShells.zig0_16 = util.mkShellWithCC' (zigWrapCC pkgs.zig_0_16); devShells.gcc13 = util.mkShellWithCC' pkgs.gcc13; @@ -215,7 +214,6 @@ devShells.gcc16 = util.mkShellWithCC' pkgs.gcc16; # valgrind with a patch for detecting variable-latency instructions - devShells.valgrind-varlat_clang18 = util.mkShellWithCC_valgrind' pkgs.clang_18; devShells.valgrind-varlat_clang19 = util.mkShellWithCC_valgrind' pkgs.clang_19; devShells.valgrind-varlat_clang20 = util.mkShellWithCC_valgrind' pkgs.clang_20; devShells.valgrind-varlat_clang21 = util.mkShellWithCC_valgrind' pkgs.clang_21; @@ -230,13 +228,7 @@ let pkgs = inputs.nixpkgs.legacyPackages.x86_64-linux; pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.x86_64-linux; - util = pkgs.callPackage ./nix/util.nix { - inherit pkgs; - inherit (pkgs) bitwuzla z3; - inherit (pkgs-unstable) cbmc; - # TODO: switch back to stable python3 for slothy once ortools is fixed in 25.11 - python3-for-slothy = pkgs-unstable.python3; - }; + util = pkgs.callPackage ./nix/util.nix { }; in util.mkShell { packages = @@ -248,6 +240,10 @@ util.toolchains_native pkgs.zig_0_13 ] + ++ builtins.attrValues { + inherit (pkgs) ocaml ledit; + inherit (pkgs.ocamlPackages) findlib camlp5 zarith; + } ++ pkgs.lib.optionals (!pkgs.stdenv.isDarwin) [ util.valgrind_varlat ]; }; # The usual flake attributes can be defined here, including system- diff --git a/nix/cbmc/default.nix b/nix/cbmc/default.nix index 58e21c796..bc649c793 100644 --- a/nix/cbmc/default.nix +++ b/nix/cbmc/default.nix @@ -36,7 +36,7 @@ buildEnv { }); inherit - bitwuzla# 0.8.2 + bitwuzla# 0.9.0 ninja; # 1.13.2 }; } diff --git a/nix/hol_light/0005-Configure-hol-sh-for-mldsa-native.patch b/nix/hol_light/0005-Configure-hol-sh-for-mldsa-native.patch deleted file mode 100644 index 16e355739..000000000 --- a/nix/hol_light/0005-Configure-hol-sh-for-mldsa-native.patch +++ /dev/null @@ -1,36 +0,0 @@ -# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT -diff --git a/hol_4.14.sh b/hol_4.14.sh ---- a/hol_4.14.sh -+++ b/hol_4.14.sh -@@ -57,4 +57,12 @@ if [ "${HOL_ML_PATH}" == "" ]; then - HOL_ML_PATH="${HOLLIGHT_DIR}/hol.ml" - fi - --${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -init ${HOL_ML_PATH} -I ${HOLLIGHT_DIR} -+# Add site-lib directory for topfind -+SITELIB=$(dirname $(ocamlfind query findlib 2>/dev/null) 2>/dev/null) -+# Resolve namespace-prefixed imports via $IMPORTS_DIR (populated by the -+# nix shellHook). The $S2N_BIGNUM_DIR fallback is retained only so -+# s2n-bignum's own internal `needs "common/..."` directives still resolve -+# during transitive loads; mldsa-native code never produces a bare path. -+export HOLLIGHT_LOAD_PATH="${IMPORTS_DIR}:${S2N_BIGNUM_DIR}:${HOLLIGHT_LOAD_PATH}" -+[ -n "${PROOF_DIR}" ] && cd "${PROOF_DIR}" -+${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -init ${HOL_ML_PATH} -I ${HOLLIGHT_DIR} ${SITELIB:+-I "$SITELIB"} -diff --git a/hol_4.sh b/hol_4.sh ---- a/hol_4.sh -+++ b/hol_4.sh -@@ -5,7 +5,7 @@ export HOLLIGHT_DIR=__DIR__ - - if [ "$#" -eq 1 ]; then - if [ "$1" == "-pp" ]; then -- echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I "__DIR__" pa_j.cmo" -+ echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I \"${HOLLIGHT_DIR}\" pa_j.cmo" - exit 0 - elif [ "$1" == "-dir" ]; then - echo "${HOLLIGHT_DIR}" -@@ -32,4 +32,4 @@ if [ "${HOL_ML_PATH}" == "" ]; then - HOL_ML_PATH="${HOLLIGHT_DIR}/hol.ml" - fi - --${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -I `camlp5 -where` camlp5o.cma -init ${HOL_ML_PATH} -safe-string -I ${HOLLIGHT_DIR} -+${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -I $(camlp5 -where) camlp5o.cma -init ${HOL_ML_PATH} -safe-string -I ${HOLLIGHT_DIR} diff --git a/nix/hol_light/0006-Add-findlib-to-ocaml-hol.patch b/nix/hol_light/0006-Add-findlib-to-ocaml-hol.patch deleted file mode 100644 index 9ad62dbb9..000000000 --- a/nix/hol_light/0006-Add-findlib-to-ocaml-hol.patch +++ /dev/null @@ -1,13 +0,0 @@ -# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT -diff --git a/Makefile b/Makefile -index abc1234..def5678 100644 ---- a/Makefile -+++ b/Makefile -@@ -100,7 +100,7 @@ hol.sh: pa_j.cmo ${HOLSRC} bignum.cmo hol_loader.cmo update_database.ml - if [ `uname` = "Linux" ] || [ `uname` = "Darwin" ] ; then \ - if [ ${OCAML_UNARY_VERSION} = "5" ] || [ ${OCAML_VERSION} = "4.14" ] ; then \ -- ocamlfind ocamlmktop -package zarith -o ocaml-hol zarith.cma bignum.cmo hol_loader.cmo ; \ -+ ocamlfind ocamlmktop -package zarith,findlib -o ocaml-hol zarith.cma bignum.cmo hol_loader.cmo ; \ - sed "s^__DIR__^`pwd`^g; s^__USE_MODULE__^$(HOLLIGHT_USE_MODULE)^g" hol_4.14.sh > hol.sh ; \ - else \ - ocamlmktop -o ocaml-hol nums.cma bignum.cmo hol_loader.cmo ; \ diff --git a/nix/hol_light/default.nix b/nix/hol_light/default.nix index 38ee4adde..dac3b4581 100644 --- a/nix/hol_light/default.nix +++ b/nix/hol_light/default.nix @@ -2,34 +2,20 @@ # Copyright (c) The mldsa-native project authors # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT -{ hol_light, fetchFromGitHub, writeText, ocamlPackages, ledit, ... }: -hol_light.overrideAttrs (old: { - setupHook = writeText "setup-hook.sh" '' - export HOLDIR="$1/lib/hol_light" - export HOLLIGHT_DIR="$1/lib/hol_light" - export PATH="$1/lib/hol_light:$PATH" - ''; - version = "unstable-2026-04-17"; - src = fetchFromGitHub { - owner = "jrh13"; - repo = "hol-light"; - rev = "af5d20e033025a9f30a490d9c39edace632405a3"; - hash = "sha256-R5hSHguVu7YPP7bnFJQ1Prc8Yy3L41LAB20LfEr/RUw="; - }; - patches = [ - ./0005-Configure-hol-sh-for-mldsa-native.patch - ./0006-Add-findlib-to-ocaml-hol.patch - ]; - propagatedBuildInputs = old.propagatedBuildInputs ++ old.nativeBuildInputs ++ [ ocamlPackages.pcre2 ledit ]; - buildPhase = '' - patchShebangs . - HOLLIGHT_USE_MODULE=1 make hol.sh - HOLLIGHT_USE_MODULE=1 make - ''; - installPhase = '' - mkdir -p "$out/lib/hol_light" - cp -a . $out/lib/hol_light - sed "s^__DIR__^$out/lib/hol_light^g; s^__USE_MODULE__^1^g" hol_4.14.sh > hol.sh - mv hol.sh $out/lib/hol_light/ - ''; -}) +# To pin a specific upstream revision instead of nixpkgs' hol_light, comment +# out `pkgs.hol_light` below and uncomment the override, adjusting +# `version`/`rev`/`hash`. + +{ pkgs }: + +pkgs.hol_light + +# pkgs.hol_light.overrideAttrs (old: rec { +# version = "unstable-2026-04-17"; +# src = pkgs.fetchFromGitHub { +# owner = "jrh13"; +# repo = "hol-light"; +# rev = "af5d20e033025a9f30a490d9c39edace632405a3"; +# hash = "sha256-R5hSHguVu7YPP7bnFJQ1Prc8Yy3L41LAB20LfEr/RUw="; +# }; +# }) diff --git a/nix/legacy/default.nix b/nix/legacy/default.nix index eae69da10..3afe04980 100644 --- a/nix/legacy/default.nix +++ b/nix/legacy/default.nix @@ -41,6 +41,7 @@ in clang15 = pkgs-2405.clang_15; clang16 = pkgs-2405.clang_16; clang17 = pkgs-2405.clang_17; + clang18 = pkgs-2405.clang_18; }; zigs = { diff --git a/nix/slothy/default.nix b/nix/slothy/default.nix index aae03aac4..1546398dd 100644 --- a/nix/slothy/default.nix +++ b/nix/slothy/default.nix @@ -2,50 +2,21 @@ # Copyright (c) The mldsa-native project authors # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT -{ stdenvNoCC -, fetchFromGitHub -, python3 -, pkgs -, llvm -, gcc -}: +# slothy is packaged in nixpkgs (>= 26.05) and used by default. +# +# To pin a specific upstream revision instead, comment out `pkgs.slothy` +# below and uncomment the override, adjusting `version`/`sha256`. -let - pythonEnv = python3.withPackages (ps: with ps; [ - ortools - sympy - unicorn - ]); -in -stdenvNoCC.mkDerivation rec { - pname = "slothy-cli"; - version = "08ead1f2e5d07617025e00152d1a701fb1195eb9"; - src = fetchFromGitHub { - owner = "slothy-optimizer"; - repo = "slothy"; - rev = version; - sha256 = "sha256-yZ4ZW2S946VJUNNHlO4hFBNpPfIJpCjNbaWTiLmz/Js="; - }; +{ pkgs }: - nativeBuildInputs = [ pkgs.makeWrapper ]; - dontConfigure = true; +pkgs.slothy - installPhase = '' - mkdir -p $out/bin - cp slothy-cli $out/bin/ - cp -r slothy $out/bin - wrapProgram $out/bin/slothy-cli \ - --set DYLD_LIBRARY_PATH ${pythonEnv}/lib \ - --set PYTHONPATH ${pythonEnv}/bin \ - --run exec - ''; - - dontStrip = true; - noAuditTmpdir = true; - propagatedBuildInputs = [ pythonEnv llvm gcc ]; - - meta = { - description = "Slothy: assembly-level superoptimizer"; - homepage = "https://slothy-optimizer.github.io/slothy/"; - }; -} +# pkgs.slothy.overrideAttrs (old: rec { +# version = "6d35cc147a0859f53f8bfc0d0f2ea3b947c8c4eb"; +# src = pkgs.fetchFromGitHub { +# owner = "slothy-optimizer"; +# repo = "slothy"; +# rev = version; +# sha256 = "sha256-TplnMBjNvY7f8RTOwRWcv+cqxcRZ8KHx6toczNC5QGo="; +# }; +# }) diff --git a/nix/util.nix b/nix/util.nix index 8babbfb86..22c09b7db 100644 --- a/nix/util.nix +++ b/nix/util.nix @@ -2,7 +2,7 @@ # Copyright (c) The mldsa-native project authors # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT -{ pkgs, cbmc, bitwuzla, z3, python3-for-slothy }: +{ pkgs, cbmc, bitwuzla, z3 }: rec { glibc-join = p: p.buildPackages.symlinkJoin { name = "glibc-join"; @@ -22,6 +22,14 @@ rec { then pkgs.clang else wrap-gcc pkgs; + pythonEnv = pkgs.python3.withPackages (ps: with ps; [ + mpmath + sympy + pyparsing + pyyaml + rich + ]); + # cross is for determining whether to install the cross toolchain dependencies or not _toolchains = { cross ? true }: let @@ -46,11 +54,10 @@ rec { # 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 ] + ++ [ pythonEnv ] ++ builtins.attrValues { - inherit (pkgs.python3Packages) sympy pyyaml; inherit (pkgs) - gnumake - python3; + gnumake; }; # NOTE: idiomatic nix way of properly setting the $CC in a nix shell @@ -78,22 +85,20 @@ rec { # some customized packages linters = pkgs.symlinkJoin { name = "pqcp-linters"; - paths = builtins.attrValues { - inherit (pkgs.llvmPackages) - clang-tools - bintools; - - inherit (pkgs) - nixpkgs-fmt - shfmt - shellcheck - actionlint - doxygen - ruff; - - inherit (pkgs.python3Packages) - mpmath sympy pyparsing pyyaml rich; - }; + paths = builtins.attrValues + { + inherit (pkgs.llvmPackages) + clang-tools + bintools; + + inherit (pkgs) + nixpkgs-fmt + shfmt + shellcheck + actionlint + doxygen + ruff; + } ++ [ pythonEnv ]; }; cbmc_pkgs = pkgs.callPackage ./cbmc { @@ -104,7 +109,7 @@ rec { hol_light' = pkgs.callPackage ./hol_light { }; hol_server = pkgs.callPackage ./hol_light/hol_server.nix { inherit hol_light'; }; s2n_bignum = pkgs.callPackage ./s2n_bignum { }; - slothy = pkgs.callPackage ./slothy { python3 = python3-for-slothy; }; + slothy = pkgs.callPackage ./slothy { }; pqmx = pkgs.callPackage ./pqmx { }; # Helper function to build individual cross toolchains @@ -112,12 +117,11 @@ rec { let common_deps = builtins.attrValues { - inherit (pkgs.python3Packages) sympy pyyaml; inherit (pkgs) gnumake - python3 qemu; - } ++ pkgs.lib.optionals (pkgs.stdenv.isDarwin) [ pkgs.git ]; + } ++ [ pythonEnv ] + ++ pkgs.lib.optionals (pkgs.stdenv.isDarwin) [ pkgs.git ]; in pkgs.symlinkJoin { name = "toolchain-${name}"; diff --git a/scripts/autogen b/scripts/autogen index b74ad4147..3f03b1547 100755 --- a/scripts/autogen +++ b/scripts/autogen @@ -497,7 +497,7 @@ class CondParser: def parse_condition(self, exp, simplify=True): try: - exp = self.parser.parseString(exp, parseAll=True).as_list()[0] + exp = self.parser.parse_string(exp, parse_all=True).as_list()[0] except pp.ParseException: print(f"WARNING: Ignoring condition '{exp}' I cannot parse") return exp @@ -1975,10 +1975,9 @@ def gen_macro_undefs(extra_notes=None): yield "" yield "#if !defined(MLD_CONFIG_MONOBUILD_KEEP_SHARED_HEADERS)" yield from gen_monolithic_undef_all_core( - filt=lambda c: not native(c) - and k_generic(c) - and not fips202(c) - and "cbmc.h" not in c, + filt=lambda c: ( + not native(c) and k_generic(c) and not fips202(c) and "cbmc.h" not in c + ), desc="MLD_CONFIG_PARAMETER_SET-generic files", ) # Handle cbmc.h manually -- most #define's therein are only defined when CBMC is set