The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Thu, Mar 06, 2008 at 03:35:28PM +0100, 
marko AT ffri.hr
 wrote:

> In system I develop I have all the time lot of (un)prooved
> subgoals. Proved subgoals are not interesting for me but unproved
> are. I guess the Coq keep all of them in RAM until I proving the
> main goal. Is it correct? I need to optimize the time of processing.
> Is it possible to store unproved subgoals on hard disk and then
> erase them from memory? Later I will take it from disk as needed.

I don't think Coq has an explicit mechanism for that, but if you
refrain from any sort of "Show Proof" and you have a sizeable amount
of swap activated, your OS should do about that automatically... until
Qed time.

-- 
Lionel