Installing for Apple/Mac's Unix

[brando90]

how does one install it for MAC OS?

[maggesi]

Hi, I have some instructions for running HOL Light in a Docker container:
https://github.com/maggesi/hol-light-docker

You may want to start with the usage guide:
https://github.com/maggesi/hol-light-docker/blob/master/USAGE.md

Actually, I now use a slightly different method that accommodates for working on a HOL repository on the host system (instead of using a cloned repository on the container). I will eventually update these script before long.

Do not hesitate to give feedback if you try to use it.

[binghe]

Some possible steps: (confirmed on Mac OS X 10.11)

1. Install Macports from https://www.macports.org
2. Install OCaml and related packages: sudo port install ocaml ocaml-num camlp5
3. Clone HOL-Light Git into your local directory.
4. Go to HOL-Light directory and execute make
5. Start OCaml by ocaml (or ocaml -safe-string)
6. Load HOL-Light by #use "hol.ml";; (# is part of the command)
7. Load a theory, e.g. needs "Multivariate/transcendentals.ml";; (it takes a long time)

[brando90]

@binghe hmmm seems I get an error:

(base) brandomiranda~ $ cd hol-light/
(base) brandomiranda~/hol-light $ make
cp update_database_`ocamlc -version | cut -c1`.ml update_database.ml
\
        if test `ocamlc -version | cut -c1-3` = "3.0"  ; \
        then cp pa_j_`ocamlc -version | cut -c1-4`.ml pa_j.ml ; \
        else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -c1` = "7" ; \
             then if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "7.01" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "7.02" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "7.03" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "7.04" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "7.05" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "7.06" ; \
									then cp pa_j_4.xx_7.06.ml pa_j.ml; \
									else cp pa_j_4.xx_7.xx.ml pa_j.ml; \
									fi \
             else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.02.1" ; \
                  then cp pa_j_3.1x_6.02.1.ml pa_j.ml; \
                  else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.02.2" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.02.3" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.03" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.04" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.05" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.06" ; \
                       then cp pa_j_3.1x_6.02.2.ml pa_j.ml; \
                       else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.06" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.07" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.08" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.09" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.10" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.11" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.12" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.13" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.14" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.15" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.16" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.17" ; \
                            then cp pa_j_3.1x_6.11.ml pa_j.ml; \
                            else cp pa_j_3.1x_`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -c1`.xx.ml pa_j.ml; \
                            fi \
                       fi \
                  fi \
             fi \
        fi
if test `ocamlc -version | cut -c1-3` = "3.0" ; \
                   then ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo" -I `camlp4 -where` pa_j.ml ; \
                   else if test `ocamlc -version | cut -c1-3` = "3.1" -o `ocamlc -version | cut -c1-4` = "4.00" -o `ocamlc -version | cut -c1-4` = "4.01"  -o `ocamlc -version | cut -c1-4` = "4.02" -o `ocamlc -version | cut -c1-4` = "4.03" -o `ocamlc -version | cut -c1-4` = "4.04" -o `ocamlc -version | cut -c1-4` = "4.05" ; \
                        then  ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I `camlp5 -where` pa_j.ml ; \
                        else ocamlc -safe-string -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I `camlp5 -where` pa_j.ml ; \
                        fi \
                   fi
File "pa_j.ml", line 806, characters 23-39:
Warning 3: deprecated: String.uppercase
Use String.uppercase_ascii instead.
File "pa_j.ml", line 807, characters 28-44:
Warning 3: deprecated: String.lowercase
Use String.lowercase_ascii instead.
(base) brandomiranda~/hol-light $ ocaml
(base) brandomiranda~/hol-light $ ocaml
        OCaml version 4.06.0

# use "hol.ml";;
Error: Unbound value use

[binghe]

Noticed that # is part of the command. Thus you should see the following text on your screen:

# #use "hol.ml";;

Don't ask why, I also hate OCaml. (I'm Standard ML and HOL4 user.)

[brando90]

Hmmm i did put that at some point...will paste that attempt later. Im stuck with ocaml

…

Sent from my iPhone

On Aug 28, 2019, at 7:04 PM, Chun Tian ***@***.***> wrote: Noticed that # is part of the command. Thus you should see the following in your screen: # #use "hol.ml";; Don't ask why, I also hate OCaml. (I'm Standard ML and HOL4 user.) — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[aqjune-aws]

HOL Light now has make switch which will create a local OPAM switch and install dependency packages in there, as well as hol.sh which encapsulates all details about how to run:

make switch
eval $(opam env)
make
./hol.sh