The Coq mailing list

[Xavier Leroy <xavier.leroy AT inria.fr>]

Dear Andrew,

On 26/04/2018 20:57, Andrew Appel wrote:

> Since that time, ocaml has gotten worse:  ocaml version 3 could support 2.0 
> gigabytes in 32-bit mode, but ocaml version 4 can support only 1 gigabyte 
> in 32-bit mode, because someone has made the bad decision to reserve part 
> of the address space for some other purpose.  I don't know the details; I 
> wish someone would permit me to run 4-gigabyte ocaml binaries in 32-bit 
> mode, but that's another story.  So I can no longer run my 1.6-gigabyte Coq 
> executions in 32-bit mode. 

You should address those remarks to us OCaml folks, e.g. on the user's
mailing list 
caml-list AT inria.fr
 or through a bug report at
https://caml.inria.fr/mantis/

However, your claim makes no sense to me.  I just checked with the
latest OCaml (4.06.1) on Ubuntu 17.04 32 bits, and I can allocate 
3.3 Gb just fine.  

My suspicion is that it's your Cygwin that limits memory usage.  Maybe
the default limit is lower now than it was earlier.  Perhaps you could
check "ulimit" ?

- Xavier Leroy