Attempt to prove a list of theorems; used for testing new versions of TPS.

The list of theorems, with the modes to be used, is stored as (theorem . mode)

pairs in the flag TEST-THEOREMS. These theorems and modes will be fetched from

the library, if they cannot be found in TPS and if you have a library. You

should set DEFAULT-LIB-DIR and BACKUP-LIB-DIR appropriately. You can only do

DATEREC after each theorem if you have a library you can write to. Quiet

running uses the mode QUIET to switch off as much screen output as possible.

You can EXPUNGE between proofs (this will reduce the amount of memory required,

but will mean that other expansion proofs in the memory may be lost; it will

also re-assert your default flag values between each proof).

The output file is kept independently of DATEREC records, and consists of single

lines, one per theorem, either stating that the theorem was proved at a certain

time using a certain mode, or that the proof terminated with proof lines still

remaining (i.e. you've got a bug somewhere) or that tps-test ended abnormally

(i.e. either a serious bug or you pressed Ctrl-C). Timing information can also

be sent to the short file if necessary.

If the short file already exists, the old copy will be renamed by adding

.bak to its name.

See the help messages for TEST-THEOREMS and TEST-INIT for more information.

The command format for TPS-TEST is:

<n>TPS-TEST MATE-ONLY RECORD MODEREC QUIET-RUN EXPU MODIFY OUTPUT TIMING TESTWIN

"YESNO" "YESNO" "YESNO" "YESNO" "YESNO" "YESNO" "FILESPEC" "YESNO" "YESNO"

The arguments have the following meaning:

MATE-ONLY : Only do mating search?

RECORD : Do a DATEREC after each theorem is proven?

MODEREC : Do a MODEREC after each theorem is proven?

QUIET-RUN : Run quietly?

EXPU : EXPUNGE and assert defaults between each proof?

MODIFY : Modify modes?

OUTPUT : Short output file

TIMING : Send timing info to the short file?

TESTWIN : Send output to the TEST window?

© 1988-99, Carnegie Mellon University.