Hi Cris,
| Correct me if I'm wrong, but the last I looked, the checkpointing could
| only work in versions of Linux that are now several years old.
Possibly, but I have not kept up-to-date on the status of various
checkpointing options in Linux. Does DMTCP no longer help? It was OK
not *that* long ago (or so it seems to me). I also remember someone
reporting successful use of BLCR. Well it's certainly less convenient
than in the days when "ckpt" could be relied on. Then the very simple
"make install" option in the Makefile gave you nice self-contained
binaries.
| Another option that does work is to use machine virtualization
| software such as VirtualBox to create a Linux environment you can
| start under Windows, Mac, or even Linux, load your preferred
| theories into HOL Light within that VirtualBox environment, and
| then save the state of the virtual machine into a snapshot on
| disk. You can restart the snapshot at any time, which for me is a
| lot quicker than reloading theories.
That is certainly a possibility. Actually I have one really ancient
debian machine under Virtualbox where no snapshotting is necessary
because the old "ckpt" works and one can immediately call up an
image with all the Multivariate theories preloaded. For example:
$ hol.complex
HOL Light 2.20++, built 22 October 2016 on OCaml 3.09.2 with ckpt
Preloaded with multivariate-based complex analysis
val it : unit = ()
#
That is hardly something I can recommend for general use though :-)
John.
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
