The Coq mailing list

[Makarius <makarius AT sketis.net>]

On Thu, 6 Mar 2008, Lionel Elie Mamane wrote:

> On Thu, Mar 06, 2008 at 04:23:05PM +0100, Freek Wiedijk wrote:
> 
> >> 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...
> 
> > Won't the garbage collector swap it in all the time?
> 
> That's a very good point; you are probably right.

Well, it depends on the kind of garbage collector and memory model of the 
ML system.  For example, as far as I understand SML/NJ's stackless 
stop-and-copy model, the virtual memory space is continously ploughed 
through, yielding swap-ins all time.  Poly/ML is much smarter in not 
touching persistent areas.  Coq uses Ocaml, so the experts on that system 
should know.


        Makarius