HOL-Light: Allow interactive use of hol.sh in the hol_light shell

- Ported from mlkem-native PR #1244
- Previously, while compiling and running the HOL-Light proofs in
  `nix develop .#hol_light` worked, trying to start the interactive
  shell `hol.sh` for proof development would fail. This required
  proof developers to install HOL-Light and s2n-bignum locally,
  both inconvenient and error proone because one would need to keep
  that local version and the nix version in sync.

- This commit adjusts the nix flake to setup HOL-Light in such a way
  that hol.sh can be used interactively inside the `hol_light` shell.
  You can test  for this PR with following in nix hol_light shell:

```
   hol.sh
```

  Now, when you enter the shell via `nix develop .#hol_light`, the
  interactive shell `hol.sh` is in the PATH, and within it, both
  s2n-bignum and proofs/hol_light/arm are added to HOL-Light's own
  search path (`load_path`).

- Note that mldsa-native currently does not have any HOL-Light proofs.
  Therefore, we have not ported the HOL-Light interactive shell tests
  to mldsa-native.

Signed-off-by: willieyz <[email protected]>

Author: willieyz

flake.nix

@@ -93,11 +93,17 @@
                 inherit (pkgs) gcc-arm-embedded qemu coreutils python3 git;
               };
           };
-          devShells.hol_light = util.mkShell {
+          devShells.hol_light = (util.mkShell {
             packages = builtins.attrValues {
-              inherit (config.packages) hol_light s2n_bignum;
+              inherit (config.packages) linters hol_light s2n_bignum;
             };
-          };
+          }).overrideAttrs (old: {
+            shellHook = ''
+              export PATH=$PWD/scripts:$PATH
+              # Set PROOF_DIR_ARM based on where we entered the shell
+              export PROOF_DIR_ARM="$PWD/proofs/hol_light/arm"
+            '';
+          });
           devShells.ci = util.mkShell {
             packages = builtins.attrValues { inherit (config.packages) linters toolchains_native; };
           };

nix/hol_light/0005-Configure-hol-sh-for-mldsa-native.patch

@@ -0,0 +1,48 @@
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+diff --git a/hol_4.14.sh b/hol_4.14.sh
+index 1311255..8b2bc36 100755
+--- a/hol_4.14.sh
++++ b/hol_4.14.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,13 @@ 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)
++
++# Set HOLLIGHT_LOAD_PATH to include S2N_BIGNUM_DIR and mldsa-native proofs
++export HOLLIGHT_LOAD_PATH="${S2N_BIGNUM_DIR}:${PROOF_DIR_ARM}:${HOLLIGHT_LOAD_PATH}"
++
++# Change to mldsa-native proofs directory if set, so define_from_elf can find object files
++[ -n "${PROOF_DIR_ARM}" ] && cd "${PROOF_DIR_ARM}"
++
++${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
+index 0aaa5c7..5adaf4c 100755
+--- 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}

nix/hol_light/0005-Fix-hollight-path.patch

@@ -0,0 +1,13 @@
+# 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 ; \

nix/hol_light/0006-Add-findlib-to-ocaml-hol.patch

@@ -2,7 +2,7 @@
 # Copyright (c) The mldsa-native project authors
 # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-{ hol_light, fetchFromGitHub, writeText, ... }:
+{ hol_light, fetchFromGitHub, writeText, ocamlPackages, ledit, ... }:
 hol_light.overrideAttrs (old: {
   setupHook = writeText "setup-hook.sh" ''
     export HOLDIR="$1/lib/hol_light"
@@ -15,8 +15,11 @@ hol_light.overrideAttrs (old: {
     rev = "0e4b1bd8c7d400214d6fa6027f15a4221b54f8d4";
     hash = "sha256-M6ddzqoAFyMBmaznuz31+o035xdEz4VXZMHhH4Dm4c8=";
   };
-  patches = [ ./0005-Fix-hollight-path.patch ];
-  propagatedBuildInputs = old.propagatedBuildInputs ++ old.nativeBuildInputs;
+  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 = ''
     HOLLIGHT_USE_MODULE=1 make hol.sh
     patchShebangs hol.sh