LP, the Larch Prover — The log-file setting

The log-file setting provides a means of recording the current LP session in a file.

Syntax

<set-log-file-command> ::= set log-file <file>

Examples

set log session

Usage

The set log command causes LP to start recording the terminal session in a file named <file>.lplog (unless <file> contains a period, in which case LP does not supply the suffix .lplog) in LP's current working directory. Any previous contents of this log file are lost. If LP was already logging to a file, that file is closed before opening the new log file. Logging is ended by the quit or unset log commands.