TPS-TEST : MEXPRTPS-TEST is a top-level command.
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?
TPS documentation homepage