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.