\( \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} \)
UP | HOME

Compiling HOL Light

Table of Contents

1. OPAM

CAUTION: You will run into problems if you have arm_64=1 in your /boot/config.txt, so before building OPAM, be sure to set arm_64=0 (or remove the line from /boot/config.txt altogether!). (End of caution)

On a Raspberry Pi, simply install OCaml using sudo apt install ocaml.

Then clone and build OPAM: 

alex@rpi:~/$ cd src
alex@rpi:~/src/$ git clone https://github.com/ocaml/opam
...
alex@rpi:~/src/$ cd OPAM
alex@rpi:~/src/OPAM/$ ./configure
alex@rpi:~/src/OPAM/$ make lib-ext
alex@rpi:~/src/OPAM/$ make
alex@rpi:~/src/OPAM/$ sudo make install

Before we finish, we need to also install bubblewrap…because…reasons… 

alex@rpi:~/src/OPAM/$ sudo apt install bubblewrap
alex@rpi:~/src/OPAM/$ cd ~
alex@rpi:~/$ opam init

[default] Initialised

<><> Required setup - please read <><><><><><><><><><><><><><><><><><><><><><><>

  In normal operation, opam only alters files within ~/.opam.

  However, to best integrate with your system, some environment variables
  should be set. If you allow it to, this initialisation step will update
  your bash configuration by adding the following line to ~/.bash_profile:

    test -r /home/alex/.opam/opam-init/init.sh && . /home/alex/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true

  Otherwise, every time you want to access your opam installation, you will
  need to run:

    eval $(opam env)

  You can always re-run this setup with 'opam init' later.

Do you want opam to modify ~/.bash_profile? [N/y/f]
(default is 'no', use 'f' to choose a different file) y                                                           

User configuration:
  Updating ~/.bash_profile.
[NOTE] Make sure that ~/.bash_profile is well sourced in your ~/.bashrc.


<><> Creating initial switch 'default' (invariant ["ocaml" {>= "4.05.0"}] - initially with ocaml-system) 

<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><><><>
Switch invariant: ["ocaml" {>= "4.05.0"}]

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed base-bigarray.base
∗ installed base-threads.base
∗ installed base-unix.base
∗ installed ocaml-system.4.11.1
∗ installed ocaml-config.1
∗ installed ocaml.4.11.1
Done.
# Run eval $(opam env --switch=default) to update the current shell environment
alex@raspberrypi:~$

CAUTION: You will run into problems if you have arm_64=1 in your /boot/config.txt, so before building OPAM, be sure to set arm_64=0 (or remove the line from /boot/config.txt altogether!). (End of caution)

Now we build the infrastructure necessary to play with HOL Light (this will take about an hour in the following state): 

alex@raspberrypi:~$ opam switch create 4.05.0

<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><><><>
Switch invariant: ["ocaml-base-compiler" {= "4.05.0"} | "ocaml-system" {= "4.05.0"}]

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed base-bigarray.base
∗ installed base-threads.base
∗ installed base-unix.base
⬇ retrieved ocaml-base-compiler.4.05.0  (https://opam.ocaml.org/cache)
Processing 13/18: [ocaml-base-compiler: make world]

CAUTION: You will run into problems if you have arm_64=1 in your /boot/config.txt, so before building OPAM, be sure to set arm_64=0 (or remove the line from /boot/config.txt altogether!). (End of caution)

2. HOL Light

Clone HOL Light from github: 

alex@box:~/src/$ git clone https://github.com/jrh13/hol-light
Cloning into 'hol-light'...
remote: Enumerating objects: 8310, done.
remote: Counting objects: 100% (768/768), done.
remote: Compressing objects: 100% (704/704), done.
remote: Total 8310 (delta 137), reused 147 (delta 63), pack-reused 7542
Receiving objects: 100% (8310/8310), 27.50 MiB | 5.38 MiB/s, done.
Resolving deltas: 100% (5585/5585), done.

alex@box:~/src/$ cd hol-light
alex@box:~/src/hol-light/$

We will need OPAM. If you're on a Raspberry pi, see OCaml on Raspberry Pi for help.

The trippy thing is we need to use OPAM to use the "correct" version of OCaml (c.f., Github Issue), the following bash commands should work: 

opam switch create 4.05.0
eval $(opam env)
opam pin add camlp5 7.08
opam install num camlp5

Remark: It seems that the latest version of OCaml to work with Camlp5 7.08 is 4.08.0 — or so OPAM tells me. I couldn't get HOL Light to compile with OCaml 4.08.0 and Camlp5 7.08, your mileage may vary. (End of Remark)

So you will see something like the following (it may appear to "hang" on Processing 7/12: [ocaml-base-compiler ...], but that's because it's building the OCaml compiler from scratch; be patient!): 

alex@box:~/src/hol-light/$ opam switch create 4.05.0

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ocaml-base-compiler.4.05.0] found in cache

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed base-bigarray.base
∗ installed base-threads.base
∗ installed base-unix.base
∗ installed ocaml-base-compiler.4.05.0
∗ installed ocaml-config.1
∗ installed ocaml.4.05.0
Done.
# Run eval $(opam env) to update the current shell environment

alex@box:~/src/hol-light/$ eval $(opam env)
alex@box:~/src/hol-light/$ opam pin add camlp5 7.08
camlp5 is now pinned to version 7.08

The following actions will be performed:
  ∗ install camlp5 7.08*
Do you want to continue? [Y/n] y

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[camlp5.7.08] found in cache

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed camlp5.7.08
Done.

alex@box:~/src/hol-light/$ opam install num camlp5
[NOTE] Package camlp5 is already installed (current version is 7.10).
The following actions will be performed:
  ∗ install base-num base [required by num]
  ∗ install num      0
===== ∗ 2 =====
Do you want to continue? [Y/n] y

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed base-num.base
∗ installed num.0
Done.

alex@box:~/src/hol-light/$

Now, the next step is to run make. It is crucial to run make before loading hol into an OCaml repl. 

alex@box:~/src/hol-light/$ make
...

Now we can do the following: open up ocaml, specifically telling it to include camlp5, and then tell it to #use "hol.ml";; (yes, both semicolons are necessary). 

alex@box:~/src/hol-light/$ ocaml -I `camlp5 -where` camlp5o.cma

        OCaml version 4.05.0

	Camlp5 parsing version 7.08

#

(This is because camlp5 isn't adequately included, for reasons I do not pretend to understand, but I am thankful for the solution from here. Without doing this, we will get Cannot find file camlp5o.cam. error, which is just confusing and cryptic.)

Now we can simply #use "hol.ml";; to get: 

# #use "hol.ml";;
...
...
...
val search : term list -> (string * thm) list = <fun>
- : unit = ()
File "help.ml" already loaded
- : unit = ()
- : unit = ()
- : unit = ()
	Camlp5 parsing version 7.08

#

You can go get a cup of tea or coffee, because it will take a minute or two for everything to load. I suspect there's some way I could combine all this into a small bash script.

Caution: on Raspberry Pi, you can expect to have about 250MB of RAM used just by starting HOL Light in this manner.

Last Updated 2022-01-20 Thu 12:01.