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 auxiliary 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 and in /usr/share/hol-light/holtest_parallel. Both scripts run the same tests, the latter one uses ``make -j $(getconf _NPROCESSORS_ONLN)'' to run the tests in parallel on all available cores. When I last tried, the tests run for about 70 CPU hours (10 hours on 8 cores for the parallel version). You should install the packages prover9, coinor-csdp, pari-gp and libocamlgraph-ocaml-dev before running the tests. The sequential version produces the output on standard output, which you should capture with something like /usr/share/hol-light/holtest 2>&1 | tee holtest.log The parallel version eventually produces the file /tmp/hollog_/holtest.log containing all the output. To check success you have to search for "Error", "Not_found" and "not found" in the output, for example by using egrep -i 'error|not.found' On Debian, the test suite will produce the error "Error: skip Minisat/make.ml...", because the Minisat examples cannot be run without zChaff, which is not available in Debian. Additionally, the tests Mizarlight/make.ml, miz3/make.ml and QBF/make.ml will fail as they do for the upstream version. On architecture i386 (and probably other 32 bit architectures as well), the test 100/pnt.ml fails because it runs out of memory. Note that the above grep command produces quite a few false positives, because a number of values and exceptions contain "error" in their name. Note also, that some tests pass successfully even if the functionality is not available. -- Hendrik Tews , Mon, 9 Jan 2017 23:30:42 +0100