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).
Tagging @Emilio Jesús Gallego Arias on this as well.
That's probably worth opening an issue on the docker-coq repository.
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.
okay filed https://github.com/coq-community/docker-coq/issues/10 and clarified docs (https://github.com/coq-community/docker-coq/pull/9).
We were discussing a bit flambda+coq on github, and there seem still to be some issues
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?
There seems to be at least two problems:
-native-compiler=yes
slowerMy top-level current understanding is that native-compute is too underspecified to be very confident of anything positive
the first bug IMHO should be solved asap
the first isn't about -native-compiler=yes, but -native-compiler=ondemand
@Paolo Giarrusso indeed, there was some missing documentation but I think we are making progress
I was talking about Coq's configure
in this case it only takes yes/no
but indeed if you add yes to configure
the default for coqc will be ondemand
I think
need to re-check
at least, I guess we both mean "configure without -native-compiler no
"
rechecking as well
yup, there are in total 6 cases as outlined in the issue
oh, seems you're right.
That's good.
So indeed, even with configure=yes
native=ondemand
there should be no slowdown
IMHO that's a serious bug
unless you call native
in your Coq files
right, and that should be fixed in future releases, but I'm also interested in past releases
(the issue about docs = https://github.com/coq/coq/issues/12564)
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 :-)
For older releases I indeed dunno
a workaround is to disable native in _CoqProject
right?
uh
so you're saying that -native-compiler no
in CoqProject (encoded with -arg
maybe) would avoid this altogether?
That's a way?
sounds very plausible, never thought or tested that
I'm not sure we can do a lot on older releases
other than compiling them with native=no in configure
which will imply
native=no
I'm very fine with that
for myself, and was wondering if it's fine for others
but IIUC from silene (@Vincent Siles ?), it's hard to use native_compute reliably with opam packages, simply because of integration issues
and if that's correct, we should bite the bullet and disable it by default on opam.
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.
and that seems useful anyway and more useful if flambda, since it seems to worsen the native-comp bug
problem is that there are some users already, so you would leave them in the cold
What's the ondemand slowdown issue?
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
searching that a second, @Gaëtan Gilbert
It's https://github.com/coq/coq/issues/11107 — I updated the title recently with my latest understanding there
IIUC, the problem is that Require
loads native code eagerly even with native-c = ondemand
by +native
variants, I mean 8.11.0+native
(or maybe 8.11.0+nonative
). But that has problems...
@Paolo Giarrusso: @silene is not Vincent Siles, he is @Guillaume Melquiond
whoops, thanks! and sorry! :-)
hmm, maybe opam config set
_is_ good enough to get package flags?
That is, if we could make the behavior of opam packages conditional, we might be able to solve the problem.
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.
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:
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.
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.
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).
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.
I’d default to ‘no-native’ and add a coq-native dummy, but hopefully choosing the default is easy.
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.
@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?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).
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.
I otherwise agree on point 3.
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.
And oh, coq-native's description might want to warn macos users.
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 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 :)
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.
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?
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 !)
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?
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.
@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_version
field 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 :)
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.)
FWIW, I'd have kept the version issue somewhat orthogonal, since it has different stateholders.
@Paolo Giarrusso OK so I ended up creating two different issues:
Last updated: Sep 25 2023 at 12:01 UTC