The Coq mailing list

["Russell O'Connor" <roconnor AT Math.Berkeley.EDU>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

[To: 
coq-club AT pauillac.inria.fr]

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.

I can see about making my Tactical smarter, and producing smaller proofs.
It would be better if I didn't have too.  After all, a proof is a
proof.

- -- 
Russell O'Connor            <http://www.math.berkeley.edu/~roconnor/>
``[Law enforcement officials] suggested that the activists were stopped
not because their names are on the list, but because their names resemble
those of suspected criminals or terrorists.'' -- SFGate.com

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.2.1 (SunOS)

iQCVAwUBPgJ0vk0+aO5oRkNZAQL3CQP/aep7DkxOR/a8QiGs6JJzECqUfbMnmejQ
g0iHPv+w7qsxFOsU7mZoQfA5DfcUZNzjtIyywh+Bceg3pnvTSL7IzkQuFe0vqwGa
Vs3ivM8sHgCtg21oHxqjvxcwciy3tzqlQNw+A/hgtGr3cN+Lfst9QnFxvUIzLO7f
9q9JUwO10Ts=
=pxDl
-----END PGP SIGNATURE-----