Stream: Coq devs & plugin devs

Topic: Flocq broken on master


view this post on Zulip Pierre-Marie Pédrot (Nov 08 2021 at 13:57):

The Flocq CI is reliably failing, at least since https://gitlab.com/coq/coq/-/commit/d9f2eebad2572f6cb31f5999b843b67928dbfea4, is that expected?

view this post on Zulip Guillaume Melquiond (Nov 08 2021 at 13:59):

Yes, since the CI does not track the development branch of Flocq, I need to backport the fix, which I don't intend to do today.

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 11:28):

@Guillaume Melquiond ping

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 14:06):

please fix quickly or give us access, as long as this is broken we're not testing vst/compcert/gappa

view this post on Zulip Guillaume Melquiond (Nov 09 2021 at 14:10):

Honestly, just remove Flocq and Gappa from CI, and use the one embedded in CompCert for CompCert and VST.

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 14:23):

https://github.com/coq/coq/issues/15151

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 14:27):

I'm not sure how much we want the stuff in the platform to also be in CI
cc @Théo Zimmermann @Michael Soegtrop

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 14:27):

coq/ceps#52 (authored by @Enrico Tassi, the person who added Gappa to Coq's CI in the first place) states:

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 14:28):

For each project P included in the platform:

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 14:29):

This means that in principle plugins in the platforms are required to be in Coq's CI.

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 14:30):

OTOH, Coq's CI documentation considers that the desire to be in Coq's CI should come from the project maintainer and states a few conditions to be kept, including:

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 14:31):

Finally, and importantly, the platform charter makes no mention of the requirement of being in Coq's CI, it just says:

view this post on Zulip Enrico Tassi (Nov 09 2021 at 14:31):

@Guillaume Melquiond I guess you are busy right now. If you are planning to backport the fix, can you estimate how long will it take?

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 14:32):

My conclusion is that there's some inconsistency in our policies at the moment, and they should be clarified...

view this post on Zulip Enrico Tassi (Nov 09 2021 at 14:32):

This piece of info will help decide what to do

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 14:34):

the fix s just cherry-pick https://gitlab.inria.fr/flocq/flocq/-/commit/b8652003b5068749c8850ffd38c356f0a60d192d btw

view this post on Zulip Karl Palmskog (Nov 09 2021 at 14:42):

I was under the impression that the Platform and Coq's CI are nearly completely separate, a project can be in both, none, or one of them. A maintainer of a theoretical plugin in the Platform that is not in Coq's CI is going to have a hard time making a commitment to releases, though...

view this post on Zulip Guillaume Melquiond (Nov 09 2021 at 14:55):

Enrico Tassi said:

If you are planning to backport the fix, can you estimate how long will it take?

I can backport it. But the question is: What good is it for the CI to follow a branch of Flocq that is not the development branch? Both branches have diverged about one year ago and the one being tested by the CI exists purely for the sake of Coq's CI.

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 14:57):

is gappa compatible with flocq master?

view this post on Zulip Enrico Tassi (Nov 09 2021 at 14:59):

Karl Palmskog said:

I was under the impression that the Platform and Coq's CI are nearly completely separate, a project can be in both, none, or one of them. A maintainer of a theoretical plugin in the Platform that is not in Coq's CI is going to have a hard time making a commitment to releases, though...

I want .ml code which is in the platform to also be in Coq's CI, otherwise maintaining the platform amounts at re-discovering these breackages

view this post on Zulip Enrico Tassi (Nov 09 2021 at 14:59):

The same for core packages (e.g mathcomp, stdpp....)

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 15:01):

rate of breakage of gappa is 2 overlays (revertcast and removal of global env calls) since the last overlay cleaning (may 31)

view this post on Zulip Guillaume Melquiond (Nov 09 2021 at 15:01):

Gaëtan Gilbert said:

is gappa compatible with flocq master?

It should be. The breaking changes between both branches target a part that is not used by Gappa (but is used by CompCert and VST).

view this post on Zulip Enrico Tassi (Nov 09 2021 at 15:01):

Now I recall, we had this discussion before. But if compcert embeds a copy, that copy of flocq3 has to be fixed anyway, no?

view this post on Zulip Enrico Tassi (Nov 09 2021 at 15:02):

IMO the plan was to have both flocq4 and flocq3 in CI until compcerts moves to version 4

