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. ------------------------------------------------------------------------------ Download Intel® Parallel Studio Eval Try the new software tools for yourself. Speed compiling, find bugs proactively, and fine-tune applications for parallel performance. See why Intel Parallel Studio got high marks during beta. http://p.sf.net/sfu/intel-sw-dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
