LP, the Larch Prover -- Unix command-line options


The following options can be specified on the Unix command line when invoking LP:
-c
Enables experimental features for conditional rewriting.

-d fileName
Specifies the location of LP's run-time library, to which ~lp in the lp-path setting refers. The default is /usr/local/lib/LP.

-e
Enables undocumented experimental features in LP.

-max_heap <number>
Sets an upper bound, in megabytes, on the size of LP's heap. This bound should be large enough for LP top handle a proof without running its collector too often (for example, 10 meg on a 32-bit machine and 20-meg on a 64-bit machine). It should be small enough for LP to run without paging (for example, half of the total amount of memory on a single-user machine).

-min_gc <number>
Sets the minimum threshhold, in megabytes, beneath which LP's collector will not run automatically.

-t
Prevents LP from aborting execution of .lp files when an error occurs; useful for testing LP.