LP, the Larch Prover -- The set command
The set command controls various aspects of LP's behavior.
<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).