HOL Light on ocamlnat

Warning

Note that ocamlnat is undocumented experimental software that comes with OCaml 3.11. This how-to guide is also experimental. Use this guide at your own risk.

Introduction

Ocaml 3.11 comes with a native toplevel ocamlnat. It compiles to native code instead of bytecode. Using HOL Light on ocamlnat is not as simple as typing #use "hol.ml" in ocamlnat because ocamlnat requires native-compiled libraries. To use HOL Light on ocamlnat, one needs a native version of the camlp5_top. At the moment, neither ocamlnat nor a native version of camlp5_top is built by default; they must be generated from source. The instructions below are the result of my crude (but successful) attempt to make HOL Light work on ocamlnat. I hope to update this guide in the future to make things a bit more elegant. Until then, they should get you rolling.

Instructions

These instructions have been tested on Linux (Ubuntu 9.04 and Sidux) and Mac OS X 10.5.7 (with Xcode 3.1.3).

It is a good idea to install everything locally. Here is what I did (using bash shell):

export HOLNATDIR=$HOME/holnat
mkdir $HOLNATDIR

You can of course choose some other directory for $HOLNATDIR.

Next, download the following source files and save them to $HOLNATDIR.

http://caml.inria.fr/pub/distrib/ocaml-3.11/ocaml-3.11.1.tar.gz
http://pauillac.inria.fr/~ddr/camlp5/distrib/src/camlp5-5.12.tgz
http://www.cl.cam.ac.uk/~jrh13/hol-light/hol_light_090717.tgz

Then issue the following commands in sequence:

cd $HOLNATDIR

tar zxvf ocaml-3.11.1.tar.gz
tar zxvf camlp5-5.12.tgz
tar zxvf hol_light_090717.tgz

cd ocaml-3.11.1
./configure -prefix $HOLNATDIR
make world.opt
make install
make ocamlnat
cp ocamlnat $HOLNATDIR/bin

export PATH="$HOLNATDIR/bin:$PATH"

cd ../camlp5-5.12
./configure -prefix $HOLNATDIR
make world
make opt
make install

cd top

sed -e 's/Toploop/Opttoploop/g' camlp5_top.ml \
| sed -e 's/Topdirs/Opttopdirs/g' > camlp5_opttop.ml

ocamlrun ../boot/camlp5r -nolib -I ../boot pa_macro.cmo q_MLast.cmo \
-mode T -o camlp5_opttop.ppo camlp5_opttop.ml

ocamlopt -warn-error A -I ../main -I ../boot -I ../ocaml_stuff/3.11.1/utils \
-I ../ocaml_stuff/3.11.1/parsing -I ../ocaml_stuff/3.11.1/typing -I \
../ocaml_stuff/3.11.1/toplevel -I $HOLNATDIR/ocaml-3.11.1/toplevel \
-c -impl camlp5_opttop.ppo

rm -f camlp5_opttop.ppo

cp camlp5_opttop.cmx camlp5_opttop.cmi camlp5_opttop.o \
$HOLNATDIR/lib/ocaml/camlp5

cd ..
cp main/*.cmx main/*.cmi main/*.o $HOLNATDIR/lib/ocaml/camlp5
cp lib/*.cmx lib/*.cmi lib/*.o $HOLNATDIR/lib/ocaml/camlp5

cd ocaml_stuff/3.11.1/utils
cp pconfig.cmx pconfig.cmi pconfig.o $HOLNATDIR/lib/ocaml/camlp5

cd $HOLNATDIR/hol_light

make
ocamlopt -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" \
-I +camlp5  pa_j.ml

sed -e 's/nums\.cma/nums.cmxa/g' sys.ml > sysnat.ml

The moment of truth

If everything above goes through successfully, you should be able to use HOL Light on ocamlnat (provided you have enough RAM on your computer). Download this file to $HOLNATDIR/hol_light. Then start ocamlnat by doing the following:

cd $HOLNATDIR/hol_light
$HOLNATDIR/bin/ocamlnat -I $HOLNATDIR/lib/ocaml/camlp5

Once you get the toplevel prompt, type:

#use "holnat.ml";;

Now, take a cup of coffee and you are on your way!

P.S.

Loading HOL Light on ocamlnat as above is much slower than on ocaml because there is a big latency in compiling to native code. I am still figuring out what is the best way to compile all of HOL Light core into native binary. Doing so should dramatically reduce the initial loading time.

Update: I have figured out a way to compile all of HOL Light into native binary. Initial load time on my Mac Pro is now down to 21 seconds. The instructions are found below.

All of HOL Light in native binary

Download all the files located here to $HOLNATDIR/hol_light. Then issue the following commands:

cd $HOLNATDIR/hol_light

export PATH="$HOLNATDIR/bin:$PATH"

ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" \
-I +camlp5  pa_j.ml

ocamlopt -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" \
-I +camlp5  pa_j.ml

ocamlopt -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo \
-I . pa_j.cmo" -I +camlp5 -I $HOLNATDIR/lib -I $HOLNATDIR/lib/camlp5 \
holcore.ml

ocamlopt -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo \
-I . pa_j.cmo" -I +camlp5 -I $HOLNATDIR/lib -I $HOLNATDIR/lib/camlp5 \
proved1.ml

ocamlopt -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo \
-I . pa_j.cmo" -I +camlp5 -I $HOLNATDIR/lib -I $HOLNATDIR/lib/camlp5 \
proved2.ml

ocamlopt -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo \
-I . pa_j.cmo" -I +camlp5 -I $HOLNATDIR/lib -I $HOLNATDIR/lib/camlp5 \
proved3.ml

Then start ocamlnat by doing the following:

$HOLNATDIR/bin/ocamlnat -I $HOLNATDIR/lib/ocaml/camlp5

Once you get the toplevel prompt, type:

#use "holx.ml";;

Last update: July 29, 2009.