Skip to content
Browse files

Update documentation concerning proofs loading (cf last commit)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13954 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent a9bf7d8 commit f8e8ffa4b7c42f6c53126d284c0bfbf8a992bc89 letouzey committed Apr 3, 2011
Showing with 22 additions and 3 deletions.
  1. +3 −0 CHANGES
  2. +19 −3 doc/refman/RefMan-com.tex
View
3 CHANGES
@@ -75,6 +75,9 @@ Libraries
Internal infrastructure
+- Opaque proofs are now loaded lazily by default. This allows to be almost as
+ fast as -dont-load-proofs, while being safer (no creation of axioms) and
+ avoiding feature restrictions (Print and Print Assumptions work ok).
- Experimental support added for camlp4 (the one provided alongside ocaml),
simply pass option -usecamlp4 to ./configure. By default camlp5 is used.
- Revised build system: no more stages in Makefile thanks to some recursive
View
22 doc/refman/RefMan-com.tex
@@ -265,9 +265,25 @@ \section{Batch compilation ({\tt coqc})}
\item[{\tt -dont-load-proofs}]\
- This avoids loading in memory the proofs of opaque theorems
- resulting in a smaller memory requirement and faster compilation;
- warning: this invalidates some features such as the extraction tool.
+ 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}).
+
+\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.
+
+\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.
\item[{\tt -vm}]\

0 comments on commit f8e8ffa

Please sign in to comment.
Something went wrong with that request. Please try again.