The Flocq CI is reliably failing, at least since https://gitlab.com/coq/coq/-/commit/d9f2eebad2572f6cb31f5999b843b67928dbfea4, is that expected?
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.
@Guillaume Melquiond ping
please fix quickly or give us access, as long as this is broken we're not testing vst/compcert/gappa
Honestly, just remove Flocq and Gappa from CI, and use the one embedded in CompCert for CompCert and VST.
https://github.com/coq/coq/issues/15151
I'm not sure how much we want the stuff in the platform to also be in CI
cc @Théo Zimmermann @Michael Soegtrop
coq/ceps#52 (authored by @Enrico Tassi, the person who added Gappa to Coq's CI in the first place) states:
For each project P included in the platform:
- if P has ML code, then it must be tested using the standard configuration. It can also be tested using another configuration.
This means that in principle plugins in the platforms are required to be in Coq's CI.
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:
- You react in a timely manner to discuss / integrate those patches. When seeking your help for preparing such patches, we will accept that it takes longer than when we are just requesting to integrate a simple (and already fully prepared) patch.
Finally, and importantly, the platform charter makes no mention of the requirement of being in Coq's CI, it just says:
- The author(s) or current maintainer(s) of the package shall agree to the inclusion of their package in the Coq Platform. This means that they agree to put reasonable effort into releasing a version of the package compatible with each new Coq release shortly after every Coq release and to maintain some relative stability between each release.
@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?
My conclusion is that there's some inconsistency in our policies at the moment, and they should be clarified...
This piece of info will help decide what to do
the fix s just cherry-pick https://gitlab.inria.fr/flocq/flocq/-/commit/b8652003b5068749c8850ffd38c356f0a60d192d btw
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...
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.
is gappa compatible with flocq master?
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
The same for core packages (e.g mathcomp, stdpp....)
rate of breakage of gappa is 2 overlays (revertcast and removal of global env calls) since the last overlay cleaning (may 31)
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).
Now I recall, we had this discussion before. But if compcert embeds a copy, that copy of flocq3 has to be fixed anyway, no?
IMO the plan was to have both flocq4 and flocq3 in CI until compcerts moves to version 4
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. :-)
so flocq3 can be be a standalone job, or a vendored one... You are suggesting the latter, right?
OK, fine by me, as long as you tell them ;-)
if we're taking over the flocq3 branch maintenance we could clone it to a repo we control and stop making Guillaume work
So yes, I agree we should stop having flocq3 as a CI job (especially with dependencies).
Yes and no, we want to push compcert people to adopt flocq4 (if reasonable)
if we maintain ourselves that fork, we are not pushing them.
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)
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.
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.)
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).
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.
I think compcert works as well on 8.15 as 8.14
Yes, but I meant switches officially, which always happen quite late...
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.
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.)
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...)
and use the vendored flocq for compcert and vst?
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.
And BTW, CompCert authors do not like merging compatibility fixes to their copy of Flocq if they haven't been merged in Flocq first...
that's why having our own flocq3 branch would work better
I see, if @Guillaume Melquiond agrees we can do that, but we should also set ourselves/compcert a timeout.
Because "test of time" is not exactly clear to me ;-)
I mean, it's like any other task, if you have no deadline you procrastinate...
is vst using flocq through compcert? I forgot how this stuff works
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.
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...
Gaëtan Gilbert said:
is vst using flocq through compcert? I forgot how this stuff works
Yes
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.
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.
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.
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:
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
A quite heavy-handed solution is to actually version library names
so you really have flocq3 and flocq4
but I dunno, specially when you compose builds things can get really tricky if you hit a diamond
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.
@Michael Soegtrop IIUC you avoid diamonds by actually requiring a canonical flocq, right?
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.
I guess Flocq4 would have to be put in Flocq4
in the Coq land.
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
Yes, module aliases would help. Without it I would have to patch the sources via some opam hacks.
module A := B
works (mostly), the problem is Require
vs the filesystem :-|
Last updated: Oct 13 2024 at 01:02 UTC