Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-07-04 06:13:44 -0700 (Sun, 04 Jul 1999)
Revision: 2775
Log message:
Things seem to be working pretty smoothly now. This is mostly minor
fixes. Still need to fix the problems with the mp toploop.
1. Proofs now use Alexey's ASCII format. By default, proofs
should be saved to CVS in .prla format. You can generate ASCII
files by using "make export", or you can use the "export ()"
instead of the "save ()" command in the editor. For speed,
.prlb files are now saved in a raw, marshaled format. When you
edit a theory, the newest of .cmoz, .prlb, or .prla files is
loaded. There is a new command "convert" to convert between
all the different proof file formats.
convert -I ... [-raw|-term|-lib|-ascii] -impl file.cmoz
raw: save the file in fast, raw format
term: save the file as <magic#>/<marshaled term_io>
lib: send the file to the Nuprl5 library
ascii: create a .prla file
Developers: _please_ mention any changes to the basic data
structures in your CVS logs. The things that matter are:
Refiner.Refiner.TermType.term
Filter_summary.summary_info
Tactic_boot_sig.TacticType.{tactic_arg,extract}
Proof_boot.io_proof
Users: to be safe, save all your proofs using "make export"
before doing a cvs update.
2. "expand ()" and "expand_all ()" now work. I also added
"clean ()" and "clean_all ()" commands to remove those peasky
dangling proof nodes when you are satisfied with a proof. By
default, proofs are saved only down to the innermost rule-box
level, and primitive refinements are omitted. I haven't added
a "deep_save ()" command; it seems unecessary.
3. Sorry, but I had to move theories/boot into the filter. There
are no major changes here, but the directory structure in
filter has changed significantly.
4. I added a THEORIES variable to the mk/config file that
specifies what theories you want to compile. This means that
you don't have to edit all the Makefiles when you add a theory,
and it also means that you can keep your own theories without
having to commit them to cvs.