From: Xavier Leroy <xavier.leroy@inria.fr>
To: "Pierre-Marie Pédrot" <pierre-marie.pedrot@inria.fr>, caml-list@inria.fr
Subject: Re: [Caml-list] Decrease in addressable memory on Windows 32-bits between 3.12 and 4.01?
Date: Mon, 15 Feb 2016 11:41:54 +0100 [thread overview]
Message-ID: <56C1AB72.90304@inria.fr> (raw)
In-Reply-To: <56C1A17D.9020902@inria.fr>
On 15/02/2016 10:59, Pierre-Marie Pédrot wrote:
>> Can I ask you all about my observation that max memory available in
>> 32-bit Coq 8.5 is less than max memory available in 32-bit Coq
>> 8.4pl6? (The 2nd-to-last paragraph of my original bug report.)
[...]
>> Coq 8.5 is compiled with 4.01 on windows. Coq 8.4 was compiled with
>> 3.12 IIRC.
>
> so I am led to think that this has to do with OCaml runtime, as I can't
> really see where this would come from the Coq codebase.
For the reasons that Enrico mentioned, it could come from the Coq code
base, so it would be best to use the same version of Coq to investigate
this issue.
This could be related to http://caml.inria.fr/mantis/view.php?id=6990
or not. (I don't know whether the heap growing policy changed between
OCaml 3.12 and OCaml 4.01).
It's helpful to run with OCAMLRUNPARAM=v=4 to monitor how much memory
OCaml requests from the OS and at which points in program execution.
- Xavier Leroy
prev parent reply other threads:[~2016-02-15 10:41 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2016-02-15 9:59 Pierre-Marie Pédrot
2016-02-15 10:09 ` Enrico Tassi
2016-02-15 10:41 ` Xavier Leroy [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=56C1AB72.90304@inria.fr \
--to=xavier.leroy@inria.fr \
--cc=caml-list@inria.fr \
--cc=pierre-marie.pedrot@inria.fr \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).