coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq Ocaml version

From: Xuanrui Qi <xqi01 AT cs.tufts.edu>
To: coq-club AT inria.fr, Laurent Thery <Laurent.Thery AT inria.fr>
Subject: Re: [Coq-Club] Coq Ocaml version
Date: Thu, 14 Mar 2019 15:43:12 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=xqi01 AT cs.tufts.edu; spf=None smtp.mailfrom=xqi01 AT cs.tufts.edu; spf=None smtp.helo=postmaster AT vm-delivery1.eecs.tufts.edu
Ironport-phdr: 9a23:8QvWzRd2Aas3mftJUTo2ldemlGMj4u6mDksu8pMizoh2WeGdxcSzYB7h7PlgxGXEQZ/co6odzbaP6+a4ACQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagfb9+Ngm6oRjMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v9LlgRgP2hygbNj456GDXhdJ2jKJHuxKquhhzz5fJbI2JKPZye6XQds4YS2VcRMZcTy9PDJ68YYURAeQOP+hYoJXzqFQBohWzHhWsCeD1xzNUmnP7x6833uI8Gg/GxgwgGNcOvWzVo9XoLqgSV/q1zLTJzT7edP1W2Cr25Y/HcxA4oPGAQa98fNHNxkk0DQ/FkkiQqYL5PzOOzOgCrXWU7/d5WO+plmUppQZxoj21ycctjInEno0Uyk3e+iV/2oY1ONy4SFd6YdK+DJRQsCSaOo1rSc0hW2FloDs2x7MatZKhfSUHx44rywDRZvCdfYWF4ArvWPiNLTp8nn5oeaizihm8/ES61+HxV8u53VBXpSRfiNbMrGoC1xnL58iHVPR9+kCh1C6R1wDW8+1LPF47la7aK54/3LEwjJoSvVnZEiDohkr5kLSWel84+ui15eTnfq7mqoWCOIBplwHyKqUumsqhDuQkKgUCQmaW9fim2LDi8kD1WqtGg/MsnqTXsp3WPcEbqbS4Aw9R3IYj8RG/DzK+3dUXhHkHLU5JdA+cgof1IFHCOuz4Deqxg1Swizdn3e7JMaD8ApnVNHjMjK/hfaph605b0Acz0dBf6IxOCrABO//yW07xtNnDAR8jKQO42efnCNNn1oMfQ22DGKGZMLnKu1+S+u0vO/WMZJMSuDvlN/cl4OfugWYlll8ZYKmmxoAaaGu4H/RjO0WWe2DggtYHEWcQvwoxVvbmiFOYUW0bW3HnVKUlozo/FYiODIHZR4nrjqbFlAOyA4dbYHwONlCBC2agI6GNRu0Bbj7UHs9siC0sVL67SoZn2wv45yHgzL8yHvfd/DcFtNra1ZAh9/TSzUga/icyE9mTz3rLQm1pyDBbDwQq1bxy9BQugmyI1rJ11rkBTYQKtqF5FzwiPJuZ9NRUTtX7WwbPZNCMEQr0Sc7gHSw/Usl3ztMTMR4kR4eSyyvb1i/vOIc70qSRDcVooKnHmWTsKdpmjXvKyft51gR0co50LWSjw5VH2U3TCorOyRTLiaPveakY3TDA7nbai2eDt1oeTBN+Tb6DUHwCNBPb

But beware that this configuration can make compiling Coq consume a lot
of memory (on my machine, up to 15G). If you don't have a lot of
memory, compilation will fail.

-Ray

--
Xuanrui (Ray) Qi

xqi01 AT cs.tufts.edu
me AT xuanruiqi.com
https://www.xuanruiqi.com

On Thu, 2019-03-14 at 13:29 +0100, Emilio Jesús Gallego Arias wrote:
> Laurent Thery
> <Laurent.Thery AT inria.fr>
> writes:
>
> > what is the recommended Ocaml version for Coq 8.9?
>
> The version I do recommend is 4.07.1+flambda with configure flags
> "-flambda-opts '-O3 -unbox-closures'"
>
> E.
>

[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