Would a CompCert/VST user be willing to port CompCert over https://github.com/coq/coq/pull/17022 ? Based on experience with the same change on other library-only developments I expect the work to be not particularly challenging: probably just removing proofs of facts now proven by
auto and adding
Require Btauto to the top of the file so the same hints are available on old Coq versions. (The first error is "No such goal"). Due to ten-foot-pole rules around copyright law I am currently unable to contribute to CompCert myself.
our general go-to person for CompCert+VST issues in the Coq ecosystem is @Michael Soegtrop.
Michael, if you don't have time for this one, who might be good to ping?
I think we should first address @Xavier Leroy and/or AbsInt. I don't know what the work split between them is.
but I think there is some tension here in on whose table an overlay for CompCert ends up: to contribute to Coq (FOSS), you might have to write extensive code for the non-free parts of CompCert. Is this a reasonable requirement if the contribution is valuable? We may want to have some guidelines on this somewhere.
@Karl Palmskog : I don't think I can follow you. That's the reason I recommended to address Xavier and/or AbsInt first.
yes, I agree AbsInt/Xavier are good to ask about this. But I'm saying that how Coq currently works (to my knowledge) is that a PR must have overlays to even be considered for merge. Let's theoretically say that a CompCert overlay is highly nontrivial, and the code will not be FOSS. Is this a reasonable constraint Coq devs can put on a contributor to a FOSS project?
if there is some agreement with Xavier/AbsInt on how such PRs are handled, that would probably lead to less moral hazard
I don't understand what kind of agreement you expect. When you submit a pull request to a projet, be it free software or not, you implicitly agree that your code will be distributed under the license of that project. Any other behavior would be insane (e.g., changing the license according to the wish of the last contributor).
the situation can be as follows: someone develops a valuable contribution to Coq, but the PR to Coq requires extensive changes to non-free parts CompCert, which is not generally something a Coq contributor signed up for. If they abandon a PR for this reason, the community loses. If we have some protocol for people to step in and do the CompCert overlay PR in such cases, that seems like a reasonable thing to guard against such losses.
I don't think this has much to do with accepting licenses to contibute under. The hypothetical original contribution was under LGPL-2.1-only.
there may be more projects under even more restrictive licenses that become part of Coq's CI in the future (I don't see license restrictions in https://github.com/coq/coq/blob/master/dev/ci/README-users.md), so good to clarify this kind of thing early.
So, in your scenario, someone submits a PR to Coq with an overlay, but refuses to submit the overlay upstream (e.g., CompCert) because they do not agree with the inclusion of that code in CompCert. I don't see how the community can help in that case. If someone else submits the overlay in place of the original contributor, this is plain copyright infringement of the original contribution. So, that other person should write a new overlay while making sure that they do not plagiarize the original overlay. Do I understand you correctly?
if there is a protocol for this, then the person who steps in to do the CompCert overlay PR code does this with full permission of the Coq PR author.
what the PR author might object to, or may be forbidden to do by contractual agreements (not just in CompCert, but any non-FOSS project) is to do work on the non-free PR.
Sure. But how does that involves Xavior of Absint? Or do you mean that the original author gives permission to Xavier to apply their overlay in their stead? How is that any different from submitting it upstream in the first place?
IIUC the scenario is that the contributor does not write a compcert overlay, not that they don't submit it as a PR
the argument here was that Xavier could himself do the overlay PR (Andres already gave permission for this implicitly), or delegate to someone at AbsInt, or someone else in the community around CompCert/VST.
I think one point is that when someone submits a Coq PR, they may not even know how their PR affects CompCert and what kind of work they need to do on overlays.
So, in the end, this is just a PR authored by several people. There is nothing specific here about CompCert which would need some kind of agreement. Or, perhaps you expect Xavier to agree a priori to write an overlay for any dumb PR submitted to Coq. In that case, I can already tell you what his answer will be: just remove CompCert from Coq's continuous integration.
I was asking for a reasonable human-oriented process or informal, non-binding agreement here: if a PR is generally agreed to be valuable to Coq, and it gets stuck on the overlay phase for these reasons (licensing, contractual issues), we have some nice way to handle that, possibly already flagged up in
@Karl Palmskog : in principle what you say is true, but many CI adjustments done in the course of a PR (not all) are hardly creative work - they are consequential actions. I don't think it is worth discussing this unless there are changes required which are really creative work. I didn't look at the specific PR).
consequential most of the time, sure. But isn't that a reason to be pro-active about it when we have the chance? At least in
I didn't say we should insist that @Xavier Leroy does the overlay for the PR. But before we get active, we should ask him if he wants to do it. If he says he is busy, we can still do it.
fine by me, I also didn't say anywhere anything about insisting that anyone does something.
Question from the peanut gallery: what's an "overlay" here?
Probably the best way to address this is more generally to state that Coq contributors are not expected to write all the required overlays all by themselves when the PR has been approved as worth pursuing and that other Coq maintainers can help, but also that maintainers of external projects can be requested for help as well (and if they are not available, we can consider removing the project if no one else can handle the overlay writing). We do already have such considerations in place (I'm not sure it's actually documented) for projects like fiat-crypto or fiat-parsers, where it can be difficult to fix the code (for purely technical reasons).
Last updated: Oct 04 2023 at 21:01 UTC