Stream: Coq devs & plugin devs

Topic: OCaml 5 performance


view this post on Zulip Karl Palmskog (Aug 01 2023 at 06:51):

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

view this post on Zulip Guillaume Melquiond (Aug 02 2023 at 07:09):

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."

view this post on Zulip Guillaume Melquiond (Aug 02 2023 at 07:10):

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.

view this post on Zulip Karl Palmskog (Aug 02 2023 at 07:11):

so it will be fixed in 5.1?

view this post on Zulip Karl Palmskog (Aug 02 2023 at 07:11):

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

view this post on Zulip Guillaume Melquiond (Aug 02 2023 at 07:11):

Yes, you can already try it with 5.1.0+beta, which was recently released.

view this post on Zulip Guillaume Melquiond (Aug 02 2023 at 07:18):

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.

view this post on Zulip Karl Palmskog (Aug 02 2023 at 07:56):

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: May 18 2024 at 10:02 UTC