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). Improvements in garbage collection, as well as increases in memory sizes, that have occurred since LP's initial development make this and the -min_gc command-line option less useful than before. Hence they are being deprecated and may not be available in recent distributions of LP.

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