Revised infrastructure for lazy loading of opaque proofs

 Get rid of the LightenLibrary hack : no more last-minute
 collect of opaque terms and Obj.magic tricks. Instead, we
 make coqc accumulate the opaque terms as soon as constant_bodies
 are created outside sections. In these cases, the opaque
 terms are placed in a special table, and some (DirPath.t * int)
 are used as indexes in constant_body. In an interactive session,
 the local opaque terms stay directly stored in the constant_body.

 The structure of .vo file stays similar : magic number, regular
 library structure, digest of the first part, array of opaque terms.
 In addition, we now have a final checksum for checking the
 integrity of the whole .vo file. The other difference is that
 lazy_constr aren't changed into int indexes in .vo files, but are
 now coded as (substitution list * DirPath.t * int). In particular
 this approach allows to refer to opaque terms from another
 library. This (and accumulating substitutions in lazy_constr)
 seems to greatly help decreasing the size of opaque tables :
 -20% of vo size on the standard library :-). The compilation times
 are slightly better, but that can be statistic noise.

 The -force-load-proofs isn't active anymore : it behaves now
 just like -lazy-load-proofs. The -dont-load-proofs mode has
 slightly changed : opaque terms aren't seen as axioms anymore,
 but accessing their bodies will raise an error.

 Btw, API change : Declareops.body_of_constant now produces directly
 a constr option instead of a constr_substituted option

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16382 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 10 deletions

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 3bf9e7cb5..543dce18f 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -219,25 +219,19 @@ Section~\ref{LongNames}).
 
 \item[{\tt -dont-load-proofs}]\ 
 
-  Warning: this is an unsafe mode.
-  Instead of loading in memory the proofs of opaque theorems, they are
-  treated as axioms. This results in smaller memory requirement and
-  faster compilation, but the behavior of the system might slightly change
-  (for instance during module subtyping), and some features won't be
-  available (for example {\tt Print Assumptions}).
+  In this mode, it is an error to access the body of opaque theorems
+  (for example via {\tt Print} or {\tt Print Assumptions}).
 
 \item[{\tt -lazy-load-proofs}]\
 
   This is the default behavior. Proofs of opaque theorems aren't
   loaded immediately in memory, but only when necessary, for instance
   during some module subtyping or {\tt Print Assumptions}. This should be
-  almost as fast and efficient as {\tt -dont-load-proofs}, with none
-  of its drawbacks.
+  almost as fast and efficient as {\tt -dont-load-proofs}.
 
 \item[{\tt -force-load-proofs}]\
 
-  Proofs of opaque theorems are loaded in memory as soon as the
-  corresponding {\tt Require} is done. This used to be Coq's default behavior.
+  Deprecated, now the same as {\tt -lazy-load-proofs}.
 
 \item[{\tt -no-hash-consing}] \mbox{}