self_destruct : string -> unit
Exits HOL Light but saves current state ready to restart.
This operation is only available in HOL images created using checkpointing (as
in the default Linux build arising from make all), not when the HOL Light
sources have simply been loaded into the OCaml toplevel without checkpointing.
A call self_destruct s will exit the current OCaml / HOL Light session, but
save the current state to an image hol.snapshot. Users can then start this
image; it will display the usual banner and also the string s, and the user
will then be in the same state as before self_destruct.
- FAILURE CONDITIONS
Never fails, except in the face of OS-level problems such as running out of
Very useful to start HOL Light quickly with many background theories or tools
loaded, rather than needing to rebuild them from sources.
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.
Suppose that all the proofs you are doing at the moment need more theorems
about prime numbers, and also a list of all prime numbers up to 1000. We reach
a suitable state:
and now issue the checkpointing command:
# needs "Library/prime.ml";;
# let primes_1000 = rev(rev_itlist
(fun q ps -> if exists (fun p -> q mod p = 0) ps then ps else q::ps)
HOL Light will exit and a new file hol.snapshot will be created. You might
want to rename it as hol.prime in the OS so it has a more intuitive name and
doesn't get overwritten by later checkpoints
self_destruct "Preloaded with prime number material";;
You can then start the new image just by hol.prime:
$ mv hol.snapshot hol.prime
and continue where you left off, with all the prime-number material
HOL Light 2.10, built 16 March 2006 on OCaml 3.08.3
Preloaded with prime number material
val it : unit = ()
val it : thm =
|- !p a b. prime p /\ p divides a * b ==> p divides a \/ p divides b
# el 100 primes_1000;;
val it : int = 547
- SEE ALSO