checkpoint : string -> unit
- SYNOPSIS
-
Exits HOL Light but saves current state ready to restart.
- DESCRIPTION
-
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
disc space.
- USES
-
To quickly save the state of HOL Light when it would take a long time to
regenerate.
- COMMENTS
-
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
-
self_destruct, startup_banner.