Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-02 16:35:41 -0800 (Wed, 02 Nov 2005)
Revision: 8080
Log message:
I am working on rewriting and simplifying MetaPRL core IO - I want to change
it so that the "role" of .cmoz/.prlb/.prla files is better established.
In particular. my goals are
- In the editor, the module is always taken from the .cmoz. (Optionally: if
.prlb or .prla is newer, then the proofs are read and _merged_)
- The .prlb is a "cache" for the .prla. If the .prla have changed since the
.prlb was generated, the old .prlb is discarded (even if it happens to be
newer).
- Optionally: refuse to load .cmoz into toploop, if it was compiled against a
version of MetaPRL that is different from the one currently running.
- Longer term: only store proofs (and other items created or modified from
the toploop) in .prlb/.prla. This way the .prla are much smaller, the
locations are not stored in .prlb, the items created from the toploop are
not discarded at repompile.
Changes | Path |
Copied | metaprl-branches/new_binary_io |