From 8d12187daff4e52037fbd252a94d7cef2933a91c Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Sat, 20 Apr 2024 23:17:19 -0500 Subject: [PATCH] Add `make switch` fore easy installation of dependencies This patch adds `make switch` that - Creates a local OPAM switch under the current hol-light directory - Chooses the latest OCaml version (4.14 for now; would be great if it is 5.0 in the future!) - And installs dependencies that are needed by HOL Light. This is to help beginners set the environment for HOL Light. I also updated README to explain(recommend) this option. A separate 'DEPENDENCIES' chapter is added to explain the original, detailed steps. --- Makefile | 9 ++++ README | 137 +++++++++++++++++++++++++++------------------------- hol_4.14.sh | 13 ++++- hol_4.sh | 11 ++++- 4 files changed, 100 insertions(+), 70 deletions(-) diff --git a/Makefile b/Makefile index 831610e6..1167d0c7 100644 --- a/Makefile +++ b/Makefile @@ -37,6 +37,15 @@ CAMLP5_VERSION=`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' default: update_database.ml pa_j.cmo hol.sh; +# Create a local OPAM switch and install dependencies on it. +# This will use the latest OCaml version that fully supports features of +# HOL Light. +# ledit is installed for line editing of OCaml REPL +switch:; \ + opam switch create . ocaml-base-compiler.4.14.0 ; \ + eval $(opam env) ; \ + opam install -y zarith camlp5 ledit + # Choose an appropriate "update_database.ml" file update_database.ml:; if [ ${OCAML_VERSION} = "4.14" ] ; \ diff --git a/README b/README index b97ca05e..39d883c0 100644 --- a/README +++ b/README @@ -24,23 +24,10 @@ Refer to the reference manual for more details of individual functions: INSTALLATION -If you use Debian Linux or some other Debian-based Linux distribution -(Knoppix, Mint, Ubuntu, etc.), there is actually a "hol-light" package, -thanks to Hendrik Tews, so installation of HOL Light and all its -prerequisites is as simple as - - sudo apt-get install hol-light - -For other OSs, more work is involved. The Objective CAML (OCaml) -implementation is a prerequisite for running HOL Light. HOL Light -should work with any recent version of OCaml; I've tried it on at -least 3.04, 3.06, 3.07+2, 3.08.1, 3.09.3, 3.10.0, 3.11.2, 4.00, -4.05 and 4.14. -However, for versions >= 3.10 (in 3.10 there was an incompatible -change in the camlp4 preprocessor) you will also need to get camlp5 -(version >= 4.07). For versions >= 4.14, you will need to get camlp5 -8.00 and ocamlfind. Installing these items should not be -too difficult, depending on the platform. +The Objective CAML (OCaml) implementation is a prerequisite for running +HOL Light. HOL Light should work with any recent version of OCaml; I've +tried it on at least 3.04, 3.06, 3.07+2, 3.08.1, 3.09.3, 3.10.0, 3.11.2, +4.00, 4.05 and 4.14. 1. OCaml: there are packages for many Linux distributions. For example, on a debian derivative like Ubuntu, you may just need @@ -54,58 +41,17 @@ too difficult, depending on the platform. http://caml.inria.fr/ocaml/index.en.html - 2. zarith or num: The HOL Light system uses the OCaml "Num" library - or "Zarith" library for rational arithmetic. If OCaml 4.14 is used, - HOL Light will use Zarith. You can install it using the OCaml package - manager "opam" by - - opam install zarith - - If OCaml 4.05 is used, HOL Light will use Num which is included in - the core system. If you are using an OCaml version between 4.06 and 4.13, - Num must be installed separately because it is no longer included in - the core system. You can use "opam" by - - opam install num - - Alternatively you can download the sources from here + 2. Dependencies: HOL Light uses camlp5 and zarith (num for OCaml + version < 4.14). If you have OPAM installed on your machine, + running the following command inside this directory will create a local + OPAM switch which uses the latest OCaml version that fully supports + features of as well as all dependencies installed: - https://github.com/ocaml/num + make switch + eval $(opam env) - and build and install them following the instructions on that - page, for example - - git clone https://github.com/ocaml/num mynums - cd mynums - make all - sudo make install [assuming no earlier errors] - - 3. camlp5: this is needed to run HOL Light under any OCaml >= 3.10. - Somtimes you need a recent version of camlp5 to be compatible with - your OCaml. For example, OCaml 4.05 is compatible with camlp5 7.10 and - OCaml 4.14 is compatible with camlp5 8.02. I recommend downloading - the sources for a recent version from - - https://github.com/camlp5/camlp5/releases ('tags' tab has full series) - - and building it in "strict" mode before installing it, thus: - - cd software/camlp5-rel701 [or wherever you unpacked sources to] - ./configure --strict - make - sudo make install [assuming no earlier errors] - - There are also packages for camlp5, so you may be able to get away - with just something like - - sudo apt-get install camlp5 - - or - - opam pin add camlp5 - - However, you may get a version in "transitional" instead of - "strict" mode (do "camlp5 -pmode" to check which you have). + To manually install dependencies, the DEPENDENCIES chapter of this document + explains it. Now for HOL Light itself. The instructions below assume a Unix-like environment such as Linux [or Cygwin (see www.cygwin.com) under @@ -255,6 +201,63 @@ kind of thing that might be done, or may be useful in further work. Thanks to Carl Witty for help with Camlp4 porting and advice on checkpointing programs. + * * * * * * * * + + DEPENDENCIES + + 1. zarith or num: The HOL Light system uses the OCaml "Num" library + or "Zarith" library for rational arithmetic. If OCaml 4.14 is used, + HOL Light will use Zarith. You can install it using the OCaml package + manager "opam" by + + opam install zarith + + If OCaml 4.05 is used, HOL Light will use Num which is included in + the core system. If you are using an OCaml version between 4.06 and 4.13, + Num must be installed separately because it is no longer included in + the core system. You can use "opam" by + + opam install num + + Alternatively you can download the sources from here + + https://github.com/ocaml/num + + and build and install them following the instructions on that + page, for example + + git clone https://github.com/ocaml/num mynums + cd mynums + make all + sudo make install [assuming no earlier errors] + + 2. camlp5: this is needed to run HOL Light under any OCaml >= 3.10. + Somtimes you need a recent version of camlp5 to be compatible with + your OCaml. For example, OCaml 4.05 is compatible with camlp5 7.10 and + OCaml 4.14 is compatible with camlp5 8.02. I recommend downloading + the sources for a recent version from + + https://github.com/camlp5/camlp5/releases ('tags' tab has full series) + + and building it in "strict" mode before installing it, thus: + + cd software/camlp5-rel701 [or wherever you unpacked sources to] + ./configure --strict + make + sudo make install [assuming no earlier errors] + + There are also packages for camlp5, so you may be able to get away + with just something like + + sudo apt-get install camlp5 + + or + + opam pin add camlp5 + + However, you may get a version in "transitional" instead of + "strict" mode (do "camlp5 -pmode" to check which you have). + * * * * * * * * [*] HOL Light uses the OCaml 'num' library for multiple-precision diff --git a/hol_4.14.sh b/hol_4.14.sh index 5eb72ecd..95bc44ae 100755 --- a/hol_4.14.sh +++ b/hol_4.14.sh @@ -2,8 +2,17 @@ # The default ocaml REPL does not accept arrow keys. # Export LINE_EDITOR to a proper program to enable this before invoking this -# script. ledit and rlwrap are good candidates. +# script. If not set, ledit will be used. +if [ "${LINE_EDITOR}" == "" ]; then + LINE_EDITOR="ledit" +fi # Makefile will replace __DIR__ with the path export HOLLIGHT_DIR=__DIR__ -${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -init ${HOLLIGHT_DIR}/hol.ml -safe-string + +# If a local OPAM is installed, use it +if [ -d "${HOLLIGHT_DIR}/_opam" ]; then + eval $(opam env --switch "${HOLLIGHT_DIR}/" --set-switch) +fi + +${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -init ${HOLLIGHT_DIR}/hol.ml diff --git a/hol_4.sh b/hol_4.sh index f60043b9..a475fe5d 100755 --- a/hol_4.sh +++ b/hol_4.sh @@ -2,8 +2,17 @@ # The default ocaml REPL does not accept arrow keys. # Export LINE_EDITOR to a proper program to enable this before invoking this -# script. ledit and rlwrap are good candidates. +# script. If not set, ledit will be used. +if [ "${LINE_EDITOR}" == "" ]; then + LINE_EDITOR="ledit" +fi # Makefile will replace __DIR__ with the path export HOLLIGHT_DIR=__DIR__ + +# If a local OPAM is installed, use it +if [ -d "${HOLLIGHT_DIR}/_opam" ]; then + eval $(opam env --switch "${HOLLIGHT_DIR}/" --set-switch) +fi + ${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -I `camlp5 -where` camlp5o.cma -init ${HOLLIGHT_DIR}/hol.ml -safe-string