From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 1CC477FCD9 for ; Mon, 15 Feb 2016 11:41:58 +0100 (CET) X-IronPort-AV: E=Sophos;i="5.22,449,1449529200"; d="scan'208";a="164752322" Received: from estephe.paris.inria.fr (HELO [128.93.64.229]) ([128.93.64.229]) by mail3-relais-sop.national.inria.fr with ESMTP; 15 Feb 2016 11:41:54 +0100 To: =?UTF-8?Q?Pierre-Marie_P=c3=a9drot?= , caml-list@inria.fr References: <56C1A17D.9020902@inria.fr> From: Xavier Leroy Message-ID: <56C1AB72.90304@inria.fr> Date: Mon, 15 Feb 2016 11:41:54 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0 MIME-Version: 1.0 In-Reply-To: <56C1A17D.9020902@inria.fr> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] Decrease in addressable memory on Windows 32-bits between 3.12 and 4.01? 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