coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [ANN] Raising the minimal OCaml version for Coq 8.10 to 4.05.0

From: Bernhard Schommer <bernhardschommer AT gmail.com>
To: coq-club AT inria.fr, theo.zimmi AT gmail.com
Subject: Re: [Coq-Club] [ANN] Raising the minimal OCaml version for Coq 8.10 to 4.05.0
Date: Mon, 24 Sep 2018 16:49:26 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bernhardschommer AT gmail.com; spf=Pass smtp.mailfrom=bernhardschommer AT gmail.com; spf=None smtp.helo=postmaster AT mail-vs1-f67.google.com
Ironport-phdr: 9a23:VQKnpxOSah9gS7R14Nkl6mtUPXoX/o7sNwtQ0KIMzox0Lfr5rarrMEGX3/hxlliBBdydt6obzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlKiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgIOT428mHZhMJzgqxGvhyuuxNxzpXIYIGMLvdyYr/Rcc8YSGdHQ81fVzZBAoS5b4YXEucOI/xYr4/9p1QUtxuxGBSnCv7zxT9IgX/22Kg63Po7EQrb2wEvBMwBsG7SrNX1LqgSS/26zLLUwjXDaPNW3DL955bSch06rvGMWKh/ccvVyUU1CwzFiVCQpJXjMjiI1eoNq3CW4/R8We+rkWIqqAF8riKxyssxiITFnIMYx1LC+C5k2og6P8e4R1R+YdO8EJtfqSWaN4xuT8MnWW5ouSI6xqQYuZ6gYSQG0Zonyh/dZvCdfIiI5RXjVOmVIThmnn5qZLW/hxOq/UihzO3zSNW03U5UoiZZltTArHMA2hzJ5sSZV/dw/F2t1DeN2gzL7+FLO0E0la7VK547xb4wk4Ievl/dES/snkX2jLWZdl859eiz9+vnYrLmppqZN4BqkAHzKasumsmlDuQ5NggCRXSU+eO51LH75032XK1KjuEqkqneqJ3VOcMbpregDwBJ1oYj9g2wAiy90NUYmHkHNEhKdAiGj4jvIVHOIer3Ae2xg1S2w39XwKXNOaSkCZHQJFDClq3gdPBz8QoU1Ao+ypZN5pdRC5kOJfvyXgn6s9mLIAU+NlmezvzhCNxn2sslUmKIB6qUKuuGu1KS4OImOeWXb48SvTPwMdAq4vfviTkynlpLLvrh5ocedH3tRqcuGE6ee3e52o5QQ1dPhRI3SanRsHPHVDdSY3ioWKdlv2M0DYunCcHIQYX/2eXdjhf+JYVfYyV9Mn7JCW3hLtzWVPIFaSbUKchkwGRdCOqRDrQ53BTrjzfUjrpqKu2Op38dvJPnkcZuvqjdy050+jtzAMCQlWqKSjMskw==

Another point why shifting to OCaml 4.05 is a good idea: This version
contains a workaround for the problems caused by a gcc optimization
that triggered the skylake bug.

Best,
-Bernhard
Am Sa., 22. Sep. 2018 um 18:45 Uhr schrieb Emilio Jesús Gallego Arias
<e AT x80.org>:
>
> Théo Zimmermann
> <theo.zimmi AT gmail.com>
> writes:
>
> > Emilio meant: at the time of the release of Coq 8.10, Debian Buster will
> > be
> > the new stable version and it contains indeed OCaml 4.05. Unfortunately,
> > given that Debian doesn't announce clear release dates, it is not clear
> > that Debian Buster will really be the new stable at the time of the
> > release
> > of Coq 8.10.
>
> Indeed, that's what I mean. Debian has gotten better at releasing more
> consistently, so indeed Coq 8.10 and Debian Buster should arrive close
> enough.
>
> Anyways, an important practical consideration is that Debian Buster
> users should be able to get packages for Coq 8.10, 8.11, 8.12 without
> too much trouble. [well, Coq is so outdated in Debian sid right now that
> we should request its removal, but that's a different story]
>
> > Side question: why do you recommend using the system compiler with OPAM?
>
> Indeed, I tend to strongly recommend _against_ mixing OPAM and system
> packages. I have seen a fair amount of issues in non-expert users due to
> this configuration. Also, OPAM 2.0 may have changed in this regard.
>
> E.
>

[Coq-Club] [ANN] Raising the minimal OCaml version for Coq 8.10 to 4.05.0, Emilio Jesús Gallego Arias, 09/19/2018
- Re: [Coq-Club] [ANN] Raising the minimal OCaml version for Coq 8.10 to 4.05.0, Ralf Jung, 09/22/2018
  - Re: [Coq-Club] [ANN] Raising the minimal OCaml version for Coq 8.10 to 4.05.0, Théo Zimmermann, 09/22/2018
    - Re: [Coq-Club] [ANN] Raising the minimal OCaml version for Coq 8.10 to 4.05.0, Emilio Jesús Gallego Arias, 09/22/2018
      - Re: [Coq-Club] [ANN] Raising the minimal OCaml version for Coq 8.10 to 4.05.0, Bernhard Schommer, 09/24/2018