The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

"This configuration" includes the use of the OCaml flambda compiler.
My point was that, in case the flambda compiler is not used, the
options are (probably, but this needs to be confirmed) harmless. In
this case, there is no problem in changing the default value of these
options, as it only affects the users of the flambda compiler.

Le ven. 15 mars 2019 à 17:56, Ian 
<itz AT very.loosely.org>
 a écrit :
>
> On 2019-03-15 11:00, Théo Zimmermann wrote:
>
> > That's a good point. This is something you can pass as argument to
> > configure when building Coq from sources, but not when using opam.
> > Emilio, if this is the default recommended flambda-opts value, why not
> > put this as the default? Or does it have an impact when building
> > without flambda? If that's not the case, the opam package could be
> > changed to use this configure flag.
>
> Up the thread someone wrote:
>
> Some1> But beware that this configuration can make compiling Coq consume
> Some1> a lot of memory (on my machine, up to 15G). If you don't have a
> Some1> lot of memory, compilation will fail.
>
> If _this_ is true, I definitely cannot afford to use these options.
> Please do not change the default unless there is a way to override it.
>
> --
> Please don't Cc: me privately on mailing lists and Usenet,
> if you also post the followup to the list or newsgroup.
> To reply privately _only_ on Usenet and on broken lists
> which rewrite From, fetch the TXT record for no-use.mooo.com.