Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Reducing memory usage

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Reducing memory usage


chronological Thread 
  • 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




Archive powered by MhonArc 2.6.16.

Top of Page