coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Managing memory from Coq - Correction

From: Lionel Elie Mamane <lionel AT mamane.lu>
To: Freek Wiedijk <freek AT cs.ru.nl>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Managing memory from Coq - Correction
Date: Thu, 6 Mar 2008 16:38:57 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.

--
Lionel

[Coq-Club] Managing memory from Coq - Correction, marko
- Re: [Coq-Club] Managing memory from Coq - Correction, Lionel Elie Mamane
  - Message not available
    - Re: [Coq-Club] Managing memory from Coq - Correction, Lionel Elie Mamane
      - Re: [Coq-Club] Managing memory from Coq - Correction, Makarius
  - Re: [Coq-Club] Managing memory from Coq - Correction, JAEGER, Eric (SGDN)
    - Re: [Coq-Club] Managing memory from Coq - Correction, Fr�d�ric Besson
      - Re: [Coq-Club] Managing memory from Coq - Correction, Benjamin Gregoire
        
        Re: [Coq-Club] Managing memory from Coq - Correction, JAEGER, Eric (SGDN)
        
        Re: [Coq-Club] Managing memory from Coq - Correction, marko
        
        [Coq-Club] Big inductive proofs, Jean Goubault-Larrecq
        Re: [Coq-Club] Big inductive proofs, Roland Zumkeller
        Re: [Coq-Club] Big inductive proofs, Jean Goubault-Larrecq
        Re: [Coq-Club] Big inductive proofs, Jean Goubault-Larrecq