I am using 4.07.1+flambda and considering upgrading to a newer version. But performance is really important to me because Coq compiled with it. I recall there was a web page with a benchmark of different OCaml versions but I could not find. Could somebody please remind me the URL? What is the current recommendation on what OCaml version/variant to use for performance? Thanks!
You were probably thinking of http://bench.flambda.ocamlpro.com, which is still running but is so outdated that it’s hard to get useful info; as a stroke of luck, it happens to still run with 4.07.1, so you can compare it against the current trunk (which is mislabelled as 4.08.0+trunk).
The multicore team has got some very good benchmarking tools, and I thought they also had a more up-to-date version of the benchmarks site, but I could only find http://ocamllabs.io/multicore, which is not in a much better state with respect to recent compilers.
I recommend using the most recent released version that is compatible with the projects you need. I’m not aware of any significant performance regressions. Although I’m not a Coq user, so you’d probably want to get advice from fellow Coq users before any decision.
In the past few years, you generally want to use the latest version of the compiler that is compatible with your Coq version. Every OCaml release has steadily been improving the quality of code output – I’m assuming that you’re talking about the runtime performance of your binary as opposed to compilation time.
@vlaviron: you’re thinking of http://bench.ocamllabs.io and http://bench2.ocamllabs.io, but these will take some interpretation. Not intended for casual consumption.
From this discussion: https://coq.discourse.group/t/install-notes-on-coq-and-ocaml-versions-configuration/713
OCaml versions >= 4.08 have a performance bug due to different GC strategies, we don’t recommend its use; see https://github.com/ocaml/ocaml/issues/9326 . If you must use OCaml >= 4.08 then wait for Coq 8.11.1 and use OCaml 4.10.0
So far, OCaml 4.07.1 has proven to be solid, so that’s what we recommend.
We have seen up to 10% slow down between Coq compiled with OCaml-4.07.1 and 4.09. I have not tried 4.10 yet and wanted to check benchmarks first.
This is the Coq-related benchmark I was looking for. It shows 4.10 is slower compared to 4.07.
https://ci.inria.fr/coq/job/benchmark-part-of-the-branch/865/consoleFull
It looks like comparing the performance without flambda though.