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.