The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi Russell,

> Using my own Tacticals, I have create some proofs that have large proof
> objects.  The .vo files are 10 to 20 megabytes.
> 
> The problem is that when I import several these files (using Require) the
> memory consumption of the coqtop application gets enormous (300-400
> megs).  Is anyway I can reduce the memory usage of the application.  It
> seems unnecessary to load a gigantic opaque proof into memory.

  Nothing is currently done not to load the opaque proofs into
memory. However a memory sharing strategy has been introduced in the
cvs version which provides gains of a magnitude of 3 in the average. I
integrated this memory sharing strategy to the bugs-fixes version of
V7.3.1 too. It will be available tomorrow on the anonymous cvs server
coqcvs.inria.fr (tag V7-3bugfix).

  Hugo Herbelin