LP, the Larch Prover -- The execute command

The execute command causes LP to execute commands from a specified file.

Syntax

<execute-command> ::= ( execute | execute-silently ) <file>
<file>            ::= <blank-free-string>

Examples

execute myProof

Usage

The execute command causes LP to execute the commands in the file named <file>.lp (unless <file> contains a period, in which case LP does not supply the suffix .lp) on the current LP search path. The execute command is ordinarily used to execute commands from a file that was created by the set script or write commands, but any text file may be specified.

Further execute commands may occur in .lp files, but recursive .lp files are not allowed. Once a .lp file has been exhausted, LP resumes accepting input from the previous .lp file or from the user if no other file is being executed. If LP encounters an error while executing a file, or if the user interrupts LP, LP takes subsequent input from the terminal.

The execute-silently command is just like execute, except that it produces no output.