COMMAND-LINE-SWITCHES : INFOCOMMAND-LINE-SWITCHES is a flag setting or other piece of information.
Several switches can be given on the command line when
TPS is started up. They are as follows:
-grader starts TPS in the GRADER top level.
-batch <file1> will execute the work file <filename>.work and
then quit TPS.
-omega will prevent -batch from quitting TPS
-outfile <file2.prf>, in the presence of -omega and -batch, runs the
work file <filename1>.work and then remains in
TPS. When the user exits, <file2.prf> will be
written, containing the current version of the
dproof created by the work file. A file <file2.prt>
will also be written. Note that the given filename
filename MUST end with .prf
-outfile <file2>, in the presence of -batch alone, sends a script
of the entire session to <file2>.
-problem -mode -slist belong together; they will execute the given problem
using the given mode and searchlist.
tps3 -- -batch thm266
runs thm266.work through tps3, showing the output on the terminal.
tps3 -- -batch thm266 -outfile thm266.script
does the same but directs the output to thm266.script.
tps3 -- -omega -batch thm266 -outfile thm266.prf
starts TPS, runs thm266.work and then enters the TPS command-line
interface. When the user exits, it writes the current proof into
the file thm266.prf
tps3 -- -batch thm266 -outfile /dev/null
does the same but discards the output.
Notice that the "--" is required for allegro lisp, but not for cmucl,
where the equivalent commands are of the form: tps3cmu -batch thm266
Each of these also writes entries to tps-batch-jobs as follows:
Attempting to run work file thm266.work
on Monday, August 25, 1997 at 17:01:00.
Ending run of work file thm266.work
on Monday, August 25, 1997 at 17:12:00.
TPS documentation homepage