[Hol-info] A new checkpointing program for HOL Light

[John H. <Joh...@cl...>]

Since OCaml doesn't have the ability to save and restore the state of
the toplevel, many people, including myself, use OS-level
checkpointing as a way of saving the state of the HOL Light process.

The two currently supported checkpointers, "ckpt" and "CryoPID", both
seem to have issues on many recent Linux versions. However, there is
another alternative that seems to work well (e.g. it works fine for
me under Ubuntu Karmic). This is "dmtcp", the successor to Condor's
ckpt program. You can get it 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. I don't yet have
the usage conveniently scripted but the basic method is this:

 1. dmtcp_checkpoint -n ocaml

 2. <use ocaml to load HOL Light as usual>

 3. (from another terminal) dmtcp_command --checkpoint 

 4. (don't forget this!) kill the original ocaml process

 5. Step 3 created a shell script in the current directory. Running
    that will restore the OCaml process with all your state and
    bindings.

John.