Stream: Dune devs & users

Topic: dependency on secondary ocaml compiler


view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Sep 15 2020 at 17:38):

The platform is currently built with 4.07.1, that's why.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 ...

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Sep 15 2020 at 19:31):

@Karl Palmskog : pefect - I go for that option then.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Sep 16 2020 at 19:28):

(no preference but) Coq bugs might be easier to fix?

view this post on Zulip Paolo Giarrusso (Sep 16 2020 at 19:29):

@Emilio Jesús Gallego Arias aren’t _you_ the source for “4.07.1 is best”?

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Sep 16 2020 at 19:31):

sorry let me rephrase

view this post on Zulip Karl Palmskog (Sep 16 2020 at 19:32):

unicoq/mtac2 were just examples, there are other plugins that have limited versions

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2020 at 20:05):

including best-fit which is supposed to improve certain scenarios

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2020 at 20:05):

so maybe 4.11.1 can do work very well

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2020 at 20:06):

also 4.11 etc... have other advantages

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2020 at 20:06):

but indeed GC numbers are still looking bad sadly

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2020 at 20:06):

https://gitlab.com/coq/coq/-/jobs/741519502

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2020 at 20:06):

will report upstream

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2020 at 20:06):

see also this JS post

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2020 at 20:06):

https://blog.janestreet.com/memory-allocator-showdown/

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2020 at 20:10):

on the other hand best-fit improves some numbers, so let's see

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Sep 17 2020 at 14:11):

ocamldebug is uselessly slow on 4.10+ IME

view this post on Zulip Emilio Jesús Gallego Arias (Sep 17 2020 at 14:13):

have we reported it?

view this post on Zulip Gaëtan Gilbert (Sep 17 2020 at 14:14):

see https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/ocamldebug.20slow.20on.20ocaml.204.2E11.3F


Last updated: Oct 16 2021 at 07:02 UTC