HOL LIGHT

HOL Light is an interactive theorem prover / proof checker. It is
written in Objective CAML (OCaml) and uses the toplevel from OCaml as
its front end. This is the HOL Light homepage:

        http://www.cl.cam.ac.uk/~jrh13/hol-light/index.html

Basic installation instructions are below. For more detailed information
on usage, see the Tutorial:

        http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf

Refer to the reference manual for more details of individual functions:

        http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.html (HTML files)
        http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.pdf (one PDF file)

        *       *       *       *       *       *       *       *

                             INSTALLATION

The Objective CAML (OCaml) implementation is a prerequisite for
running HOL Light. HOL Light should work with any recent version of
OCaml; I've tried it on at least 3.04, 3.06, 3.07+2, 3.08.1, 3.09.3,
3.10.0 and 3.11.2. However, for versions >= 3.10 (in 3.10 there was an
incompatible change in the camlp4 preprocessor) you will also need to
get camlp5 (version >= 4.07). Installing both items of software should
not be too difficult, depending on the platform. For example, in
Ubuntu Linux, the following line is all you need (followed by your
password if prompted):

        sudo apt-get install ocaml camlp5

However, if your platform has no convenient package manager or you
prefer to build from sources, you can download OCaml and camlp5
directly from their respective Web pages:

        http://caml.inria.fr/ocaml/index.en.html

        http://pauillac.inria.fr/~ddr/camlp5/

If you do build camlp5 from source, it is recommended that you build
it in "strict" mode, i.e. begin with "./configure --strict" before
doing "make".

The instructions below assume a Unix-like environment such as Linux
[or Cygwin (see www.cygwin.com) under Windows], but the steps
automated by the Makefile are easy enough to invoke manually. There's
more detail on doing that in the Tutorial.

(0) You can download the HOL Light sources from the Google Code site.
    For example, the following will copy the code from the trunk of the
    Google Code repository into a new directory 'hol_light':

        svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light

    Alternatively, if you download one of the gzipped tar files
    directly from the HOL Light Web page, you can unpack it as usual:

        tar xvfz hol_light.tar.gz

    In either case, you should next enter the 'hol_light' directory
    that has been created:

        cd ./hol_light

There are now two alternatives: launch the OCaml toplevel and directly
load the HOL Light source files into it, or create a standalone image
with all the HOL Light sources pre-loaded. The latter is more
convenient, but requires a separate checkpointing program, which may not
be available for some platforms. First the basic approach:

(1) Do 'make'. This ought to build the appropriate syntax extension
    file ('pa_j.cmo') for the version of OCaml that you're using. If you
    have the camlp4 or camlp5 libraries in a non-standard place rather
    than /usr/local/lib/ocaml/camlp4 or /usr/local/lib/ocaml/camlp5
    then you may get an error like this

      Error while loading "pa_extend.cmo": file not found in path.

    in which case you should add the right directory to CAMLP4LIB or
    CAMLP5LIB, e.g.

      export CAMLP5LIB=$HOME/mylib/ocaml/camlp5

(2) Do 'ocaml' (possibly 'ocamlnum' on some platforms --- see [*] below).
    You should see a prompt, something like:

                Objective Caml version 3.08.2

        #

(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 define : term -> thm = <fun>
        - : unit = ()
        val help : string -> unit = <fun>
        - : unit = ()
                Camlp5 Parsing version 3.10

        #

    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 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

        let hol_dir = ref (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());;

    to, for example

        let hol_dir = "/home/johnh/hol_light";;

    or

        let hol_dir = "/usr/share/hol";;

Now for the alternative approach of building a standalone image.
The level of convenience depends on the checkpointing program you
have installed. The earlier checkpointing programs in this list
are more convenient to use but seem less easy to get going on
recent Linux kernel/libc combinations.

(1) If you have the 'ckpt' program installed, then the Makefile will
    conveniently create a HOL Light binary. You can get 'ckpt' here:

        http://www.cs.wisc.edu/~zandy/ckpt/

    Once 'ckpt' is installed, simply type

        make hol

    in the 'hol_light' directory, and a standalone HOL Light image
    called 'hol' should be created. If desired you can move or copy
    this to some other place such as '~/bin' or '/usr/local/bin'. You
    then simply type 'hol' (or './hol') to start the system up and
    start proving theorems.

    Note that although the HOL binary will work on its own, it
    does not pre-load all the source files. You will probably want
    to keep the sources available to be loaded later as needed (if
    you need additional mathematical theories or tools), so it's
    better to unpack the HOL distribution somewhere permanent
    before doing 'make hol'.

    If you later develop a large body of proofs or tools, you can
    save the augmented system using the command "self_destruct"
    (this is the same approach as in the Makefile) rather than
    re-load each time. For example, the following will create a
    HOL Light binary (always called 'hol.snapshot'):

        self_destruct "My version of HOL Light";;

(2) Another checkpointing option is CryoPID, which you can get
    here:

        http://cryopid.berlios.de/

    In this case, the Makefile doesn't have a convenient way of
    making HOL binaries, but you can make one yourself once HOL
    Light is loaded and you are sitting in its toplevel loop.
    (This also works if you have your own extensions loaded, and
    indeed this is when it's most useful.) Instead of the
    'self_destruct' command, use 'checkpoint', which is similar
    except that the current process is not terminated once the
    binary (again called hol.snapshot) is created:

        checkpoint "My version of HOL Light";;

(3) A third option which seems to work with recent Linuxes is
    DMTCP, which you can download from here:

      http://dmtcp.sourceforge.net/

    You may try installing from the packages (e.g.
    'sudo dpkg -i dmtcp.deb'), but I found it was better to
    compile from source. HOL Light does not have convenient
    commands or scripts to exploit DMTCP, but you can proceed
    as follows:

        1. Start ocaml running under the DMTCP coordinator:

              dmtcp_checkpoint -n ocaml

        2. Use ocaml to load HOL Light as usual, for example:

              #use "hol.ml";;

        3. From another terminal, issue the checkpoint command:

             dmtcp_command --checkpoint

        4. (Don't forget this!) Kill the original ocaml process,
           e.g. by just typing control-d to the Ocaml prompt.

        5. Step 3 created a checkpoint of the OCaml process and
           a shell script to invoke it, both in the directory in
           which ocaml was started. Running that should restore
           the OCaml process with all your state and bindings:

             ./dmtcp_restart_script.sh

(4) If none of these options work, you may find some others on the
    following Web page. Unfortunately I don't know of any such
    checkpointing program for either Windows or Mac OS X; I would
    be glad to hear of one.

        http://checkpointing.org

The directories "Library" and "Examples" may give an idea of the
kind of thing that might be done, or may be useful in further work.

Thanks to Carl Witty for help with Camlp4 porting and advice on
checkpointing programs.

        *       *       *       *       *       *       *       *

[*] HOL Light uses the OCaml 'num' library for multiple-precision
rationals. On many platforms, including Linux and native Windows, this
will be loaded automatically by the HOL root file 'hol.ml'. However,
OCaml on some platforms (notably Cygwin) does not support dynamic
loading, hence the need to use 'ocamlnum', a toplevel with the 'num'
library already installed. This is normally created as part of the
OCaml build, but if not, you can make your own with:

    ocamlmktop -o ocamlnum nums.cma