coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <Pierre.Courtieu AT sophia.inria.fr>
- To: "Russell O'Connor" <roconnor AT Math.Berkeley.EDU>, "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Reducing memory usage
- Date: Mon, 6 Jan 2003 10:32:45 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- Re: [Coq-Club] Reducing memory usage, Pierre Courtieu
- Re: [Coq-Club] Reducing memory usage,
Russell O'Connor
- Re: [Coq-Club] Reducing memory usage,
Judicael Courant
- Re: [Coq-Club] Reducing memory usage, Russell O'Connor
- Re: [Coq-Club] Reducing memory usage,
Judicael Courant
- Re: [Coq-Club] Reducing memory usage,
Russell O'Connor
Archive powered by MhonArc 2.6.16.