chore: improve HOL Light path detection and update gitignore by arademaker · Pull Request #336 · awslabs/s2n-bignum

arademaker · 2026-01-09T18:45:55Z

Issue #335

Description of changes:

Use which hol.sh and hol.sh -dir to detect HOL Light installation
Support both git installations and opam package installations
Add .DS_Store to gitignore for macOS compatibility

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

- Use `which hol.sh` and `hol.sh -dir` to detect HOL Light installation - Support both git installations and opam package installations - Add .DS_Store to gitignore for macOS compatibility

Copilot

Pull request overview

This PR improves HOL Light path detection by using which hol.sh and hol.sh -dir to support both git installations and opam package installations. It also adds .DS_Store to gitignore for macOS compatibility.

Key changes:

Modified HOL Light detection to query hol.sh directly for installation path
Updated .gitignore to exclude macOS-specific .DS_Store files

Reviewed changes

Copilot reviewed 2 out of 3 changed files in this pull request and generated 5 comments.

File	Description
tools/build-proof.sh	Updated to use `hol.sh -dir` to query the actual HOLLIGHT_DIR location, supporting both git and opam installations
arm/Makefile	Changed HOLLIGHT detection to use `which hol.sh` instead of hardcoded path
.gitignore	Added `.DS_Store` pattern to ignore macOS system files

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-01-09T18:49:58Z

arm/Makefile

-HOLDIR?=$(HOME)/hol-light
-HOLLIGHT:=$(HOLDIR)/hol.sh
+HOLLIGHT=$(shell which hol.sh)
+HOLDIR?=$(${HOLLIGHT} -dir)


The variable HOLDIR is defined but never used anywhere in the Makefile. Only HOLLIGHT is referenced in the build rules. This variable definition appears to be unnecessary and can be removed, or if it's intended for future use or external consumption, this should be documented.

Suggested change

HOLDIR?=$(${HOLLIGHT} -dir)

Copilot · 2026-01-09T18:49:59Z

arm/Makefile


-HOLDIR?=$(HOME)/hol-light
-HOLLIGHT:=$(HOLDIR)/hol.sh
+HOLLIGHT=$(shell which hol.sh)


If which hol.sh fails to find hol.sh in the PATH, HOLLIGHT will be empty, which will cause cryptic errors later when the build rules try to use it. Consider adding an error check after this line or providing a more helpful error message when HOLLIGHT is not found.

Suggested change

HOLLIGHT=$(shell which hol.sh)

HOLLIGHT?=$(shell which hol.sh 2>/dev/null)

ifeq ($(HOLLIGHT),)

$(error hol.sh not found in PATH. Please install HOL Light and ensure hol.sh is on your PATH, or set HOLLIGHT to the hol.sh path.)

endif

Copilot · 2026-01-09T18:49:59Z

arm/Makefile

+HOLLIGHT=$(shell which hol.sh)
+HOLDIR?=$(${HOLLIGHT} -dir)


The x86/Makefile still uses the old HOL Light detection approach (HOLDIR?=$(HOME)/hol-light). For consistency and to support both git installations and opam package installations, the x86/Makefile should be updated to use the same approach as this arm/Makefile (using which hol.sh and hol.sh -dir).

Copilot · 2026-01-09T18:49:59Z

arm/Makefile

-HOLDIR?=$(HOME)/hol-light
-HOLLIGHT:=$(HOLDIR)/hol.sh
+HOLLIGHT=$(shell which hol.sh)
+HOLDIR?=$(${HOLLIGHT} -dir)


The syntax for the shell command is incorrect. In Makefiles, you should use $(HOLLIGHT) instead of ${HOLLIGHT} when invoking shell commands with $(shell ...). The current syntax will not properly expand the variable.

Suggested change

HOLDIR?=$(${HOLLIGHT} -dir)

HOLDIR?=$(shell $(HOLLIGHT) -dir)

not relevant, since the HOLDIR variable was removed.

Copilot · 2026-01-09T18:49:59Z

tools/build-proof.sh

 output_path=${s2n_bignum_arch}/$3

-export HOLLIGHT_DIR="$(dirname ${hol_sh_cmd})"
+# Query hol.sh for the actual HOLLIGHT_DIR location This works for


Missing period at the end of the first sentence. The comment should read "Query hol.sh for the actual HOLLIGHT_DIR location." with a period after "location".

Suggested change

# Query hol.sh for the actual HOLLIGHT_DIR location This works for

# Query hol.sh for the actual HOLLIGHT_DIR location. This works for

… does not require HOL Light by default (it only builds assembly files)

aqjune-aws · 2026-01-12T15:23:00Z

Hi Alexandre, thank you for writing a pull request! I added minor commits that make the Github Action tests pass.
Would you mind if the default path is set to the hol-light in the HOME directory ($(HOME)/hol-light) if hol.sh is absent from PATH? This was a useful setting for many of us (Amazon internal users) using s2n-bignum.
Another comment is that I found there was a short paragraph mentioning HOLDIR in the README file in the root directory, which was kind of obscure that I also missed that part at the first time :/ Do you want to edit the README file as well?

- presents OPAM installation as the recommended option with the specific commands - keeps source installation as an alternative for those who prefer it - removes the outdated warning about OPAM not working - removes the HOLDIR environment variable reference (since the build system now uses `hol.sh -dir` automatically) - emphasizes that hol.sh must be in PATH (which is how the Makefiles discover HOL Light via `which hol.sh`)

arademaker · 2026-01-16T11:16:10Z

Hi @aqjune-aws , I have updated the README. I preserved the option to install HOL Light from source, but I now make it clear that HOL Light can be installed with OCaml 5.2 using OPAM, and that it works fine. I believe this is the easier way to install HOL Light.

