nix: bump to nixpkgs 26.05

.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 || '' }}

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,17 +54,16 @@
             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
         {
           _module.args.pkgs = import inputs.nixpkgs {
             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,15 +198,14 @@
           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;
           devShells.clang22 = util.mkShellWithCC' pkgs.clang_22;
 
           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-

nix/cbmc/default.nix

@@ -36,7 +36,7 @@ buildEnv {
       });
 
       inherit
-        bitwuzla# 0.8.2
+        bitwuzla# 0.9.0
         ninja; # 1.13.2
     };
 }

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=";
+#   };
+# })

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 = {

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=";
+#   };
+# })