HOL Light folder

[arademaker]

s2n-bignum/arm/Makefile

Line 450 in 67c5c23

HOLDIR?=$(HOME)/hol-light

When HOL Light is installed via opam, following the directions from https://hol-light.github.io

opam install hol_light
opam install hol_light hol_light_module 

HOL Light is installed in

% which hol.sh
/Users/ar/.opam/4.14.2/bin/hol.sh

and the HOLLIGHT_DIR is set to /Users/$HOME/.opam/4.14.2/lib/hol_light, see the first 4 lines of the hol.sh

[arademaker]

Not clear what would be the best solution. I tried to manually solve my problem changing the Makefile to:

# HOLDIR?=$(HOME)/hol-light
# HOLLIGHT:=$(HOLDIR)/hol.sh
HOLDIR?=$(HOME)/.opam/4.14.2/lib/hol_light
HOLLIGHT=$(HOME)/.opam/4.14.2/bin/hol.sh

but I still have a warning in the make tutorial

% make tutorial
../tools/build-proof.sh "tutorial/bignum.ml" "/Users/ar/.opam/4.14.2/bin/hol.sh" "tutorial/bignum.native"
hol_lib.cmxa does not exist in HOLLIGHT_DIR('/Users/ar/.opam/4.14.2/bin').
Did you compile HOL Light with HOLLIGHT_USE_MODULE set to 1?
make: *** [tutorial/bignum.native] Error 1

See that HOLLIGHT_DIR was resolved to the location of the hol.sh because of this. But it is located in the bin folder inside the .opam, and the remain files of HOL Light are located in the lib folder.