The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Xavier,

> 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" ?

I think Andrew is using the MinGW version compiled with my scripts (that is 
the version downloadable under the link Andrew gave). There is absolutely no 
Cygwin involved in running this version (only in building it).

The reason that the IMAGE_FILE_LARGE_ADDRESS_AWARE exists is that some old 
compilers (in the really old days) did treat pointers as signed numbers in 
comparison, so that if you have an array spanning the signed/unsigned wrap at 
2GB, it could happen that say &a[0]>&a[1]. The IMAGE_FILE_LARGE_ADDRESS_AWARE 
flag tells the system that the binary treats pointers as unsigned values and 
it is safe to give it memory at large addresses. Unless a binary has this 
flag set, Windows won't give it more than 2GB user VM. On 32 bit Windows this 
is not a problem since only server versions of 32 bit Windows allow more than 
2 GB user VM anyway. For this reason it is the default to not set this flag 
on 32 bit Windows. But when running 32 bit binaries on 64 bit machines, it 
makes a difference.

Since no Linux program would use signed pointer compares, Cygwin might have 
chosen to set IMAGE_FILE_LARGE_ADDRESS_AWARE by default while MinGW might 
follow the Windows standard (although no program compiled with MinGW gcc 
would have such a restriction either).

So if OCaml for Cygwin behaves differently than OCaml for MinGW we should 
research and fix this. Can you please check if your Cygwin compiled binaries 
have the IMAGE_FILE_LARGE_ADDRESS_AWARE flag set?

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928