Would you mind if the default path is set to the hol-light in the HOME directory ($(HOME)/hol-light) if hol.sh is absent from PATH?

I don't want to impose any particular solution! Please take all my comments as suggestions.

First, the HOL Light folder is named HOLLIGHT_DIR in the tools/build-proof.sh but also referenced as HOLDIR in the arm/Makefile and x86/Makefile and in two YML files in the codebuild folder. Maybe we can fix this tiny inconsistency later.

I didn't really test this comment in the Makefiles. I guess we need to remove it now since HOLDIR is not defined in the Makefiles.

# If you build hol-light yourself (see https://github.com/jrh13/hol-light)
# in your home directory, and do "make" inside the subdirectory hol-light,
# then the following HOLDIR setting should be right:

I haven't tried HOL Light from the source installation, but I guess the command hol.sh -dir will work and will give back the proper folder containing the HOL Light files. So this will never fail if hol.sh is found.

So the question is: what should the default location of hol.sh be if which hol.sh doesn't find it? I assume in the README that hol.sh needs to be in the PATH. I am not sure if having an alternative default location will make the installation more or less robust. Once more, take my words only as suggestions. I don't want to introduce too much noise here. If you think another option is better, that's fine with me. It took me some time to understand the problem I was dealing with. I guess someone without HOL Light experience would run into the same issues I did.

Let me know what do you prefer. I would replace this comment above from the Makfiles with somethink like:

Make sure your hol.sh is in the PATH. It can be either in the $HOME/hol-light/ if you installed it from source or at $HOME/.opam/ocaml-5.2/bin if you installed it with OPAM (see README)

aqjune-aws · 2026-01-17T04:25:00Z

Hi Alexandre,

So the question is: what should the default location of hol.sh be if which hol.sh doesn't find it? I assume in the README that hol.sh needs to be in the PATH. I am not sure if having an alternative default location will make the installation more or less robust.

Yes, indeed this is more for backward compatibility. I think the new update of using which hol.sh is great and would like to recommend this for anyone who newly clones s2n-bignum.

--

Another comment is - could you slightly update the doc to recommend the latest HOL Light than the OPAM version? It is because to run the full proofs (make proofs) the features in latest HOL Light is necessary. :) For example, without a commit in 2025 Nov: jrh13/hol-light@b9a430b a few proofs will break.
I think there is still a great value in explaining how to use OPAM based HOL Light, because tutorials and many proofs will still pass with it, enabling quick tour of s2n-bignum. So I think having both OPAM and git clone-based installation manual makes sense. It is just about which one to recommend more.
The Github Action file (.github/workflows/ci.yml) mentions exactly which HOL Light commit hash is being used to test the whole proofs, but the HOL Light more recent than the commit hash must always support the proofs.

arademaker · 2026-01-19T11:37:02Z

README updated to make clear that OPAM installation is the easier option, but the GitHub clone-based approach is recommended.

What may confuse people is that at https://github.com/jrh13/hol-light/, the latest release is HOL-Light-3.1.0, whereas on https://opam.ocaml.org/packages/hol_light/, the OPAM package appears to use the same latest HOL Light release, 3.1.0. Moreover, in https://github.com/jrh13/hol-light, OPAM is the first recommended approach for installing HOL Light. Both versions, from OPAM and from source, finished the loading of the files with the same message (before the REPL: "Camlp5 parsing version (HOL-Light) 8.03.06" and both have the same version at the beginning of the hol.ml file.

I didn't install the tools to build a standalone image. That may be the only big difference between the two versions.

chore: improve HOL Light path detection and update gitignore

c6545f9

- Use `which hol.sh` and `hol.sh -dir` to detect HOL Light installation - Support both git installations and opam package installations - Add .DS_Store to gitignore for macOS compatibility

Copilot AI review requested due to automatic review settings January 9, 2026 18:45

Copilot started reviewing on behalf of arademaker January 9, 2026 18:46 View session

Copilot AI reviewed Jan 9, 2026

View reviewed changes

arademaker mentioned this pull request Jan 9, 2026

make proofs fails in MacOS #337

Closed

arademaker and others added 4 commits January 9, 2026 16:00

fix: issues reported by Copilot

884dfec

Merge branch 'main' into issue-335

dd5b264

Fix Github Action

1d39cd0

Postpone checking HOLLIGHT to build-proof.sh because the make command…

5c3975e

… does not require HOL Light by default (it only builds assembly files)

aqjune-aws added 2 commits January 16, 2026 16:55

Merge branch 'main' into issue-335

4dda2fd

Fix the new proof check

5595a20

update README to recommend HOL Light from github instead of OPAM

f2a93c4

-HOLLIGHT=$(shell which hol.sh)
+HOLLIGHT?=$(shell which hol.sh 2>/dev/null)
+ifeq ($(HOLLIGHT),)
+$(error hol.sh not found in PATH. Please install HOL Light and ensure hol.sh is on your PATH, or set HOLLIGHT to the hol.sh path.)
+endif

	HOLDIR?=$(${HOLLIGHT} -dir)
	HOLDIR?=$(shell $(HOLLIGHT) -dir)

	# Query hol.sh for the actual HOLLIGHT_DIR location This works for
	# Query hol.sh for the actual HOLLIGHT_DIR location. This works for

Conversation

arademaker commented Jan 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

arademaker Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

arademaker Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

arademaker Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

arademaker Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

arademaker Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

aqjune-aws commented Jan 12, 2026

Uh oh!

arademaker commented Jan 16, 2026

Uh oh!

aqjune-aws commented Jan 17, 2026

Uh oh!

arademaker commented Jan 19, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

arademaker commented Jan 9, 2026 •

edited

Loading