Just to relay here some remarks made by Emilio in the Coq Workshop final session: it seems the OCaml team has some plans to look at Coq performance in OCaml 5 this fall.
For reference, below is the building time for a nontrivial but not huge Coq project on my machine (Coq 8.17.1, one thread). I believe this slowdown is typical and warrants flagging up to people that they should avoid 5.0.0 if possible.
OCaml 5.0.0:
real 3m24.228s
user 2m55.947s
sys 0m14.168s
OCaml 4.14.1:
real 2m25.702s
user 2m2.404s
sys 0m7.926s
Karl Palmskog said:
I believe this slowdown is typical and warrants flagging up to people that they should avoid 5.0.0 if possible.
The documentation of Coq already contains this sentence: "While Coq supports OCaml 5, users are likely to experience slowdowns ranging from +10% to +50% compared to OCaml 4."
Also, I did report this issue to OCaml's developers at the time and the main issue. It was a poor interaction between the garbage collector and the dynamic linker, so this constant overhead had a terrible impact when compiling small .v
files. It was quickly fixed, but OCaml 5.0.1 has not been deemed worth releasing for just that issue.
so it will be fixed in 5.1?
by "flagging up" I meant we can communicate it [warnings about OCaml 5.0.0] also in other venues besides the release notes, such as the Coq Platform and other release announcements
Yes, you can already try it with 5.1.0+beta, which was recently released.
Karl Palmskog said:
such as the Coq Platform and other release announcements
The Coq platform ships its own version of OCaml, which is not 5.0. As for the sentence I quoted, it was part of the announcement of Coq 8.17.
not a serious benchmark, but 5.1.0~beta1 is seemingly between 4.14.1 and 5.0.0 in terms of performance for a mid-size Coq project:
OCaml 5.0.0:
real 3m24.228s
user 2m55.947s
sys 0m14.168s
OCaml 5.1.0~beta1:
real 2m54.134s
user 2m28.455s
sys 0m10.957s
OCaml 4.14.1
real 2m25.702s
user 2m2.404s
sys 0m7.926s
Last updated: Oct 13 2024 at 01:02 UTC