LP, the Larch Prover -- The script-file setting

The script-file setting provides a means of recording user input in a file.

Syntax

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

Examples

set script session

Usage

The set script command causes LP to start recording user input in a file named <file>.lpscr (unless <file> contains a period, in which case LP does not supply the suffix .lpscr) in LP's current working directory. Any previous contents of this log file are lost. If LP was already scripting to a file, that file is closed before opening the new one is opened. Scripting is ended by the quit or unset script command, which is not recorded in the script file.

LP annotates the script file by commenting out erroneous commands, by substituting the text of the executed file for an execute command, by marking the creation of subgoals and the completion of proofs, and by indenting the script to reveal its proof structure.

Script files can be replayed using the execute command, and they can be edited before being replayed. Although a script file can be replayed directly using the command execute fileName.lpscr, it is generally advisable to rename the script file to fileName.lp and then replay it using the command execute fileName (lest a set script command cause LP to overwrite the command file being executed).

See also