Hello caml-list,

We Coq developers were given a fancy bug report by Andrew Appel
regarding Coq 8.5 memory usage that spawned quite a lot of distinct
discussions related to several performance issues. Although most of them
were solved, there is one which I believe is not due to Coq but rather
to OCaml. Here is the issue.

> 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.)
> 
> That is, run Coq 8.4pl6 in a 32-bit Windows binary, on some script 
> that takes many gigabytes to process, and see what is the maximum 
> memory usage is before it dies. It should be about 2048 megabytes. 
> Then run the same script in Coq 8.5 32-bit Windows binary, and 
> measure the same.  In the case of bug 4547, it was 1848 MB.  Can the 
> same disparity be measured under Linux?  What is causing Coq to lose 
> the use of the last 200MB of a 31-bit address space?

Note that

> 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.

What do you OCaml experts think about this? Has there been some change
in the runtime that could explain this problem?

Thanks,
PMP