coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq Ocaml version

From: Emilio Jesús Gallego Arias <e AT x80.org>
To: Théo Zimmermann <theo.zimmi AT gmail.com>
Cc: Coq Club <coq-club AT inria.fr>, Xuanrui Qi <xqi01 AT cs.tufts.edu>
Subject: Re: [Coq-Club] Coq Ocaml version
Date: Fri, 15 Mar 2019 18:28:26 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:UXNBIh0bu2tVFtC2smDT+DRfVm0co7zxezQtwd8Zse0TLvad9pjvdHbS+e9qxAeQG9mCs7Qc0qL/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHOfwlEniaxba5vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7Vq4/Vyi84Kh3SR/okCYHOCA/8GHLkcx7kaZXrAu8qxBj34LYZYeYP+d8cKzAZ9MXXWpPUNhMWSxGDIOyYYkAAekPMulXs4bzqEADrQenBQS2GO/j1iVFi33w0KYn0+ohCwbG3Ak4EtwBtXTUrdH1NKYVUe+tyKfH0y7Dd+lN2Tjl6YbHaBQhofWSUrJ/dsre0VUiFxnEjlqKsozuIjSY2foWvmmU7OdsSfiji2k9qwF+uzWiwNonhIrRho8N11zJ9iZ0zJwrKdGmSUN3e8OoHZlNuy2AKod7TN0uT3l1tCs0yLAKo4O3cSwFxZg9xRPSZeaLf5aW7h/jUuuaPC12i2h/eL2lgha/6UigxfP4VsmzyFtLoSlInsXWunAKzRzT5dCLSvp7/ki/xTaCzx3f5+JHLEwui6bXNZ8szqQtmpcRrEjPBDL6lUvogKOOc0Ur4Omo6+DpYrX8oZ+cMpd5hR/lP6UhmcGzHf40Mg8UX2iU4ei8zqHs/VXlQLVWif07irXWsJfDJcgCuqG5BxJV3Z045hakDzam1cwYkmMdIFJEfhKHlYnpNEvULPD2F/fsy2irxQtrRveODLzkB5jXK3HFlv+1YbZw7AhOyQ82zPhQ4ptVDvcKJ/elCWHrs9mNIxo4Nw2z9MTqE0dm4awXXWaCDaiuGbnTuETAsu8HM7nUIogPt2CueLAe+/fygCphyhcmdq6z0M5SMSjgR6U0EwCieXPpx+w5PyIPtws6QvbtjQzQQW4LIXGoUPBlv21pOMedFY7GA7uVrvmZxi7qTI0GPiZBEF/eSS61JbXBYO8FbWepGuEkkjEAUunzW995kxa0u12jxg==
Organization: X80 Heavy Industries

Théo Zimmermann
<theo.zimmi AT gmail.com>
writes:

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

Unfortunately these set of flags is only "safe" in 4.07.1, so it is a
bit tricky to setup OPAM to apply them only in that case.

I hope that 8.10 opam will be much improved in that regards, but not
100% sure yet.

> Another question in passing: what is the support for building with
> flambda using Coq's Dune build system? Is it necessary to run
> configure manually? Can we avoid this?

The current Dune setup does indeed set the optimizing flags by default
when using release mode [it doesn't enable native so this is not a
problem in < 4.07], however the profile also needs more tweaking.

E.

[Coq-Club] Coq Ocaml version, (continued)
- [Coq-Club] Coq Ocaml version, Laurent Thery, 03/14/2019
  - Re: [Coq-Club] Coq Ocaml version, CYRIL SIX, 03/14/2019
  - Re: [Coq-Club] Coq Ocaml version, Emilio Jesús Gallego Arias, 03/14/2019
    - Re: [Coq-Club] Coq Ocaml version, Xuanrui Qi, 03/14/2019
      - Re: [Coq-Club] Coq Ocaml version, Laurent Thery, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Théo Zimmermann, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Gaëtan Gilbert, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Ian, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Théo Zimmermann, 03/15/2019
        Re: [Coq-Club] Coq Ocaml version, Emilio Jesús Gallego Arias, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Emilio Jesús Gallego Arias, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Emilio Jesús Gallego Arias, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Laurent Thery, 03/16/2019
      - Re: [Coq-Club] Coq Ocaml version, Emilio Jesús Gallego Arias, 03/15/2019