HOL Light for Debian
====================


Usage and Documentation
-----------------------

On Debian you can use the command hol-light to run HOL Light, see the
man page hol-light(1).

For information on how to use HOL Light, please visit the HOL Light
website at http://www.cl.cam.ac.uk/~jrh13/hol-light/

HOL Light runs inside an OCaml toplevel. On every session start, the
logical core and all auxilary theorems are loaded as sources into the
OCaml toplevel. On modern hardware this takes about 90 seconds.

HOL Light can use several external tools. Prover9, CSDP, PARI/GP and
Maxima are available in Debian as packages prover9, coinor-csdp,
pari-gp and maxima. The SAT-solver interface of HOL Light requires
MiniSat and zChaff. MiniSat can be installed as package minisat, but
zChaff has a very restrictive license. If you are eligible you can
install it from http://www.princeton.edu/~chaff/zchaff.html . HOL
Light can also make use of cddlib (freely available from
http://www.ifor.math.ethz.ch/~fukuda/cdd_home/) and of squolem2
(available at http://www.cprover.org/qbv/).


Improve startup time with snapshots
-----------------------------------

It is possible to save a snapshot of a running HOL Light instance to
disk by using a user-level checkpointing tool. In Debian, dmtcp is
available. To use it do:

1. install dmtcp: become root and do

   aptitude install dmtcp

2. run hol-light under control of dmtcp

   dmtcp_checkpoint hol-light

3. When you reached a state that you want to save, do

   dmtcp_command --checkpoint

   in a different terminal. This creates several dmtcp* and ckpt*
   files in the directory where you started hol-light. 

4. To restart your snapshop do

   ./dmtcp_restart_script.sh


Keep in mind that the snapshots of dmtcp contain all needed shared
libraries. You should therefore regenerate your snapshots after
installing security updates.


Hol Light test suite
--------------------

The HOL Light test suite is in /usr/share/hol-light/holtest. You
should install the packages prover9, coinor-csdp, pari-gp and
libocamlgraph-ocaml-dev before running it. The test suite will run for
the best part of a day. To check success you have to search for
"Error", "Not_found" and "not found" in the output, for example by
doing

    /usr/share/hol-light/holtest 2>&1 | tee holtest.log | egrep -i '###|error|not.found' 

With this command you can watch all HOL Light messages flying by with
"tail -f holtest.log". 

On Debian the test suite will produce one error 
"Error: skip Minisat/make.ml...", because the Minisat examples cannot
be run without zChaff, which is not available in Debian. Further,
there are a number of false positives, because a number of values and
exceptions contain "error" in their name.

Note that some tests pass successfully even if the functionality is
not available. For instance, "QBF/make.ml" is loaded successfully,
regardless of whether squolem2 is installed or not.


 -- Hendrik Tews <hendrik@askra.de>, Fri, 17 May 2013 13:54:06 +0200