checkpoint : string -> unit
Exits HOL Light but saves current state ready to restart.
This is only available in Linux. A call checkpoint s calls the freeze
function from CryoPID to create a checkpoint of the current state of HOL Light,
named hol.snapshot. When this image is restarted, the string s is printed
as well as the usual startup banner.
- FAILURE CONDITIONS
Never fails, except in the face of OS-level problems such as running out of
To quickly save the state of HOL Light when it would take a long time to
Unfortunately I do not know of any checkpointing tool that can give this
behaviour under Windows or Mac OS X. See the README file and tutorial for
additional information on Linux checkpointing options.
- SEE ALSO