Paolo Giarrusso (Jul 07 2020 at 21:58): Paolo Giarrusso (Jul 07 2020 at 21:58):Hi @Erik Martin-Dorel, thanks again for your Coq images! I wanted to use 8.11-ocaml-4.09-flambda, but I'm not sure it actually enables flambda — it just uses the flambda version of ocaml, but doesn't pass the flambda flags to Coq, because it runs opam install coq and that _doesn't_ enable flambda yet. The same applies to images using 4.07.1-flambda.
_Maybe_ this can be fixed by something like https://github.com/ocaml/opam-repository/pull/16779
Otherwise, we'll need one of the workarounds in https://coq.discourse.group/t/install-notes-on-coq-and-ocaml-versions-configuration/713.
I've built my own opam overlay fixing this (example), but you're not supposed to depend on (EDIT) my overlay: I haven't committed to maintaining it for public use, nor documented its quirks (tags in version numbers are a really poor encoding of flags).
Paolo Giarrusso (Jul 07 2020 at 22:28):Tagging @Emilio Jesús Gallego Arias on this as well.
Théo Zimmermann (Jul 08 2020 at 15:57):That's probably worth opening an issue on the docker-coq repository.
Paolo Giarrusso (Jul 08 2020 at 21:12):Ah. I didn’t find a tracker on https://gitlab.com/coq-community/docker-coq. But now I checked again, and it’s on https://github.com/coq-community/docker-coq/issues.
Paolo Giarrusso (Jul 08 2020 at 21:23):okay filed https://github.com/coq-community/docker-coq/issues/10 and clarified docs (https://github.com/coq-community/docker-coq/pull/9).
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:28):We were discussing a bit flambda+coq on github, and there seem still to be some issues
Paolo Giarrusso (Jul 09 2020 at 13:28):Indeeed! You wrote on GitHub:
We are gonna see what we do with that problem, if you are not using native in your lib, the slowdown shouldn't happen.
I'm not sure I'm getting all the details right tho, so maybe we can chat on Zulip a bit more interactively?
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:29):There seems to be at least two problems:
-native-compiler=yesslower Emilio Jesús Gallego Arias (Jul 09 2020 at 13:29): Paolo Giarrusso (Jul 09 2020 at 13:30):My top-level current understanding is that native-compute is too underspecified to be very confident of anything positive
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:30):the first bug IMHO should be solved asap
Paolo Giarrusso (Jul 09 2020 at 13:30):the first isn't about -native-compiler=yes, but -native-compiler=ondemand
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:30):@Paolo Giarrusso indeed, there was some missing documentation but I think we are making progress
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:30):I was talking about Coq's configure
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:31):in this case it only takes yes/no
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:31):but indeed if you add yes to configure
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:31):the default for coqc will be ondemand I think
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:31):need to re-check
Paolo Giarrusso (Jul 09 2020 at 13:31):at least, I guess we both mean "configure without -native-compiler no"
Paolo Giarrusso (Jul 09 2020 at 13:31):rechecking as well
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:32):yup, there are in total 6 cases as outlined in the issue
Paolo Giarrusso (Jul 09 2020 at 13:32):oh, seems you're right.
Paolo Giarrusso (Jul 09 2020 at 13:32):That's good.
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:33):So indeed, even with configure=yes native=ondemand there should be no slowdown
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:33):IMHO that's a serious bug
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:33):unless you call native in your Coq files
Paolo Giarrusso (Jul 09 2020 at 13:34):right, and that should be fixed in future releases, but I'm also interested in past releases
Paolo Giarrusso (Jul 09 2020 at 13:34):(the issue about docs = https://github.com/coq/coq/issues/12564)
Paolo Giarrusso (Jul 09 2020 at 13:36):And to be sure, personally, I confess to having unreasonable standards — you're moving there in the right way, and I know there's tons to do :-)
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:37):For older releases I indeed dunno
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:38):a workaround is to disable native in _CoqProject right?
Paolo Giarrusso (Jul 09 2020 at 13:38):uh
Paolo Giarrusso (Jul 09 2020 at 13:39):so you're saying that -native-compiler no in CoqProject (encoded with -arg maybe) would avoid this altogether?
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:39):That's a way?
Paolo Giarrusso (Jul 09 2020 at 13:39):sounds very plausible, never thought or tested that
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:39):I'm not sure we can do a lot on older releases
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:40):other than compiling them with native=no in configure
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:40):which will imply
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:40):native=no
Paolo Giarrusso (Jul 09 2020 at 13:41):I'm very fine with that
Paolo Giarrusso (Jul 09 2020 at 13:41):for myself, and was wondering if it's fine for others
Paolo Giarrusso (Jul 09 2020 at 13:42):but IIUC from silene (@Vincent Siles ?), it's hard to use native_compute reliably with opam packages, simply because of integration issues
Paolo Giarrusso (Jul 09 2020 at 13:44):and if that's correct, we should bite the bullet and disable it by default on opam.
Paolo Giarrusso (Jul 09 2020 at 13:45):if we go ahead, if you do use it, and compile and install all your libraries without opam, then you'll now have to compile and install coq without opam as well.
Paolo Giarrusso (Jul 09 2020 at 13:46):and that seems useful anyway and more useful if flambda, since it seems to worsen the native-comp bug
Emilio Jesús Gallego Arias (Jul 09 2020 at 13:52):problem is that there are some users already, so you would leave them in the cold
Gaëtan Gilbert (Jul 09 2020 at 13:57):What's the ondemand slowdown issue?
Paolo Giarrusso (Jul 09 2020 at 13:57):yeah that's the question — since you say there are, we could leave configure -native yes, or try adding +native or -native variants of the coq package
Paolo Giarrusso (Jul 09 2020 at 13:57):searching that a second, @Gaëtan Gilbert
Paolo Giarrusso (Jul 09 2020 at 13:58):It's https://github.com/coq/coq/issues/11107 — I updated the title recently with my latest understanding there
Paolo Giarrusso (Jul 09 2020 at 13:59):IIUC, the problem is that Require loads native code eagerly even with native-c = ondemand
Paolo Giarrusso (Jul 09 2020 at 14:05):by +native variants, I mean 8.11.0+native (or maybe 8.11.0+nonative). But that has problems...
Théo Zimmermann (Jul 09 2020 at 14:10):@Paolo Giarrusso: @silene is not Vincent Siles, he is @Guillaume Melquiond
Paolo Giarrusso (Jul 09 2020 at 14:11):whoops, thanks! and sorry! :-)
Paolo Giarrusso (Jul 09 2020 at 14:26):hmm, maybe opam config set _is_ good enough to get package flags?
Paolo Giarrusso (Jul 09 2020 at 21:58):That is, if we could make the behavior of opam packages conditional, we might be able to solve the problem.
Paolo Giarrusso (Jul 09 2020 at 21:59):I'm not sure that variables have the same behavior as "package flags" — I don't think Coq would be recompiled if you changed a variable. But it might be better than nothing.
Erik Martin-Dorel (Jul 09 2020 at 22:28):I'm unsure to precisely know the contexts where native_compute is slow with flambda enabled (is this especially reproducible on macos?)
anyway I share the concerns raised by @Guillaume Melquiond in https://github.com/coq/coq/issues/12564#issuecomment-647546401 :
to avoid the runtime overhead he mentions, Coq's stdlib (and compiled Coq libraries) should ideally generate .coq-native/* files by default when installing a standard opam package.
and if need be, one could provide a way to users to easily disable this, e.g. by installing a dummy opam package coq-nonative? which would trigger something like this in the opam recipe:
…
"-native-compiler" {coq-nonative:installed} "no" {coq-nonative:installed}
…
but this is only a very rough idea/suggestion…
I also Cc @Pierre Roux as he has taken a closer look than me on native_compute recently.
FYI Pierre, here are some GitHub issues/PRs related to this zulip thread:
while you were aware of these older issues/PRs:
Paolo Giarrusso (Jul 10 2020 at 06:56):Somewhere else on Zulip, @Emilio Jesús Gallego Arias discussed indeed how to address @Guillaume Melquiond's concern with separate -native packages, but that would require small additional Coq features; IIRC he planned to summarize that on GitHub.
Paolo Giarrusso (Jul 10 2020 at 07:01):On the bugs: if you create .coq-native files for library foo, loading foo will load the .coq-native files eagerly. That's measurable on Linux and has larger effects on Mac, sometimes absurdly so.
Paolo Giarrusso (Jul 10 2020 at 07:10):The issues are https://github.com/coq/coq/issues/11178 and https://github.com/coq/coq/issues/11107. I edited titles/OP for some clarity (GitHub has edit histories, so I felt more comfortable doing that).
Paolo Giarrusso (Jul 10 2020 at 07:21):Encoding “package flags” in opam might be a way forward. Opam has both configuration variables and dummy opam packages, but the latter might work better — there’s a proposal for that in https://github.com/ocaml/opam-repository/pull/16753.
Paolo Giarrusso (Jul 10 2020 at 07:22):I’d default to ‘no-native’ and add a coq-native dummy, but hopefully choosing the default is easy.
Paolo Giarrusso (Jul 25 2020 at 10:02):FWIW: been swamped; I closed https://github.com/ocaml/opam-repository/pull/16779 for now, no promises on when/if I might try this again. At least we have a plan, tho it's locked up here in a lengthy discussion.
Erik Martin-Dorel (Jul 25 2020 at 20:16):@Paolo Giarrusso thanks for the follow-up.
just to recap the plan:
-native-compiler flag, we would disable it by default for all Coq supporting native_compute, except if the new dummy package coq-native is installed beforehand (and ideally, installing this package after Coq should rebuild Coq itself!)-flambda-opts flags, we would pass them to configure for all Coq >= 8.7 if OCaml >= 4.07, doing something like "-flambda-opts" {ocaml:version >= "4.07"} "-O3 -unbox-closures" {ocaml:version >= "4.07"} (as the -flambda-opts would just amount to no-op with a no-flambda compiler)So I have four questions:
coq-native to opam-repository in the upcoming days?-flambda-opts would then occur in a +flambda switch, if coq-native is also installed. I guess it is unnecessary to "automatically disable flambda if coq-native is installed" (so combining the two options would be "at the discretion/risk of the user"), but on the other hand I propose to refactor afterwards the Docker-Coq images so that coq-native is always installed in the 4.05.0 switch, but coq-native is not installed in 4.07.1+flambda / 4.09.1+flambda. Do you agree?coqorg/coq images because of this +flambda issue, but given that move will take a bit more time, maybe I could just as well finalize that migration soon? (basically to have ASAP the gain of shortening the size and download time of coqorg/coq:*-ocaml-{4.07,4.09}-flambda images… albeit flambda would not be fully leveraged at first). WDYT? Paolo Giarrusso (Jul 25 2020 at 20:23):That sounds good, a couple of points: I'm confused about the 4.09 images for orthogonal reasons (IIUC that OCaml is worse for Coq, from what @Emilio Jesús Gallego Arias says, and my more limited testing agreed). I agree on not doing anything special for the coq-native + flambda combo (apart from maybe a comment in coq-native's description).
Paolo Giarrusso (Jul 25 2020 at 20:25):I'm also not sure on using 4.05; I guess there are good reasons and I'm happy to not learn that (maybe document it for the others who have a clue, if appropriate). Should it be 4.07.1 without flambda and with coq-native? Probably not.
Paolo Giarrusso (Jul 25 2020 at 20:26):I otherwise agree on point 3.
Paolo Giarrusso (Jul 25 2020 at 20:29):point 4 sounds fine to me; shrinking image size might even be more important. BTW, I think I tagged you on my issue about opam clean; not sure how relevant that is for your images, but it might matter.
Paolo Giarrusso (Jul 25 2020 at 20:30):And oh, coq-native's description might want to warn macos users.
Paolo Giarrusso (Jul 25 2020 at 20:35):I think that's it; I'd post that to an issue somewhere sensible, and allow volunteers to help. I might be able to help myself, but I shouldn't block things (I'm busier with the new job etc.). Submitting coq-native sounds good. I'm not sure how easy it is to automatically rebuild coq on installing it, but even without that feature, this seems be a massive improvement.
Erik Martin-Dorel (Jul 25 2020 at 20:45):OK thanks!
BTW can you just elaborate on your remark below? I'm not sure I fully got your idea:
I'm also not sure on using 4.05; I guess there are good reasons and I'm happy to not learn that (maybe document it for the others who have a clue, if appropriate). Should it be 4.07.1 without flambda and with coq-native? Probably not.
Actually providing three different versions of OCaml in coqorg/coq was just a compromise to have:
coqorg/coq:8.11-ocaml-4.10-flambda as well for example!) → without native_compiler as wellso if we want to have coq-native installed in at least one flavor of the images, there is not many possibilities, hence my proposal to add it later on in 4.05.0 :)
Erik Martin-Dorel (Jul 25 2020 at 20:46):Paolo Giarrusso said:
I think that's it; I'd post that to an issue somewhere sensible, and allow volunteers to help. I might be able to help myself, but I shouldn't block things (I'm busier with the new job etc.). Submitting coq-native sounds good. I'm not sure how easy it is to automatically rebuild coq on installing it, but even without that feature, this seems be a massive improvement.
OK good idea, to open an issue to track the progress on this move.
But I guess I'll first look after the move to single-switches in docker-coq.
Karl Palmskog (Jul 25 2020 at 21:26):Ocaml 4.05.0 is now more than 3 years old and to me a terrible release compared to 4.07.1. Will we ever get rid of it? From conversation here, it seems it will be around for several years more?
Erik Martin-Dorel (Jul 25 2020 at 21:38):Sure, it may be possible to put forward 4.07.1+flambda as the default ocaml version within docker-coq… (say, when flambda support will be fully enabled :)
Also, maybe at some point the Coq team will decide to not support 4.05.0 anymore;
but for the moment anyway, we should probably not remove these images, as 4.05.0 is by definition the minimal version of ocaml that can be used for each Coq ≥ 8.7… (and there is also ocaml 4.02.3 for yet older Coq versions !)
Paolo Giarrusso (Jul 25 2020 at 22:20):What's the goal of using "the minimal working version of OCaml (4.05.0)"? That still seems a means to an end, but which?
Paolo Giarrusso (Jul 25 2020 at 22:22):my only guess is "some users have plugins that break on newer OCaml" — I know of plugins that don't support 4.10.0 yet.
Erik Martin-Dorel (Jul 25 2020 at 23:05):@Paolo Giarrusso yes, from a Coq perspective (if a given project does not have any plugin code) I agree this is not especially useful to stick to 4.05.0; being able to readily use not-yet-ported OCaml plugins was one of the main ideas indeed. (And maybe the fact that when doing benchmarks to gauge the impact of a change on a development involving plugin-based tactics, we might want to test two different OCaml versions; just to gauge the compiler influence… but having, say, more than 3 OCaml versions in docker-coq would be overkill indeed!)
BTW note that the current semantics of the ocaml_versionfield of docker-coq-action provides three values: minimal, 4.07-flambda, 4.09-flambda;
I don't know what's @Théo Zimmermann's opinion but I'm unsure it would be very convenient to "drop" minimal (at least for the backward compatibility of the projects' CI that use that value minimal).
However as I mentioned in my previous comment, I'd rather propose to just promote 4.07-flambda as the default version soon: this would thus be in line with Emilio's Discourse post about recommending OCaml 4.07.1+flambda… while keeping one or two more OCaml versions, for users who really wants a more recent (or not!) version :)
Erik Martin-Dorel (Jul 25 2020 at 23:10):Anyway this question regarding the default ocaml versions / variants to put forth is an excellent question indeed, and I don't claim that having three ocaml versions is the definite solution!
let's say we discuss this again and further in the issue I'll open in github as you suggested @Paolo Giarrusso (to deal with the new coq-native package etc.)
Paolo Giarrusso (Jul 26 2020 at 06:15):FWIW, I'd have kept the version issue somewhat orthogonal, since it has different stateholders.
Erik Martin-Dorel (Jul 26 2020 at 16:05):@Paolo Giarrusso OK so I ended up creating two different issues:
Last updated: Jun 06 2023 at 23:01 UTC