Hello both, This may be anecdotal, but I am checkpointing HOL Light with dmtcp 1.2.8 on Ubuntu 16.04.1 and Scientific Linux 6 with no visible problems. (Haven't managed to make later versions of dmtcp work though.)
Having said that, I would agree a virtual machine is in principle the better, more widely applicable/portable way to go. Regards, Petros On 23/10/2016 04:24, john.harri...@cl.cam.ac.uk wrote: > 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 > -- Petros Papapanagiotou, Ph.D. CISA, School of Informatics The University of Edinburgh Email: p...@ed.ac.uk --- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ 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
