coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq Ocaml version

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Cc: Xuanrui Qi <xqi01 AT cs.tufts.edu>, Emilio Jesús Gallego Arias <e AT x80.org>
Subject: Re: [Coq-Club] Coq Ocaml version
Date: Fri, 15 Mar 2019 11:00:09 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-vs1-f49.google.com
Ironport-phdr: 9a23:NZb74xHFqyzy4j9L1zUgJJ1GYnF86YWxBRYc798ds5kLTJ78osqwAkXT6L1XgUPTWs2DsrQY0rKQ6/mocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmSaxbaluIBmrsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95eWCxPAIyyb4UBAekcM+hGs4bzqEADrQenBQS2GO/j1iNEi33w0KYn0+ohCwbG3Ak4EtwQsHTTttL1O78RXuC0yanIyCvMb+lT2Tjn7ojIdA0qrPaQXbJwb8XRzlMjFgLEjlWVrIzlPiiY1usIs2eB7upgUfijhHIgqwF0uzWiwNonhIrRho8N1FzI6SF0zJw2KNC4UkJ3f8OoHZlKuyyVM4Z7RN4pTXtytyYg0LIGvIa2fCgUx5QjwB7Sc/mHfJKJ4hLnTeqRPyx4iG98dLKxiBu/9VKsyuL7Vsmz31ZKqjRKnsPQuXAK0hzf8smHSv1j8Ue9wTuDyRzf5+VeLU03lafXMYAtzqMym5YJvknOGjf6mEDsg6+XckUk9PKo6+PiYrj+up+cN5F7igbkPqUvm8y/BOE4MgkVUmiU/OSzzrzj/UnjTLpWif02l7HVsIrGKsQDuq65HwhV354/5Ba4FjeqycgXnX0aLF1eYx+HlIjoO1TWIP/iF/u/glKskC1qx//cJLHhDI/NfTD/l+LKeq81wEpBwkJnxtdGoplQF7spIfTpW0a3usaOXTEjNAnh/+ZmD+JP14YbVHiKC6mfePfOsVKPoPAuJuyNTIAQsTf5bfMi4qi93jcChVYBcPzxjtMsY3eiE6Ejeh3BOCu+spI6CW4P+zEGYqnvgVyGXyRUYi/rDa057zA/TomhCNWaH9z/sPm6xC6+W6ZuSCVeEFnVSCXncoyFX7EHbyfAepY8wAxBbqCoTsoa7T/rtAL+zOA6fO/d+yldq4m6kdYptqvckhY98TEyBMOYgTmA

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.

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?

Le ven. 15 mars 2019 à 08:45, Laurent Thery
<Laurent.Thery AT inria.fr>
a écrit :
>
>
>
> > The version I do recommend is 4.07.1+flambda with configure flags
> > "-flambda-opts '-O3 -unbox-closures'"
>
> Could not figure out how to do this in opam.
>
> Manage the first step
>
> opam switch create 4.07.1+flambda
>
> but then how do I tell to use the optim
> "-flambda-opts '-O3 -unbox-closures'" to build Coq
>
> What should I write?
>
> opam install coq --???
>
>
> > -Ray
> >

[Coq-Club] Implementation of Coq's automation tactics, Xuanrui Qi, 03/08/2019
- Re: [Coq-Club] Implementation of Coq's automation tactics, Joomy Korkut, 03/08/2019
  - Re: [Coq-Club] Implementation of Coq's automation tactics, Gaëtan Gilbert, 03/08/2019
- [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