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 | freeze-current) <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 freeze-current command does the same, except that it only saves the state of the current proof context. This command is faster and uses less disk space than the freeze command. It is useful primarily for trying different strategies for proving the current conjecture.

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