Andres Erbsen (Feb 07 2023 at 17:07): Andres Erbsen (Feb 07 2023 at 17:07):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.
Karl Palmskog (Feb 07 2023 at 18:38):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?
Michael Soegtrop (Feb 08 2023 at 08:56):I think we should first address @Xavier Leroy and/or AbsInt. I don't know what the work split between them is.
Karl Palmskog (Feb 08 2023 at 09:22):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.
Michael Soegtrop (Feb 08 2023 at 09:25):@Karl Palmskog : I don't think I can follow you. That's the reason I recommended to address Xavier and/or AbsInt first.
Karl Palmskog (Feb 08 2023 at 09:27):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?
Karl Palmskog (Feb 08 2023 at 09:28):if there is some agreement with Xavier/AbsInt on how such PRs are handled, that would probably lead to less moral hazard
Guillaume Melquiond (Feb 08 2023 at 09:48):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).
Karl Palmskog (Feb 08 2023 at 09:53):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.
Karl Palmskog (Feb 08 2023 at 09:55):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.
Karl Palmskog (Feb 08 2023 at 10:01):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.
Guillaume Melquiond (Feb 08 2023 at 10:01):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?
Karl Palmskog (Feb 08 2023 at 10:02):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.
Karl Palmskog (Feb 08 2023 at 10:03):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.
Guillaume Melquiond (Feb 08 2023 at 10:05):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?
Gaëtan Gilbert (Feb 08 2023 at 10:05):IIUC the scenario is that the contributor does not write a compcert overlay, not that they don't submit it as a PR
Karl Palmskog (Feb 08 2023 at 10:06):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.
Karl Palmskog (Feb 08 2023 at 10:08):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.
Guillaume Melquiond (Feb 08 2023 at 10:11):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.
Karl Palmskog (Feb 08 2023 at 10:14):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 ci/README-users.md.
Michael Soegtrop (Feb 08 2023 at 10:27):@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).
Karl Palmskog (Feb 08 2023 at 10:31):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 ci/README-users.md.
Michael Soegtrop (Feb 08 2023 at 11:12):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.
Karl Palmskog (Feb 08 2023 at 12:00):fine by me, I also didn't say anywhere anything about insisting that anyone does something.
Stefan Monnier (Feb 08 2023 at 14:23):Question from the peanut gallery: what's an "overlay" here?
Gaëtan Gilbert (Feb 08 2023 at 14:25):https://github.com/coq/coq/blob/master/dev/ci/user-overlays/README.md
Théo Zimmermann (Feb 08 2023 at 14:50):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: Apr 20 2024 at 15:01 UTC