The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT sophia.inria.fr>]

CC to coq-club

"Russell O'Connor" 
<roconnor AT Math.Berkeley.EDU>
 wrote:
> Are all the dependant modules also loaded into memory?  If B
> requires A, C requires B, and D requires C, when I compile D will
> all of C B and A be loaded into memory?

"Pierre Courtieu" 
<Pierre.Courtieu AT sophia.inria.fr>
 wrote:
> I think separate compilation of modules (this is what you are
> talking about after all) is still a research area, the new module
> system may be a step toward that. I think one of the problems is
> that the anti-paradox checking (universe constraints) must be done
> globally.

"Russell O'Connor" 
<roconnor AT Math.Berkeley.EDU>
 wrote:
>  Robert gave me a work around for by problem.  I've created ``stub''
>  files for these theorems with large proofs that take these theorems
>  as axioms. I work from these stub files, knowing the axioms are
>  sound because I have proved them in other files.

That is a work around, but you can't be absolutly sure that no paradox
have been used unless you typecheck everything globally with no axiom
(that said, the probability that you use paradox is low). But of
course you can do global typing (if possible) only from time to time.


Pierre