view this post on Zulip Guillaume Melquiond (Nov 09 2021 at 15:02):

Enrico Tassi said:

Now I recall, we had this discussion before. But if compcert embeds a copy, that copy of flocq3 has to be fixed anyway, no?

Sure, but it means that the work is no longer on me but on CompCert's developers. :-)

view this post on Zulip Enrico Tassi (Nov 09 2021 at 15:02):

so flocq3 can be be a standalone job, or a vendored one... You are suggesting the latter, right?

view this post on Zulip Enrico Tassi (Nov 09 2021 at 15:03):

OK, fine by me, as long as you tell them ;-)

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 15:04):

if we're taking over the flocq3 branch maintenance we could clone it to a repo we control and stop making Guillaume work

view this post on Zulip Enrico Tassi (Nov 09 2021 at 15:04):

So yes, I agree we should stop having flocq3 as a CI job (especially with dependencies).

view this post on Zulip Enrico Tassi (Nov 09 2021 at 15:04):

Yes and no, we want to push compcert people to adopt flocq4 (if reasonable)

view this post on Zulip Enrico Tassi (Nov 09 2021 at 15:05):

if we maintain ourselves that fork, we are not pushing them.

view this post on Zulip Enrico Tassi (Nov 09 2021 at 15:05):

IMO there is a bit of communication to do, and in the short term have compcert use their vendored copy (and post there the overlay PR)

view this post on Zulip Guillaume Melquiond (Nov 09 2021 at 15:06):

You don't have to push them. They will adopt it. But the issue is that Coq's CI lives in a world where changes have to be taken into account instantly (see this discussion as an example), while Flocq and CompCert have a much slower-paced development process.

view this post on Zulip Guillaume Melquiond (Nov 09 2021 at 15:07):

CompCert would never switch to Flocq 4 until Flocq 4 has passed the test of time. (And one week is definitely not what "passing the test of time" means.)

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 15:09):

Just to insist because it doesn't seem that clear in the discussion: the Coq platform can only ship one version of Flocq. For 2021.09 and almost certainly for 2021.11, this version is Flocq 3 (because of CompCert and VST).

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 15:10):

Can CompCert switch to Flocq 4 at the same time as it switches to Coq 8.15? Maybe, but I'm not convinced this will happen.

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 15:11):

I think compcert works as well on 8.15 as 8.14

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 15:11):

Yes, but I meant switches officially, which always happen quite late...

view this post on Zulip Guillaume Melquiond (Nov 09 2021 at 15:11):

Flocq 4 is not compatible with Coq 8.11. So, if CompCert wants to preserve compatibility with 8.11 (?), they will not switch to Flocq 4.

view this post on Zulip Guillaume Melquiond (Nov 09 2021 at 15:13):

Anyway, I have backported the fix to the branch. (But not tested it, so it might still get reverted if it does not pass Flocq's CI.)

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 15:13):

That being said, if Gappa can be compatible with Flocq 3 and 4 at the same time, then it does sound like a good plan to move the Flocq version being tested in Coq's CI to Flocq 4 so that Gappa is kept in check. (Although strictly speaking this wouldn't fully respect what was written in CEP#52, but well...)

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 15:14):

and use the vendored flocq for compcert and vst?

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 15:24):

Yes. The main drawback would be that by going back to the previous situation, we end up having to fix Flocq twice when it breaks.

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 15:24):

And BTW, CompCert authors do not like merging compatibility fixes to their copy of Flocq if they haven't been merged in Flocq first...

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 15:26):

that's why having our own flocq3 branch would work better

view this post on Zulip Enrico Tassi (Nov 09 2021 at 15:32):

I see, if @Guillaume Melquiond agrees we can do that, but we should also set ourselves/compcert a timeout.

view this post on Zulip Enrico Tassi (Nov 09 2021 at 15:32):

Because "test of time" is not exactly clear to me ;-)

view this post on Zulip Enrico Tassi (Nov 09 2021 at 15:34):

I mean, it's like any other task, if you have no deadline you procrastinate...

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 15:35):

is vst using flocq through compcert? I forgot how this stuff works

view this post on Zulip Guillaume Melquiond (Nov 09 2021 at 15:36):

As I said, it is no just a matter of procrastinating. Currently, CompCert supports Coq 8.9. As long as they want to support this version of Coq, they cannot switch to Flocq 4.

