HOL Light on ocamlnat

Warning

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

Introduction

Objective Caml 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 camlp5_top of Camlp5. 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 the process a bit more polished. Until then, they should get you rolling.

Instructions (Updated)

These instructions have been tested on Linux (Ubuntu 9.04 and sidux 2009-02) and Mac OS X 10.5.7 (with Xcode 3.1.3). (The original set of instructions, which are deprecated, can be found here.)

Unless you know what you are doing, it maybe 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_090731.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_090731.tgz

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

cd toplevel

cp opttopdirs.cmx opttopdirs.cmi opttopdirs.o \
   opttoploop.cmx opttoploop.cmi opttoploop.o \
   $HOLNATDIR/lib/ocaml

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

cd ..

ocamlopt -linkall -a \
ocaml_stuff/3.11.1/utils/pconfig.cmx lib/ploc.cmx lib/plexing.cmx \
lib/plexer.cmx lib/fstream.cmx lib/gramext.cmx lib/grammar.cmx lib/diff.cmx \
lib/extfold.cmx lib/extfun.cmx lib/pretty.cmx lib/pprintf.cmx \
lib/eprinter.cmx main/quotation.cmx main/ast2pt.cmx main/reloc.cmx \
main/exparser.cmx main/pcaml.cmx main/prtools.cmx lib/stdpp.cmx \
lib/token.cmx etc/pa_o.cmx etc/pa_op.cmx top/camlp5_opttop.cmx -o camlp5o.cmxa
      
cp camlp5o.cmxa camlp5o.a $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!

Loading HOL Light on ocamlnat as above is slower than on ocaml because there is a big latency in compiling to native code. (It is much slower in Linux.) To pre-compile all of HOL Light into native binary, continue with the instructions below.

Pre-compiling HOL Light core into 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_jnat.ml

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

ocamlopt -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo \
-I . pa_jnat.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_jnat.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_jnat.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_jnat.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: August 5, 2009.