BUG-SAVE is a top-level command.
Records details of a bug. Saves the current flag settings, the output
of the HISTORY command, all currently loaded library objects, the
current proof, the date and time and any comments (the best idea
is to copy any error messages in to the "comments" prompt).
This setup can then be retrieved with BUG-RESTORE.
The details are saved as a MODE1, under the name that the user provides
(in a file of the same name) with the assertion and library objects in
other-attributes and other-remarks respectively, and the context set
to BUG. The file will be saved in an appropriate directory (see
The command format for BUG-SAVE is:


The arguments have the following meaning:
NAME : Name for bug
COMMENT : Your choice

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage