The Coq mailing list

["M. Scott Doerrie" <mdoerri AT cs.jhu.edu>]

Just so there is some code sitting behind this question, coqtop begins 
to use 3.5+ GB of memory when attempting to instantiate DA.


Require DirectAccess.
Require Semantics.

Module Make (Sem: Semantics.SemanticsType).

  Module DA := (DirectAccess.Make Sem).


I have tested this in 8.2pl2 and am reworking my scripts to compile 
using the standard library in 8.3.  Semantics.SemanticsType is exactly 
the Module Type required by DirectAccess.Make.

Michael Doerrie


On 11/18/2010 12:13 PM, M. Scott Doerrie wrote:
> I am running out of memory instantiating a module from a functor.  My 
> coqtop process grows to 3.5 Gb before I kill it.   I will be upgrading 
> coq again to the latest release in an attempt to fix this, but I'm 
> concerned that my proofs may be to blame.  Are there any known issues 
> that could cause this?
>
> Michael Doerrie