coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Emilio Jesús Gallego Arias <e AT x80.org>
To: coq-club AT inria.fr
Subject: [Coq-Club] [ANN] Raising the minimal OCaml version for Coq 8.10 to 4.05.0
Date: Wed, 19 Sep 2018 23:21:11 +0200
Authentication-results: mail3-smtp-sop.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:aiMhsR0M+UVRKNW5smDT+DRfVm0co7zxezQtwd8Zse0VIvad9pjvdHbS+e9qxAeQG9mDtLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiDkJOSM+8G/ZicJ/gq1Urw66qhxj34LZep2ZOOZkc67fe94RWGpPXtxWVyxEGo6yYI4PD+sFPeZZqInyv18AogWlBRG2H+Pg0j5GiWXy3a0+zeshHgbG0xQ8EtIUsXTbts71P7oVXO+r16TJwjbOY+9M1Tf68ojIfQksrPeRVrx+dsrRzFMgFwLDjliIqIzlOSmV1uUXvGSB4epgT/qji2EmqwFtojiv29wjhpPViYISz1DJ8zhyzoUtJdCgVUJ2Yt2pHIFOuy2ENoZ6WN4uTmN1tCog17ELt4C3cDAIxZkl3RLTdvKKfomS7h7+V+udOzR1iXBjdbminRi961Kgxff5VsSs0FZFsC5Fkt7Uu3EC1BHf9tKLSvxn/keuwTqP1gbT5f9YIU0siKbWKJ0szqQumpYNsEnPBDL6lUfrgKOMa0kp9Pak5/ziYrr8p5+cM4F0ihv5MqQrgsGwH/81MwcNUmSH4+i806fj/ULhTLVQkvI2irXZsIzdJckDuqG5BBZV3p8/5Ba7Ejepy88VnWIHLVJAYBKIlZLlO1DIIPDiDPewmU6gkDlxx6OOArq0CZLUa3PHjb3JfLBn6kcaxhBg48pY4sd5D7AFIfXEeELqJsfvIRY9NwG7xNHOEtR0zctKVEqfUvffN7nd5wzbrtkzKvWBMddG8A32LOIosqa33C0J3GQFdKzs5qM5LXWxH/BoOUKcMCj80o9HFn0F7FNnEL7azWaaWDsWXE6cGrom72BpGNL+S4DZSdL12eHT7GKABpRTI1t+JBWMHHPvJteUC69KbzidcJZs
Organization: X80 Heavy Industries

Dear Coq users,

Coq 8.9 will require OCaml >= 4.02.3, however, there is strong support
among developers to target OCaml >= 4.05.0 for Coq 8.10 (scheduled
Spring 2019).

OCaml 4.02 was released in Aug 29, 2014, and much progress and many
useful features have since then been incorporated by the amazing OCaml
team; no doubt Coq can make good use of them.

It is however clear to the Coq team that this is a potentially impactful
change, and we would like to hear from users before proceeding with the
change.

Please leave your feedback here or in the corresponding issue / PR:

- https://github.com/coq/coq/issues/7380
- https://github.com/coq/coq/pull/7522

OPAM users will see little change. For Ubuntu / Debian users, it will
mean that they will have to use the latest stable distribution [or
resort to OPAM] Most other distributions have already catch up with
4.05.0

I'd also like to take the opportunity to remind that the recommended
OCaml version for those in need of high performance is 4.07.0 with the
flambda backend enabled [4.07.0+flambda in OPAM].

A recent benchmark [1] shows significant improvement in a diverse set of
scenarios.

Best regards,
Emilio

[1] https://ci.inria.fr/coq/job/benchmark-part-of-the-branch/513/console

[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