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

-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.