LP, the Larch Prover — The set command


The set command controls various aspects of LP's behavior.

Syntax

<set-command>  ::= set [ <setting-name> [ <setting-value> ] ]
<setting-name> ::= activity | automatic-ordering | automatic-registry 
                      | box-checking | completion-mode | directory 
                      | display-mode | hardwired-usage | immunity 
                      | log-file | lp-path | name-prefix | ordering-method
                      | page-mode | prompt | proof-methods 
                      | reduction-strategy | rewriting-limit | script-file
                      | statistics-level | trace-level | write-mode
<setting-value> ::= <string>
Note: The setting-name can be abbreviated.

Examples

set
set proof-methods
set script session

Usage

The set command with no arguments prints the current values of all settings. The set command with a <setting-name> and no <setting-value> displays the current value of the setting and then requests a new value; responding with a carriage return leaves the value of the setting unchanged. The set command with both a <setting-name> and a <setting-value> sets the value of one of the following settings.

Settings marked with (L) are local to the current proof context. If such a setting is changed, for example, during the proof of one case in a proof by cases it reverts to its previous value upon termination of that case in the proof. Settings marked with G are global and remain in effect until changed by the user. All settings have default values, which can be restored by the unset command.

(L) activity ( on | off )
New assertions are active if on (the default).
(L) automatic-ordering ( on | off )
Formulas are oriented automatically into rewrite rules if on (the default).
(L) automatic-registry ( on | off )
The registry is extended automatically during ordering if on (the default).
(G) box-checking ( on | off )
Markings (<>, []) for proof steps are checked in command files if on (the default).
(L) completion-mode ( big | expert | standard )
Controls the action of the complete command (default standard).
(G) directory <file>
Output files are created in this directory (default ".").
(L) display-mode ( qualified | unqualified | unambiguous )
Controls the qualification of identifiers and terms by the display command (default unambiguous).
(L) hardwired-usage <number>
Turns off some hardwired rules.
(L) immunity ( on | off | ancestor )
Controls the immunity of new assertions (default off).
(G) log-file <file>
Creates file <file>.lplog for log of session (default none).
(G) lp-path <string>
Defines search path for help, .lp, .lpfrz files (default . ~/lp).
(L) name-prefix <simpleId>
Defines prefix for names of assertions, conjectures (default user).
(L) ordering-method <ordering>
Defines method for orienting formulas into rewrite rules (default noeq-dsmpos).
(G) page-mode ( on | off )
Output is paged if on (default off).
(G) prompt <string>
Defines LP's command prompt (default `LP! ').
(L) proof-methods <default-proof-method>+[,]
Defines list of default proof methods for conjectured formulas (default normalization).
(L) reduction-strategy ( inside-out | outside-in )
Controls application of rewrite rules to terms (default outside-in).
(L) rewriting-limit <number>
Bounds number of steps in possibly infinite rewrites (default 1000).
(G) script-file <file>
Creates file <file>.lpscr for record of input (default none).
(G) statistics-level <number>
Controls the kinds of statistics kept by LP (default 2).
(G) trace-level <number>
Controls the amount of detailed output produced by LP (default 1).
(L) write-mode ( qualified | unqualified | unambiguous )
Controls the qualification of identifiers and terms by the write command (default qualified).