From 9cb9ec9c21bf6deae6ef476efe1ddc7046b35630 Mon Sep 17 00:00:00 2001
From: Hanno Becker <beckphan@amazon.co.uk>
Date: Wed, 31 Dec 2025 05:24:01 +0000
Subject: [PATCH] nix: Add HOL-Light cross shells

As a first step towards developing and checking HOL-Light proofs
for architectures different from the host architecture, this
commit adds new nix shells for HOL-Light + cross toolchains.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
---
 flake.nix | 25 +++++++++++++++----------
 1 file changed, 15 insertions(+), 10 deletions(-)

diff --git a/flake.nix b/flake.nix
index 0b9c73fd5d..d1d6d3c407 100644
--- a/flake.nix
+++ b/flake.nix
@@ -41,6 +41,10 @@
                 '')
             ];
           };
+          holLightShellHook = ''
+            export PATH=$PWD/scripts:$PATH
+            export PROOF_DIR="$PWD/proofs/hol_light"
+          '';
         in
         {
           _module.args.pkgs = import inputs.nixpkgs {
@@ -95,16 +99,17 @@
 
           devShells.avr = util.mkShell (import ./nix/avr { inherit pkgs; });
           devShells.hol_light = (util.mkShell {
-            packages = builtins.attrValues {
-              inherit (config.packages) linters hol_light s2n_bignum;
-            };
-          }).overrideAttrs (old: {
-            shellHook = ''
-              export PATH=$PWD/scripts:$PATH
-              # Set PROOF_DIR based on where we entered the shell
-              export PROOF_DIR="$PWD/proofs/hol_light"
-            '';
-          });
+            packages = builtins.attrValues { inherit (config.packages) linters hol_light s2n_bignum; };
+          }).overrideAttrs (old: { shellHook = holLightShellHook; });
+          devShells.hol_light-cross = (util.mkShell {
+            packages = builtins.attrValues { inherit (config.packages) linters toolchains hol_light s2n_bignum; };
+          }).overrideAttrs (old: { shellHook = holLightShellHook; });
+          devShells.hol_light-cross-aarch64 = (util.mkShell {
+            packages = builtins.attrValues { inherit (config.packages) linters toolchain_aarch64 hol_light s2n_bignum; };
+          }).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; };
+          }).overrideAttrs (old: { shellHook = holLightShellHook; });
           devShells.ci = util.mkShell {
             packages = builtins.attrValues { inherit (config.packages) linters toolchains_native; };
           };