LP, the Larch Prover -- The freeze and thaw commands

The freeze and thaw commands enable LP to save and restore its state.

Syntax

<freeze-command> ::= freeze <file>
<thaw-command>   ::= thaw <file>

Examples

freeze case1
thaw case1

Usage

The freeze command saves LP's entire state, excluding the statistics and global settings, but including all proof contexts, in the file named <file>.lpfrz (unless <file> contains a period, in which case LP does not supply the suffix .lpfrz) in LP's current working directory. If a file with that name already exists, its previous contents are erased; if it does not exist, it is created.

The thaw command restores the state of LP from that saved previously using the freeze command in the file named <file>.lpfrz (unless <file> contains a period, in which case LP does not supply the suffix .lpfrz) on the current LP search path. The thaw command will not thaw files that were frozen using an out-of-date version of LP.

These commands are useful for checkpointing attempted proofs. They are also useful for saving and restoring completed or partially-completed systems.

See also