Michael Soegtrop (Sep 15 2020 at 17:17): Michael Soegtrop (Sep 15 2020 at 17:17):Dune depends on a secondary OCaml compiler when the system OCaml compiler is too old (4.07.1). This is problematic on Windows where one generally needs patched up OCaml compilers, so the build of the secondary compiler fails, which in turn has the effect that the opam chosen default dune fails to build. I fixed this by disabling the secondary OCaml compiler on windows - opam chooses a dune matching the OCaml version then.
I wonder if there are really projects which use an older OCaml compiler but require a newer dune, so that this, well, hack - which also takes a bit of build time btw - is justified.
Karl Palmskog (Sep 15 2020 at 17:23):@Michael Soegtrop so which Dune version do you get then? It sounds like this might be a version without any Coq support (which would be sad for the Coq Platform)
Rudi Grinberg (Sep 15 2020 at 17:32):If you are trying to build dune on a recent version of OCaml, the secondary compiler will not be built. If you look at the opam file, the dependency on the secondary compiler is only for old versions of OCaml. So I'm not sure why opam is unable to pick up that you're using a recent version of the compiler.
Théo Zimmermann (Sep 15 2020 at 17:38):The platform is currently built with 4.07.1, that's why.
Théo Zimmermann (Sep 15 2020 at 17:40):And the reason why is that OCaml >= 4.08 is known to have performance bugs (see https://coq.discourse.group/t/install-notes-on-coq-and-ocaml-versions-configuration/713)
Karl Palmskog (Sep 15 2020 at 18:06):I would say OCaml 4.07.1 is the best OCaml version the world has ever seen if you're a Coq user
Karl Palmskog (Sep 15 2020 at 18:07):it may have its issues, but they are dwarfed by those for 4.05.0, 4.08.1, etc.
Michael Soegtrop (Sep 15 2020 at 18:43):@Karl Palmskog : I get dune version 2.7.0b. Would this be acceptable? How hard would it be to build a later dune with 4.07.1? Maybe I just patch the opam file and give it a try ...
Karl Palmskog (Sep 15 2020 at 19:23):@Michael Soegtrop version 2.7.0b is fine, the important threshold was at 2.5 vs 2.4
Michael Soegtrop (Sep 15 2020 at 19:31):@Karl Palmskog : pefect - I go for that option then.
Rudi Grinberg (Sep 16 2020 at 00:17):Do you have an idea which version of OCaml you'll be able to upgrade to in the near/medium future?
Rudi Grinberg (Sep 16 2020 at 00:18):Next time before dune drops support for a version of OCaml, I'll bring up the impact on the coq platform.
Karl Palmskog (Sep 16 2020 at 08:46):it seems unlikely the Coq Platform will go beyond 4.09 in the near future, even for Coq 8.13. But the final decision (to go from 4.07.1 to some higher version) will probably be taken in light of outstanding bugs and so on, so hard to tell right now.
Michael Soegtrop (Sep 16 2020 at 08:47):@Rudi Grinberg : on Windows 4.07.1 is currently the only reasonably supported version (the only one for which opam works at least somehow) and I want to use the same OCaml version on all systems. As far as I know INRIA is working on improving the situation, but I do not have a timeline. I am somewhere between hope and confident that this will be ready for Coq platform 8.13. @Théo Zimmermann : can you comment on this?
On Windows the current situation is that there is a separate opam repo at (https://github.com/fdopen/opam-repository-mingw) maintained by Andreas Hauptmann which does work for what Coq needs from OCaml.
Théo Zimmermann (Sep 16 2020 at 09:42):I don't know how the work of Antonin which I contributed to supervise ended after he started being mentored by OCamllabs people but the opam team is announcing the next release as the "Windows release" (don't put too high hopes in a release for Coq 8.13 or even 8.14 though).
Emilio Jesús Gallego Arias (Sep 16 2020 at 11:54):Karl Palmskog said:
I would say OCaml 4.07.1 is the best OCaml version the world has ever seen if you're a Coq user
We have no idea on how 4.11 does perform, it could indeed do better; but unfortunately we have lost our independent benching capability so right now it is not possible to run that kind of benches unless you open a draft PR which would by the way waste a lot of other CI resources :S
It seems strange to me the way the bench situation was handled.
Karl Palmskog (Sep 16 2020 at 11:58):I agree 4.11 could be good as well, but I was not talking just about performance here, but combination of stability, wide support, benchmark numbers
Emilio Jesús Gallego Arias (Sep 16 2020 at 11:58):On the other hand using >= 4.08 is tricky due to Coq linking bugs; these are Coq bugs and OCaml does fine in rejecting the invalid code
But I do contest that 4.07 is the best OCaml version for Coq, that's at least debatable; myself I use 4.11 for development for example
Karl Palmskog (Sep 16 2020 at 12:04):to a Coq user, why would it make difference whether a bug is in Coq or OCaml w.r.t. choosing OCaml version? I can't use Unicoq or Mtac2 on 4.11, whether due to Coq or OCaml is irrelevant if I'm just a user
Karl Palmskog (Sep 16 2020 at 12:05):for 4.11 and performance, the burden unfortunately falls on devs to demonstrate that it doesn't lead to performance issues (when we know 4.07.1 doesn't have such issues)
Karl Palmskog (Sep 16 2020 at 12:07):my point is that "best for Coq" and "best for Coq users [of the platform]" can be quite different
Paolo Giarrusso (Sep 16 2020 at 19:28):(no preference but) Coq bugs might be easier to fix?
Paolo Giarrusso (Sep 16 2020 at 19:29):@Emilio Jesús Gallego Arias aren’t _you_ the source for “4.07.1 is best”?
Paolo Giarrusso (Sep 16 2020 at 19:30):in this case, if the problem is a unicoq/mtac limitation, that might be fixable, especially _if_ 4.11(+flambda?) beats 4.07.1+flambda
Paolo Giarrusso (Sep 16 2020 at 19:31):sorry let me rephrase
Karl Palmskog (Sep 16 2020 at 19:32):unicoq/mtac2 were just examples, there are other plugins that have limited versions
Paolo Giarrusso (Sep 16 2020 at 19:33):under those conditions, there’d be more motivation for certain industrial users (hint hint) to upgrade ocaml and try porting the plugins they use/contribute to (hint hint)
Emilio Jesús Gallego Arias (Sep 16 2020 at 20:05):4.07.1 is the version I recommend to users, indeed, but 4.11.1 has some goodies
Emilio Jesús Gallego Arias (Sep 16 2020 at 20:05):including best-fit which is supposed to improve certain scenarios
Emilio Jesús Gallego Arias (Sep 16 2020 at 20:05):so maybe 4.11.1 can do work very well
Emilio Jesús Gallego Arias (Sep 16 2020 at 20:06):also 4.11 etc... have other advantages
Emilio Jesús Gallego Arias (Sep 16 2020 at 20:06):but indeed GC numbers are still looking bad sadly
Emilio Jesús Gallego Arias (Sep 16 2020 at 20:06):https://gitlab.com/coq/coq/-/jobs/741519502
Emilio Jesús Gallego Arias (Sep 16 2020 at 20:06):will report upstream
Emilio Jesús Gallego Arias (Sep 16 2020 at 20:06):see also this JS post
Emilio Jesús Gallego Arias (Sep 16 2020 at 20:06):https://blog.janestreet.com/memory-allocator-showdown/
Emilio Jesús Gallego Arias (Sep 16 2020 at 20:10):on the other hand best-fit improves some numbers, so let's see
Emilio Jesús Gallego Arias (Sep 17 2020 at 13:41):Recent numbers on 4.07.1 vs 4.11.1 are fairly mixed, for example fourcolor is 11% faster on 4.11 ; so the picture is kinda mixed, also 4.11 does provide better memory consumption with best-fit in some cases
Gaëtan Gilbert (Sep 17 2020 at 14:11):ocamldebug is uselessly slow on 4.10+ IME
Emilio Jesús Gallego Arias (Sep 17 2020 at 14:13):have we reported it?
Gaëtan Gilbert (Sep 17 2020 at 14:14):Last updated: Oct 13 2024 at 01:02 UTC