Enrico Tassi (Feb 05 2021 at 10:17): Enrico Tassi (Feb 05 2021 at 10:17):I just discovered that perennial uses its own fork of iris and stdpp. This makes overlays hard/impossible to write. Didn't we somewhat agree that projects in CI must not embed other projects that happen to be in CI?
Enrico Tassi (Feb 05 2021 at 10:18):(not to talk about the fact that it recompiles stdpp and iris...)
Jason Gross (Feb 05 2021 at 12:17):Tangential: Note that fiat-crypto also does this (but changing this fact is as simple as adding EXTERNAL_BEDROCK2=1 to https://github.com/coq/coq/blob/9485db5e16edeaf408f73758f2e7f9531dc7d3e0/dev/ci/ci-fiat_crypto.sh#L17 (Or, well, it used to be, except now fiat-crypto depends on bedrock2 via rubicola, and rubicola is not on Coq's CI (though perhaps it should be, so passing EXTERNAL_BEDROCK2=1 may complain about not being able to find rubicola).) The reason we do this is that bedrock2 is unstable enough that fiat-crypto is not guaranteed to be compatible with the tip of bedrock2, and we only update the submodule every so often.
Théo Zimmermann (Feb 05 2021 at 13:24):No, we never forbade using submodule to get dependencies and we have a lot of projects that do it like this. Are you specifically asking about the "fork" aspect?
Enrico Tassi (Feb 07 2021 at 16:58):Well, I guess it's easier to discuss live at the coq call. But I'll make a short summary of the problems here:
If you want to develop your software this way (embedding copies of others) it is you choice (and your problem, eventually). But if we get this software in CI "as is", it is getting in our way as I explain above. IMO we should write down what we consider acceptable and what is not.
Théo Zimmermann (Feb 07 2021 at 19:48):Eventually, I would also like to rule out submodule-based dependencies in Coq's CI. But to be realistic, we are far from there: there are too many projects that do that currently. And the case of projects that do plain copy-paste vendoring (VST which embeds its copy of CompCert) or of projects that implement a custom pinning method (Iris and cie) are not better for us.
Théo Zimmermann (Feb 07 2021 at 19:51):I suggest you have a look at Section 3.6.3.2 of my PhD thesis (https://www.irif.fr/_media/users/theo/memoirthesis.pdf), in particular what follows "Another crucial point that is still absent from our inclusion policy, but will have to be addressed in the future, is the way projects can manage their dependencies". Even if it is about 1 year and a half old, it still contains a rather correct picture of what we have today.
Enrico Tassi (Feb 08 2021 at 09:25):IMO real dependencies should be on released versions (you can vendor them to simplify things). Then you can relax this pinning to .dev version for the sake of testing (via makefile/configuration and/or .dev packages). Pinning/vendoring an unreleased commit/custom fork is another story. It's not very different technically, but it defeats any hope to do sensible porting work only once.
I think pinning random commit/branches during development is inevitable, but exposing this to others (e.g. us) is not something you want. I did advocate for having coq-master (in addition to master) so that you have a choice at what to expose to our CI.
E.g. I'm currently adding a feature to HB, which requires a feature to coq-elpi, which required a fix in elpi. So my dev setup here is a mess, but I don't push that setup to coq-master.
Especially for .v projects it is irrelevant if Coq tests a 2 months old version of my .v stuff. We are testing millions of LOC, my output in 2 months is not going to change the statistics and fixing myself the code in the delta is not going to be a huge task. Sometimes, e.g. for .ml code, it may make sense to expose my code to Coq CI asap, having a dedicated branch for them gives me some flexibility.
To wrap up my thoughts, I think we should let our users develop as they like, even if they do it in non orthodox ways. But I don't see why we need to be exposed to that complexity.
(tiny note, I think you dropped a 0 for coq-elpi count of LOC. It has never been 700 lines, I'd love that to be true)
Enrico Tassi (Feb 08 2021 at 09:30):BTW, the VST/Compcert/Floq/MenhirLib thing is sort of fixed now.
Théo Zimmermann (Feb 10 2021 at 16:11):@Enrico Tassi This is the main document: https://github.com/coq/coq/blob/master/dev/ci/README-users.md
Enrico Tassi (Feb 10 2021 at 16:21):I think you identified the core of the issue at the call, we should test/fix released versions for most projects. This has good side effects:
Théo Zimmermann (Feb 10 2021 at 16:38):Yes, though testing "released" versions would actually mean a released branch containing the last release + compatibility updates.
Emilio Jesús Gallego Arias (Feb 11 2021 at 00:03):I'm not sure our policy should be such as to influcence / interfere with the cycle developers do chose to work with; for example I would not enjoy a lot if Coq would force me to do releases; IMHO it is better to have a set of abstract requirements and let developers implement them as they see fit
Emilio Jesús Gallego Arias (Feb 11 2021 at 00:05):The latency problem is still quite worrying, as the cost to reconcile may be high, but yeah we can try that way, and see where it does lead to us; one advantage of the current model tho is its simplicity and very low latency
Emilio Jesús Gallego Arias (Feb 11 2021 at 00:06):Actually, I'm personally happy with how things have worked out, and while it is true we have found some cases where the current model was hard to work with, the tradeoff of having to systematically reconcile patches with all devs in CI vs having to deal with some vendoring not very often is not yet clear to me
Paolo Giarrusso (Feb 11 2021 at 13:46):if you have a use-case for Iris having releases at all, I’m sure they’d be happy to hear it.
Paolo Giarrusso (Feb 11 2021 at 13:47):almost each master commit is good and useful for users, at best they’d only need a way to mark some of them as bad.
Paolo Giarrusso (Feb 11 2021 at 13:50):you should tag Tej but AFAIK they don’t have “local fixes they’re not pushing upstream”, they have a real tracking fork.
Enrico Tassi (Feb 11 2021 at 13:58):real tracking fork.
If you want to pin a commit, you don't need a fork. They do have a fork in perennial, why? @Tej Chajed
each master commit is good and useful for users
Are they always backward compatible? If it was the case, why one would need to pin a commit in the first place?
@Paolo Giarrusso are we seriously questioning what is the point of making releases in software development?
Tej Chajed (Feb 11 2021 at 14:58):We have a fork of Iris that changes some internals (which for technical reasons are not user extensible, unlike most of Iris); prior to this change the git submodule directly pointed to the https://gitlab.mpi-sws.org/iris/iris repo. Perennial does have a submodule with std++.
Enrico Tassi (Feb 11 2021 at 15:03):This confirms my findings. When we will merge https://github.com/coq/coq/pull/13448 you will have to do some work on your side, since the overlay makes .gitmodules point to our fork, which is not something you want to merge
Tej Chajed (Feb 11 2021 at 15:03):That said, we stay extremely up-to-date with upstream Iris and std++. The effect is that if you make an overlay for std++ which is up-to-date with std++ master, Perennial can almost certainly use it. Similarly with Iris, although we have to incorporate it by merging with our fork. I have a CI run every night that attempts to upgrade everything to the latest release so I'm always aware if we have an incompatibility and I tend to fix things within 24h. If all of this infrastructure ever breaks down for the Coq devs I'm also a real person (not a cat) that you can ask to do something and I'm happy to help.
Enrico Tassi (Feb 11 2021 at 15:04):This is the commit we are testing, but I guess you don't want to merge it: https://github.com/ybertot/perennial/commit/bcac0b9aafe5d71456203e1244475835a0994da4
Enrico Tassi (Feb 11 2021 at 15:09):It is maybe not clear from this chat, but I find it totally normal that you do this kind of git gimmicks in your master branch. I do it as well. What I'm suggesting is that we should not track your master branch in our CI, but one which is less of a moving target. This will let you update things when you have the time and will let us test/overlay something which is not that complex.
I'll try to explain this better in the documentation, right now we've just discussed the status quo, pros, cons, etc at the last Coq call. (it is not specific to perennial, to be clear).
Enrico Tassi (Feb 11 2021 at 15:14):If your project makes releases, then this branch is likely to be the last release + our overlay/fixes, and shall not pin a commit of a project in CI, but just use what is there. For this to work, your changes to other projects in CI should be pushed upstream, at some point (again, if we track another branch, you have all the time you want to do it).
Théo Zimmermann (Feb 11 2021 at 15:33):Note that we already test a dedicated branch for perennial.
Enrico Tassi (Feb 11 2021 at 15:40):It is true, but it coincides with master. So I guess the use they make of it is not the one I have in mind.
Tej Chajed (Feb 11 2021 at 15:46):coq/tested is basically the latest commit on master where our CI succeeds, so it's not a great target for overlays (we could separate the two temporarily but it would be a bit of work)
Tej Chajed (Feb 11 2021 at 15:49):Incidentally this overlay for std++ is very simple and I can probably get it merged upstream
Enrico Tassi (Feb 11 2021 at 16:10):IMO the branch should be pushed ahead only once there are no "local" changes to other projects in CI. So that we can use/overlay their CI branch also for perennial (limit the git submodule update --init only to projects we don't already test, if any).
Gaëtan Gilbert (Feb 11 2021 at 16:20):it sounds like there's no plan to upstream the iris change
Enrico Tassi (Feb 11 2021 at 17:27):27 files changed, 3648 insertions(+), 248 deletions(-)
I'm looking at the patch, there are many additions... To the best of my understanding this is the culprit:
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 236c1d02..003ebc4f 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -12,6 +12,7 @@ From iris.prelude Require Import options.
Class heapG Σ := HeapG {
heapG_invG : invG Σ;
+ heapG_crashG : crashG Σ;
heapG_gen_heapG :> gen_heapG loc (option val) Σ;
heapG_inv_heapG :> inv_heapG loc (option val) Σ;
heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ;
Enrico Tassi said:
each master commit is good and useful for users
Are they always backward compatible? If it was the case, why one would need to pin a commit in the first place?
no, every commit can change APIs if justified.
Paolo Giarrusso are we seriously questioning what is the point of making releases in software development?
no no, just saying that (almost) every Iris commit pushed to master has basically all the properties that I as a user want from a release.
Tej Chajed (Feb 12 2021 at 15:34):The std++ overlay is now upstream (https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/228) and Perennial is using it, so no overlay should be needed for that PR.
Tej Chajed (Feb 12 2021 at 15:36):Why were the std++ developers not notified of this issue to begin with? We could've had this fixed at the source a month ago. For future changes this should continue to be the case - eventually std++ and Iris will have to find a backwards-compatible solution, so why not do it as soon as the Coq devs have a change in mind?
Last updated: Dec 07 2023 at 17:01 UTC