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

[Emilio Jesús Gallego Arias]

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

[Ralf Jung]

Hi,

Post by Emilio Jesús Gallego Arias
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

That's not correct, latest Debian stable has OCaml 4.02.3

Also, many OPAM users (I think) will be impacted by this: The default behavior
of OPAM (and the one I personally usually recommend) is to use the system OCaml.

Kind regards,
Ralf

[Théo Zimmermann]

Hi,

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. Note that we have already proceeded like this in the past:
bumping the minimum required version of OCaml for the development version
before the release of Debian with the corresponding version.

Side question: why do you recommend using the system compiler with OPAM?

Best,
Théo

Post by Ralf Jung
Hi,

Post by Emilio Jesús Gallego Arias
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

That's not correct, latest Debian stable has OCaml 4.02.3
Also, many OPAM users (I think) will be impacted by this: The default behavior
of OPAM (and the one I personally usually recommend) is to use the system OCaml.
Kind regards,
Ralf

[Emilio Jesús Gallego Arias]

Post by Théo Zimmermann
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]

Post by Théo Zimmermann
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.

[Bernhard Schommer]

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

Post by Emilio Jesús Gallego Arias

Post by Théo Zimmermann
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]

Post by Théo Zimmermann
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.

[Ralf Jung]

Hi,

Post by Théo Zimmermann
Side question: why do you recommend using the system compiler with OPAM?

Mostly to save tons of time and space. I have plenty of switches.

; Ralf

Post by Théo Zimmermann
Best,
Théo
Hi,

Post by Emilio Jesús Gallego Arias
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

That's not correct, latest Debian stable has OCaml 4.02.3
Also, many OPAM users (I think) will be impacted by this: The default behavior
of OPAM (and the one I personally usually recommend) is to use the system OCaml.
Kind regards,
Ralf