view this post on Zulip Enrico Tassi (Nov 09 2021 at 15:38):

OK, but then this is the question. How long do the want to support that? If the answer is "for the next foreseeable future", then we are no good...

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 15:48):

Gaëtan Gilbert said:

is vst using flocq through compcert? I forgot how this stuff works

Yes

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 15:49):

Enrico Tassi said:

OK, but then this is the question. How long do the want to support that? If the answer is "for the next foreseeable future", then we are no good...

I don't think so. They regularly drop compatibility with old Coq versions.

view this post on Zulip Michael Soegtrop (Nov 09 2021 at 16:46):

I agree with @Théo Zimmermann : plugins (ML code) which are in the platform should be in Coq CI - for pure Coq developments it should be sufficient to test them in Coq Platform CI.

Please note that currently I don't run daily tests on dev, but wanted to reeanble this soon.

view this post on Zulip Michael Soegtrop (Nov 09 2021 at 17:04):

A note on the Flocq3 vs. Flocq4 question: technically it would be possible to ship both Flocq3 and Flocq4 by making them separate projects, say by installing Flocq4 into a "Flocq4" folder or Flocq3 into a "Flocq3" folder and patching the dependencies. But this is not desirable because if CompCert and VST use Flocq3 but proof tools like Coq Interval or gappa use Flocq4, one can't use these tools any more to prove properties of C programs. My plan is to switch to Flocq 4 when CompCert switches. In case there emerge some good developments which require Flocq4 or feature updates to say Coq Interval (or Flocq itself) are so nice that people are willing to take measures to get around the compatibility issues (in the end it all boils down to R), I will go the dual Flocq path, but then likely also include Coq Interval & Co for both Flocq 3 and Flocq 4.

For the sake of testing, one could prepare this already in Coq Platform dev. The question is if one should publish corresponding opam packages (flocq3.xyz, flocq4.xyz, coq-interval-flocq3.xyz, coq-interval-flocq4.xyz ...) then. In such a setup the usual opam packages should use the un-amended installation path while the flocq3/flocq4 packages would install into an amended path ad use Flocq from an amended path.

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 17:18):

I agree with @Théo Zimmermann : plugins (ML code) which are in the platform should be in Coq CI - for pure Coq developments it should be sufficient to test them in Coq Platform CI.

I only restated what is documented in CEP#52 :wink:

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2021 at 11:04):

Indeed, very interesting discussion, we have had similar discussion in the context of vendoring OCaml libraries too, it is not yet clear to me what the best model is

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2021 at 11:05):

A quite heavy-handed solution is to actually version library names

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2021 at 11:05):

so you really have flocq3 and flocq4

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2021 at 11:05):

but I dunno, specially when you compose builds things can get really tricky if you hit a diamond

view this post on Zulip Michael Soegtrop (Nov 10 2021 at 11:30):

Emilio Jesús Gallego Arias said:

but I dunno, specially when you compose builds things can get really tricky if you hit a diamond

Yes, that's the reason why I want to avoid it and stick to Flocq3 until CompCert has updated unless there are good arguments for including Flocq4 and .3 and .4 variants of its derivatives.

Since Coq Platform now has variants, it would also be an option to add a Flocq4 variant, which has only those packages which are Flocq4 compatible. So one could have Flocq3 with Compcert in one opam switch and Flocq4 without it in another opam switch.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2021 at 11:31):

@Michael Soegtrop IIUC you avoid diamonds by actually requiring a canonical flocq, right?

view this post on Zulip Michael Soegtrop (Nov 10 2021 at 11:33):

Yes - in Coq Platform everything has a fixed version (it is not pinned but I call opam install with specific versions requested).

But if one supports Flocq3 and Flocq4 in one switch by having different package names, one could still have diamonds.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2021 at 11:44):

I guess Flocq4 would have to be put in Flocq4 in the Coq land.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2021 at 11:45):

We don't have module aliases, which really help to do this kind of stuff so you can do module Floqc = Flocq3 etc... in OCaml

view this post on Zulip Michael Soegtrop (Nov 10 2021 at 11:46):

Yes, module aliases would help. Without it I would have to patch the sources via some opam hacks.

view this post on Zulip Paolo Giarrusso (Nov 10 2021 at 15:31):

module A := B works (mostly), the problem is Require vs the filesystem :-|


Last updated: Feb 01 2023 at 16:03 UTC