Like TPS-TEST (see the help message for that command), but calls

the TEST top level and attempts to prove one theorem repeatedly with several

different values of some crucial flags, to see how the time taken will vary.

TEST-THEOREMS should contain a list of dotted pairs of theorems and modes

in which they can be proven; the searchlist which is used should have at

least one setting in which the theorem can be proven (otherwise tps-test2

will never finish that theorem).

The output file (by default, tps-test2-output.doc) will contain a summary of

the results. If this file already exists, it will be renamed by adding .bak

to its name.

The command format for TPS-TEST2 is:

<n>TPS-TEST2 SEARCHLIST QUIET-RUN EXPU OUTPUT TESTWIN

"SYMBOL" "YESNO" "YESNO" "FILESPEC" "YESNO"

The arguments have the following meaning:

SEARCHLIST : Searchlist to use?

QUIET-RUN : Run quietly?

EXPU : EXPUNGE and assert defaults between each theorem?

OUTPUT : Short output file

TESTWIN : Send output to the TEST window?

© 1988-99, Carnegie Mellon University.