Stream: coq-community devs & users

Topic: flambda-using Docker-Coq images


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

view this post on Zulip Paolo Giarrusso (Jul 07 2020 at 22:28):

Tagging @Emilio Jesús Gallego Arias on this as well.

view this post on Zulip Théo Zimmermann (Jul 08 2020 at 15:57):

That's probably worth opening an issue on the docker-coq repository.

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:29):

There seems to be at least two problems:

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:29):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:30):

the first bug IMHO should be solved asap

view this post on Zulip Paolo Giarrusso (Jul 09 2020 at 13:30):

the first isn't about -native-compiler=yes, but -native-compiler=ondemand

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:30):

I was talking about Coq's configure

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:31):

in this case it only takes yes/no

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:31):

but indeed if you add yes to configure

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:31):

the default for coqc will be ondemand I think

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:31):

need to re-check

view this post on Zulip Paolo Giarrusso (Jul 09 2020 at 13:31):

at least, I guess we both mean "configure without -native-compiler no"

view this post on Zulip Paolo Giarrusso (Jul 09 2020 at 13:31):

rechecking as well

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:32):

yup, there are in total 6 cases as outlined in the issue

view this post on Zulip Paolo Giarrusso (Jul 09 2020 at 13:32):

oh, seems you're right.

view this post on Zulip Paolo Giarrusso (Jul 09 2020 at 13:32):

That's good.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:33):

So indeed, even with configure=yes native=ondemand there should be no slowdown

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:33):

IMHO that's a serious bug

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:33):

unless you call native in your Coq files

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

view this post on Zulip Paolo Giarrusso (Jul 09 2020 at 13:34):

(the issue about docs = https://github.com/coq/coq/issues/12564)

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:37):

For older releases I indeed dunno

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:38):

a workaround is to disable native in _CoqProject right?

view this post on Zulip Paolo Giarrusso (Jul 09 2020 at 13:38):

uh

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:39):

That's a way?

view this post on Zulip Paolo Giarrusso (Jul 09 2020 at 13:39):

sounds very plausible, never thought or tested that

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:39):

I'm not sure we can do a lot on older releases

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:40):

other than compiling them with native=no in configure

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:40):

which will imply

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 13:40):

native=no

view this post on Zulip Paolo Giarrusso (Jul 09 2020 at 13:41):

I'm very fine with that

view this post on Zulip Paolo Giarrusso (Jul 09 2020 at 13:41):

for myself, and was wondering if it's fine for others

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

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

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

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

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

view this post on Zulip Gaëtan Gilbert (Jul 09 2020 at 13:57):

What's the ondemand slowdown issue?

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

view this post on Zulip Paolo Giarrusso (Jul 09 2020 at 13:57):

searching that a second, @Gaëtan Gilbert

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

view this post on Zulip Paolo Giarrusso (Jul 09 2020 at 13:59):

IIUC, the problem is that Require loads native code eagerly even with native-c = ondemand

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

view this post on Zulip Théo Zimmermann (Jul 09 2020 at 14:10):

@Paolo Giarrusso: @silene is not Vincent Siles, he is @Guillaume Melquiond

view this post on Zulip Paolo Giarrusso (Jul 09 2020 at 14:11):

whoops, thanks! and sorry! :-)

view this post on Zulip Paolo Giarrusso (Jul 09 2020 at 14:26):

hmm, maybe opam config set _is_ good enough to get package flags?

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

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

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

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

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

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

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

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

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

view this post on Zulip Erik Martin-Dorel (Jul 25 2020 at 20:16):

@Paolo Giarrusso thanks for the follow-up.

just to recap the plan:

So I have four questions:

  1. Is the recap above OK or am I missing something?
  2. Does it help if I try to prepare one such dummy package coq-native to opam-repository in the upcoming days?
  3. the only potentiel issue with -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?
  4. I had slightly postponed the migration to single-switches for 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?

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

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

view this post on Zulip Paolo Giarrusso (Jul 25 2020 at 20:26):

I otherwise agree on point 3.

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

view this post on Zulip Paolo Giarrusso (Jul 25 2020 at 20:30):

And oh, coq-native's description might want to warn macos users.

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

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

so 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 :)

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

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

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

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

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

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

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

view this post on Zulip Paolo Giarrusso (Jul 26 2020 at 06:15):

FWIW, I'd have kept the version issue somewhat orthogonal, since it has different stateholders.

view this post on Zulip Erik Martin-Dorel (Jul 26 2020 at 16:05):

@Paolo Giarrusso OK so I ended up creating two different issues:


Last updated: Feb 05 2023 at 14:02 UTC