Merge pull request #93 from aqjune/makehol

Add `make hol.sh` that creates `hol.sh` running `ocaml` initialized with `hol.ml`

.github/workflows/main.yml

@@ -37,7 +37,7 @@ jobs:
           cd hol-light
           eval $(opam env)
           make
-          ocaml -I `camlp5 -where` camlp5o.cma -init "hol.ml" | tee log.txt
+          ./hol.sh | tee log.txt
           ! grep "Error" log.txt
 
   test2:
@@ -62,6 +62,5 @@ jobs:
           cd hol-light
           eval $(opam env)
           make
-          ocamlmktop -o ocaml-hol
-          ./ocaml-hol -init "hol.ml" | tee log.txt
+          ./hol.sh | tee log.txt
           ! grep "Error" log.txt

.gitignore

@@ -1,7 +1,10 @@
 .DS_Store
+_opam
 *.cmi
 *.cmo
 *.o
 *.cmx
 pa_j.ml
-update_database.ml
+update_database.ml
+ocaml-hol
+hol.sh

Makefile

@@ -35,7 +35,7 @@ CAMLP5_VERSION=`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-'
 
 # Main target
 
-default: update_database.ml pa_j.cmo;
+default: update_database.ml pa_j.cmo hol.sh;
 
 # Choose an appropriate "update_database.ml" file
 
@@ -85,6 +85,20 @@ pa_j.ml: pa_j_3.07.ml pa_j_3.08.ml pa_j_3.09.ml pa_j_3.1x_5.xx.ml pa_j_3.1x_6.xx
         else cp pa_j_3.1x_${CAMLP5_BINARY_VERSION}.xx.ml pa_j.ml; \
         fi
 
+# Create a bash script 'hol.sh' that loads 'hol.ml' in OCaml REPL.
+
+hol.sh: pa_j.cmo ${HOLSRC} update_database.ml
+	if [ `uname` = "Linux" ] || [ `uname` = "Darwin" ] ; then \
+		ocamlmktop -o ocaml-hol nums.cma ; \
+		if test ${OCAML_VERSION} = "4.14" ; \
+		then sed "s^__DIR__^`pwd`^g" hol_4.14.sh > hol.sh ; \
+		else sed "s^__DIR__^`pwd`^g" hol_4.sh > hol.sh ; \
+		fi ; \
+		chmod +x hol.sh ; \
+	else \
+		echo 'FAILURE: hol.sh assumes Linux' ; \
+	fi
+
 # TODO: update this and hol.* commands to use one of checkpointing  tools
 # other than ckpt.
 # Build a standalone hol image called "hol" (needs Linux and ckpt program)
@@ -136,13 +150,12 @@ hol.complex: ./hol.multivariate                                         \
         echo -e 'loadt "Multivariate/complexes.ml";;\nloadt "Multivariate/canal.ml";;\nloadt "Multivariate/transcendentals.ml";;\nloadt "Multivariate/realanalysis.ml";;\nloadt "Multivariate/cauchy.ml";;\nloadt "Multivariate/complex_database.ml";;\nloadt "update_database.ml";;\nself_destruct "Preloaded with multivariate-based complex analysis";;' | ./hol.multivariate; mv hol.snapshot hol.complex;
 
 # Build all those
-
-all: hol hol.multivariate hol.sosa hol.card hol.complex;
+all: hol.sh hol hol.multivariate hol.sosa hol.card hol.complex;
 
 # Build binaries and copy them to binary directory
 
-install: hol hol.multivariate hol.sosa hol.card hol.complex; cp hol hol.multivariate hol.sosa hol.card hol.complex ${BINDIR}
+install: hol.sh hol hol.multivariate hol.sosa hol.card hol.complex; cp hol hol.multivariate hol.sosa hol.card hol.complex ${BINDIR}
 
 # Clean up all compiled files
 
-clean:; rm -f update_database.ml pa_j.ml pa_j.cmi pa_j.cmo hol hol.multivariate hol.sosa hol.card hol.complex;
+clean:; rm -f update_database.ml pa_j.ml pa_j.cmi pa_j.cmo ocaml-hol hol.sh hol hol.multivariate hol.sosa hol.card hol.complex;

README

@@ -140,36 +140,28 @@ be available for some platforms. First the basic approach:
 
       export CAMLP5LIB=$HOME/mylib/ocaml/camlp5
 
-(2) Do 'ocaml'. (Actually for OCaml >= 4.02 I prefer 'ocaml -safe-string'
-    to avoid mutable strings, while you may need something else like
-    'ocamlnum' on some platforms --- see [*] below.) You should see a
-    prompt, something like:
+(2) If you are using a Unix-like environment, simply run `./hol.sh`.
+    This should rebuild all the core HOL Light theories, and terminate after
+    a few minutes with the usual OCaml prompt, something like:
 
-                Objective Caml version 4.01.0
+                Camlp5 parsing version (HOL-Light) 8.02.00
 
         #
 
+    HOL Light is now ready for the user to start proving theorems.
+
+    If you are not using a Unix-like environment, do
+    'ocaml'. (Actually for OCaml >= 4.02 I prefer 'ocaml -safe-string'
+    to avoid mutable strings, while you may need something else like
+    'ocamlnum' on some platforms --- see [*] below.)
     If you are using OCaml 4.14, you need to create a top-level OCaml
     using 'ocamlmktop -o ocaml-hol' and use 'ocaml-hol' because the default
     'ocaml' does not have 'compiler-libs' that is necessary to run HOL Light.
 
-(3) At the OCaml prompt '#', do '#use "hol.ml";;' (the '#' is part of the
-    command, not the prompt) followed by a newline. This should rebuild
-    all the core HOL Light theories, and terminate after a few minutes
-    with the usual OCaml prompt, something like:
-
-        val search : term list -> (string * thm) list = <fun>
-        - : unit = ()
-        File "help.ml" already loaded
-        - : unit = ()
-        - : unit = ()
-        - : unit = ()
-                Camlp5 parsing version 7.03
-
-        #
+    At the OCaml prompt '#', do '#use "hol.ml";;' (the '#' is part of the
+    command, not the prompt) followed by a newline.
 
-    HOL Light is now ready for the user to start proving theorems. You
-    can also use the load process (2) and (3) in other directories, but
+    You can also use the load process (2) in other directories, but
     you should either set the environment variable HOLLIGHT_DIR to point
     to the directory containing the HOL source files, or change the
     first line of "hol.ml" to give that explicitly, from

hol_4.14.sh

@@ -0,0 +1,9 @@
+#!/bin/bash
+
+# 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.
+
+# Makefile will replace __DIR__ with the path
+export HOLLIGHT_DIR=__DIR__
+${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -init ${HOLLIGHT_DIR}/hol.ml -safe-string

hol_4.sh

@@ -0,0 +1,9 @@
+#!/bin/bash
+
+# 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.
+
+# Makefile will replace __DIR__ with the path
+export HOLLIGHT_DIR=__DIR__
+${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -I `camlp5 -where` camlp5o.cma -init ${HOLLIGHT_DIR}/hol.ml -safe-string