Merge pull request #569 from pq-code-package/hol_light_interactive

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

Author: mkannwischer

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,21 +2,25 @@
 # 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"
     export HOLLIGHT_DIR="$1/lib/hol_light"
+    export PATH="$1/lib/hol_light:$PATH"
   '';
-  version = "unstable-2024-12-22";
+  version = "unstable-2025-09-22";
   src = fetchFromGitHub {
     owner = "jrh13";
     repo = "hol-light";
-    rev = "0e4b1bd8c7d400214d6fa6027f15a4221b54f8d4";
-    hash = "sha256-M6ddzqoAFyMBmaznuz31+o035xdEz4VXZMHhH4Dm4c8=";
+    rev = "bed58fa74649fa74015176f8f90e77f7af5cf8e3";
+    hash = "sha256-QDubbUUChvv04239BdcKPSU+E2gdSzqAWfAETK2Xtg0=";
   };
-  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