Paolo Giarrusso (Jul 02 2020 at 17:33): Paolo Giarrusso (Jul 02 2020 at 17:33):Now, shameless plug, not for me but for my last boss: Also, careful engineering works for Iris, a separation logic that is a... relative? competitor? alternative? to VST (but not focused on C)
Simon Hudon (Jul 02 2020 at 17:34):That's true. I don't know how they managed it actually. They're such huge engineering projects spanning a long period of time
Simon Hudon (Jul 02 2020 at 17:34):I'll forgive the plug. Iris does look like an impressive piece of software
Paolo Giarrusso (Jul 02 2020 at 17:34):At least Iris doesn’t have instructions for Coq 8.4. It also didn’t exist back then :-).
Simon Hudon (Jul 02 2020 at 17:35)::)
Paolo Giarrusso (Jul 02 2020 at 17:35):but they clearly invest a lot into making it pretty high quality (tho not as much as math-comp, I’m told and can believe)
Simon Hudon (Jul 02 2020 at 17:37):I think with the size of the Coq community, a standard (@Karl Palmskog mentioned the Coq platform) should go a long way to making each development more usable. A similar idea that I like is the approach that stack has in Haskell, of curating generations of packages. That should make everyone's instructions simpler
Paolo Giarrusso (Jul 02 2020 at 17:37):we had the 1st Iris seminar last year, with IIRC 45 attendees, even before @Ralf Jung (one of the authors) finished his PhD
Karl Palmskog (Jul 02 2020 at 17:37):as yet, there is no release of Iris supporting Coq 8.11.
Paolo Giarrusso (Jul 02 2020 at 17:38):uh really? must be because we don’t use releases
Paolo Giarrusso (Jul 02 2020 at 17:38):(or not really)
Karl Palmskog (Jul 02 2020 at 17:38):Iris 3.2.0 has: "coq" {(= "8.7.2") | (= "8.8.2") | (>= "8.9" & < "8.11~") | (= "dev")}
Paolo Giarrusso (Jul 02 2020 at 17:39):alternatively, each commit is released on their own opam repo, so we’re confused on what “releases” should even be
Karl Palmskog (Jul 02 2020 at 17:39):where = "dev" is likely broken long ago...
Paolo Giarrusso (Jul 02 2020 at 17:40):Right, but "Iris releases" are like Debian stable. From my opam:
depends: [
"coq" { (>= "8.11.2" & < "8.12~") }
"coq-iris" { = "dev.2020-06-29.0.462b056f" }
}
right, the idea of the Coq platform is that all platform packages should be available within a month or so after major Coq release ("generational")
Karl Palmskog (Jul 02 2020 at 17:41):I can tell you that there are practically zero users of the MPI-SWS opam repo outside MPI-SWS and their collaborators
Karl Palmskog (Jul 02 2020 at 17:43):if the aim is for broad/wide userbase for a library, I think there is no alternative to putting regular releases into the released Coq opam repo
Paolo Giarrusso (Jul 02 2020 at 17:44):I'm not an Iris/stdpp maintainer, and this has come up sometimes on https://mattermost.mpi-sws.org/iris/, but it's never been clear what the difference between a release and a snapshot is
Karl Palmskog (Jul 02 2020 at 17:44):I can completely understand that some library maintainers don't want to do regular releases or submit packages to the released repo, but then they, in my opinion, can't seriously claim they want a broad userbase.
Paolo Giarrusso (Jul 02 2020 at 17:45):Can somebody explain what's the _downside_ of using an external opam repo?
Paolo Giarrusso (Jul 02 2020 at 17:46):(beyond opam update taking longer, which is annoying)
Karl Palmskog (Jul 02 2020 at 17:46):it's one more repo that everyone needs to add to all their switches every time
Karl Palmskog (Jul 02 2020 at 17:46):for example, MPI-SWS opam repo is not in Coq Docker images, so CI won't work unless you manually configure it (released repo is preconfigured)
Paolo Giarrusso (Jul 02 2020 at 17:47):hm, we should suggest --all-switches --set-default for opam repo add
Paolo Giarrusso (Jul 02 2020 at 17:47):is that why "> they can't seriously claim they want a broad userbase." ?
Karl Palmskog (Jul 02 2020 at 17:48):I think it's a terrible idea to configure repos in all switches
Karl Palmskog (Jul 02 2020 at 17:49):I mean, we have one repo where we check/organize/advertise packages for stable versions of Coq
Paolo Giarrusso (Jul 02 2020 at 17:49):in any case, for Iris the bigger obstacle is that the "introduction" is a ~100 page paper, but that doesn't apply to stdpp
Karl Palmskog (Jul 02 2020 at 17:49):it is documented nearly everywhere, on Coq website, etc.
Karl Palmskog (Jul 02 2020 at 17:50):any other repo will get magnitudes less exposure to regular Coq users.
Karl Palmskog (Jul 02 2020 at 17:50):again, perfectly fine by me to not be a part of this if one wants to run own infrastructure. But quite clear that everything else will be obscure.
Paolo Giarrusso (Jul 02 2020 at 17:51):I'm not a maintainer, so it's probably more productive to ask Robbert or Ralf
Paolo Giarrusso (Jul 02 2020 at 17:52):But I wonder: do people discover packages from opam list? I've never done that
Karl Palmskog (Jul 02 2020 at 17:52):stdpp works fine for 8.11 in released and seems up to date.
Paolo Giarrusso (Jul 02 2020 at 17:53):And if I end up on https://gitlab.mpi-sws.org/iris/stdpp, that'll give me the option of adding the opam repo
Paolo Giarrusso (Jul 02 2020 at 17:55):In any case, @Karl Palmskog, I wonder if _I_ have said something wrong to irk you (and I'm happy to apologize) or you've seen misleading claims somewhere
Paolo Giarrusso (Jul 02 2020 at 17:55):was it my plug?
Karl Palmskog (Jul 02 2020 at 17:57):well, if I came across as irked I apologize. I just think the community suffers from not having all library releases in a single place.
Karl Palmskog (Jul 02 2020 at 18:01):specifically, if there indeed is an investment from the developers in making a library high quality, I think it shouldn't be such a big step of doing some extra release management (once per major Coq version) to let the community yield the benefits more easily.
Simon Hudon (Jul 02 2020 at 18:04):This seems like a constructive resolution for a potential conflict. We recently had a pretty bitter conflict in the Lean community and I was reminded how powerful tact and emotional maturity can really be and how painful their absence can be
Karl Palmskog (Jul 02 2020 at 18:07):I don't want to single out Iris or its authors either. Unfortunately, there are quite many big and serious Coq projects that are near-impossible to find commits for that build with a certain stable Coq version. This mean that most kinds of research and reuse of those libraries is severely limited.
Paolo Giarrusso (Jul 02 2020 at 18:09):Ah! Okay, I can easily understand somebody being annoyed about that problem, and why even Iris's status is a problem
Karl Palmskog (Jul 02 2020 at 18:11):If you think I should bring this up [w.r.t. Iris] with Robbert and Ralf I can do that. There was no wilful intention to go so far on this tangent (and I've broken out the topic from the original one to avoid disturbing the original issue)
Paolo Giarrusso (Jul 02 2020 at 18:12):I mentioned the lack of a release in our Mattermost, and they're aware of it and plan to get to it after POPL.
Paolo Giarrusso (Jul 02 2020 at 18:12):For the general release practice, I guess you'll have to talk to them.
Paolo Giarrusso (Jul 02 2020 at 18:14):In particular, in every discussion about Iris releases, nobody is entirely sure what "release" should mean, and there's a couple of other technical questions they want to get to.
Karl Palmskog (Jul 02 2020 at 18:16):for us opam repo maintainers, a release is anything from a git repo tag to a curated "package", basically as long as it builds on a stable Coq version and makes sense it's all good (but it has to be a tarball/zip living somewhere)
Paolo Giarrusso (Jul 02 2020 at 18:18):the confusion for us is that most/all commits pass that criterion, so we need to find additional ones
Paolo Giarrusso (Jul 02 2020 at 18:18):I think in the Iris case, getting started is daunting mostly because of the maths (tho I'm an extreme case) — and if you get to https://iris-project.org/ or https://gitlab.mpi-sws.org/iris/iris _I think_ you're mostly set, except that you'll have to learn to use opam.
Paolo Giarrusso (Jul 02 2020 at 18:18):Well, opam and everything that Iris uses but Software Foundations doesn't explain
Paolo Giarrusso (Jul 02 2020 at 18:20):And quite a few users _have_ asked for more frequent releases, mostly because they want something "stable" to migrate to — I think that's an actual concern
Paolo Giarrusso (Jul 02 2020 at 18:22):And I totally get your complaint and annoyance at most projects being borderline-bitrotted, and why Iris could have seemed to be there
Karl Palmskog (Jul 02 2020 at 18:22):Paolo G. Giarrusso said:
And I totally get your complaint and annoyance at most projects being borderline-bitrotted, and why Iris could have seemed to be there
Thanks. Sorry again for my "tone" in the exchange above.
Paolo Giarrusso (Jul 02 2020 at 18:23):No worries, I just sensed there was a misunderstanding :-)
Paolo Giarrusso (Jul 02 2020 at 18:23):All is good :-)
Karl Palmskog (Jul 02 2020 at 18:24):I remember back in 2008-2010, the standard was that research papers came with Coq artifacts that only built with a certain commit in master, and then the artifact was never ported to any stable release at all. Thankfully we have come quite far since then.
Paolo Giarrusso (Jul 02 2020 at 18:26):Look, the bare minimum is to know which commit or release to use, and I've run into repos failing _that_ test — that wasn't fun.
Paolo Giarrusso (Jul 02 2020 at 18:27):Many papers won't be kept up-to-date, but at least we're moving towards reproducible artifacts. Which reminds me, I should get back to packaging mine :-)
Tej Chajed (Jul 02 2020 at 19:10):my sense from following the Iris discussion was that it wasn't considered high priority to release on opam because as you said, Iris collaborators just use the MPI-SWS repo
Tej Chajed (Jul 02 2020 at 19:11):@Karl Palmskog I think your opinion is helpful in pushing for using Coq's opam repo, to make it easier for newcomers to install and add a dependency on Iris
Tej Chajed (Jul 02 2020 at 19:14):on a technical level I think it's just a matter of automating the release a bit more on the Iris side - the code is pretty much always ready to be released (CI passes, there's a CHANGELOG, reverse dependencies are even up-to-date)
Karl Palmskog (Jul 02 2020 at 19:16):@Tej Chajed thanks for chiming in. Indeed, one could probably set up machinery to auto-open a pull request in the Coq opam repo when a button or timeout triggers, and just increment the last release minor number by one.
Karl Palmskog (Jul 02 2020 at 19:18):what I would prefer not to happen is that Coq Platform maintainers choose their own commit (of Iris or similar library) for inclusion in the platform revision for Coq 8.XY. Then we suddenly have two parallel release processes.
Théo Zimmermann (Jul 02 2020 at 19:27):Being in the released repo on opam will likely be a requirement for being in the platform and only released versions will be used.
Paolo Giarrusso (Jul 02 2020 at 20:22):Once the platform is there, being in it sounds like an excellent reason, especially if e.g. the platform also comes with Windows installers (I recall one user attempted to use Iris on Windows, I don't think he found a pretty way to do it).
Karl Palmskog (Jul 02 2020 at 20:25):right now, the Windows installer in effect is the platform (or at least, the installer is the closest current approximation to the platform)
Karl Palmskog (Jul 02 2020 at 20:26):Michael has been doing tireless work to select commits for various projects for the installer, many props to him for that (I know how hard it is)
Michael Soegtrop (Jul 04 2020 at 10:40):Btw.: I plan to do the major work of the platform this week (essentially I start now). The first step is to move the Windows build to opam, the second step is to provide an OSX installer. On Linux the plan at first is to provide a shell script which checks prerequisites and compiles from sources. After that we can add packages and then release the first Coq platform.
Karl Palmskog (Jul 04 2020 at 10:43):I can definitely see a plausible future where some project provides immense value to the Coq community, but its developers are not willing/able to put any effort into entering the Coq Platform. In this case, it may be justified to do friendly forks.
Michael Soegtrop (Jul 04 2020 at 10:46):My plan for this is to have levels of the platform. Say level 0 is core Coq, level 1 is "the" platform and level 2 is an extended platform where the time between coq core release and platform release is larger, say 6 months. This would still be better than having 2020 tutorials mentioning Coq 8.9. The higher levels could also include "friendly forks" - for the level 1 platform I would try to avoid this.
Michael Soegtrop (Jul 04 2020 at 10:56):I think such a hierarchical setup might also simplify the work of keeping packages up to date. I would think quite a few people are reluctant to update to latest Coq, because it is so much work to update the required infrastructure, in case this is large. If the majority of the infrastructure is provided by the platform, this should help. But this obviosuly means that we need to have a layered platform architecture, where the basic platform is a pre-requisite for the extended platform. But I have that 3 layers, including Core Coq, will be sufficient.
Théo Zimmermann (Jul 05 2020 at 08:32):I disagree with the idea of doing friendly forks: this would mean more work. Iris is already in Coq's CI (same thing for CompCert). This means that it gets support from Coq developers. But this also mean that we can decide to add new requirements for the Iris / CompCert developers in exchange.
Ralf Jung (Jul 05 2020 at 11:15):Karl Palmskog said:
I can tell you that there are practically zero users of the MPI-SWS opam repo outside MPI-SWS and their collaborators
people that want to use iris add that repository -- so far we didn't get any complaints about that. it's not hard to do, much easier than learning opam in the first place.
someone mentioned yesterday that this makes it hard to use in a Coq CI docker image, but that's it. and for anything opam-based I would argue that it should have support for adding more repos. we use opam for internal dependency management, so certainly for our own CI support for custom repos is absolutely mandatory. we don't want to have to publish a new iris version on the official repo just so that some other internal project can use it.^^ And I expect this situation would come up any time when people are working not just on a single project, but on a small ecosystem of interdependent projects.
(of course the even better option would be if opam would be less limited. in Rust, I can just depend on a git hash in a given external repo. the MPI-SWS repo exists solely as a work-around for opam's limited dependency treatment.)
the opam repo is not how people discover iris/std++, and I don't think it would be useful for that. thus I think "nobody has that repo added" is no problem at all, on its own.
Ralf Jung (Jul 05 2020 at 11:16):Karl Palmskog said:
any other repo will get magnitudes less exposure to regular Coq users.
so you are suggesting that people will actually find coq packages through those repos? that is very surprising to me. I certainly never found anything that way...
my expectation is that people learn about iris or std++ somehow, and then figure out how to install it, at which point I hope our docs are clear enough.
Ralf Jung (Jul 05 2020 at 11:20):so yeah, others have explained well why we are not spending much time to work on releases -- basically every commit we push builds with the last 2-3 stable coq versions, the current beta, and master.
Ralf Jung (Jul 05 2020 at 11:21):but I understand some people prefer to point to a particular commit instead of picking whatever is currently HEAD
Ralf Jung (Jul 05 2020 at 11:21):and I agree we should strive to have an opam package for latest stable coq
Ralf Jung (Jul 05 2020 at 11:23):so we agreed on a new iris release policy :megaphone: : after a stable coq release (or already after the beta, maybe), we will take current master and make a new opam package ASAP.
typically the things that make this hard (the reason it gets delayed) is updating our LaTeX docs to match the Coq changes, finalizing the changelog (making sure really everything is in there), finalizing the sed script that helps people update. if then the release happens <4 weeks before an important deadline (such as Coq 8.12 beta and the POPL deadline), that can also delay releases.
Ralf Jung (Jul 05 2020 at 11:24):many of these are things that others could help with, it doesnt have to be the maintainers doing all that work :)
Ralf Jung (Jul 05 2020 at 11:25):if we manage to follow that release schedule, what else would it take to make iris part of the "Coq platform", and what would that even mean?
Ralf Jung (Jul 05 2020 at 11:25):@Karl Palmskog @Michael Soegtrop ^
Ralf Jung (Jul 05 2020 at 11:27):hm, thinking about the beta... if we now make a release (we hope to do that right after the popl deadline), can we claim that it works with Coq 8.12 after testing with the beta? in principle things could still break before 8.12.0 really gets out.
Ralf Jung (Jul 05 2020 at 11:28):(an iris release for 8.11 was delayed mostly because everyone was just too busy to do the things I mentioned above, and without much demand for proper releases and without a clear schedule, then of course nothing happens. I hope by having a release policy, this will not happen again.)
Karl Palmskog (Jul 05 2020 at 11:48):@Ralf Jung if you follow this new release policy, I have no complaints.
Under the old policy and no versioned releases for 8.11, it was an impossibility to add a package to the released Coq opam archive that depended on Iris and Coq 8.11, since our CI would reject it. This would have meant the Iris ecosystem would have been completely one-way: Iris users could use any Coq package, but nobody who wanted to depend a result/definition from Iris users could have their project be part of the Coq opam archive. I see discoverability as a much less important issue than this.
Ralf Jung (Jul 05 2020 at 11:55):fair, I had not considered packages depending on iris that would themselves want to be on the repo. I do not think we have experience with that (typically things depending on iris are leavess in the dependency tree), and it might be hard (e.g. importing iris together with other things frequently runs into notation conflicts, as coq's notation mechanism is inherently unmodular). but it is certainly something we should facilitate :)
Ralf Jung (Jul 05 2020 at 11:57):I think the only non-leaf iris reverse dependency I am aware of is GPFSL. Not sure if Hai wants to package that at some point, but he certainly shouldn't be blocked on us if he wants to.
Karl Palmskog (Jul 05 2020 at 11:57):what about the distributed systems framework from Aarhus?
Ralf Jung (Jul 05 2020 at 11:57):I am not aware of that being itself a dependency of something
Ralf Jung (Jul 05 2020 at 11:58):nor do I think the authors expressed interest in packaging it
Karl Palmskog (Jul 05 2020 at 11:58):well, a framework is meant to be used, no? Clearly, it will likely be a leaf forever unless there is some packaging
Ralf Jung (Jul 05 2020 at 11:58):but that (what I said above) is besides the point, I do agree that for packaging iris reverse dep.s, releases are crucial
Ralf Jung (Jul 05 2020 at 11:59):do you have an opinion on whether a release that we make in mid-july, tested against the 8.12 beta, can declare compatibility with 8.12?
Karl Palmskog (Jul 05 2020 at 12:00):I'm personally fine with this, but the CI won't accept it if it's only compatible with 8.12 (until after release of 8.12.0). Setting, e.g., >= 8.10 & < 8.13 will work
Karl Palmskog (Jul 05 2020 at 12:04):Ralf Jung said:
nor do I think the authors expressed interest in packaging it
For the record, many packages in the Coq opam archive are actually submitted by others than the developers (and in some cases, without the developers being aware).
Ralf Jung (Jul 05 2020 at 12:13):oh it will support 8.10 and 8.11 as well
Ralf Jung (Jul 05 2020 at 12:13):Karl Palmskog said:
Ralf Jung said:
nor do I think the authors expressed interest in packaging it
For the record, many packages in the Coq opam archive are actually submitted by others than the developers (and in some cases, without the developers being aware).
interesting. for iris I would be somewhat irritated by that, TBH.^^
Michael Soegtrop (Jul 05 2020 at 12:13):Ralf Jung said:
if we manage to follow that release schedule, what else would it take to make iris part of the "Coq platform", and what would that even mean?
See (https://github.com/MSoegtropIMC/coq-platform/blob/master/charter.md) for the basic idea of the Coq platform - which I would say is pretty much agreed on among the past and present Coq release managers - possibly with a few changes here and there. So if IRIS becomes part of the platform, the platform takes care that there is a reliable, fast and fool proof way to install Coq including IRIS on Windows, OSX and - maybe a bit less fool proof - Linux. This should make it easier for teachers and interested explorers to install IRIS. On the other hand you agree to do your best to deliver a working release of IRIS for any major Coq release (like 8.12, 8.13) within at most 3 months, better 1 month.
Currently the way to request to become part of the platform is to make an issue on my private repo I linked above (currently this is the place of the Coq platform - likely this changes after the first release).
Ralf Jung (Jul 05 2020 at 12:14):(FWIW, it's Iris, not IRIS. There is no acronym here. ;)
Ralf Jung (Jul 05 2020 at 12:15):thanks @Michael Soegtrop, that sounds useful! I will discuss with the other Iris maintainers.
Michael Soegtrop (Jul 05 2020 at 12:15):Ralf Jung said:
(FWIW, it's Iris, not IRIS. There is no acronym here. ;)
Thanks, good to know - not that I misspell it in the Windows installer!
Michael Soegtrop (Jul 05 2020 at 12:25):that sounds useful! I will discuss with the other Iris maintainers.
I am looking forward to it. I expect to nail down the list end of July, so it would be good to have your decision by then. It will likely take me until then to finish all the infrastructure anyway.
Ralf Jung (Jul 05 2020 at 13:54):sounds good
Ralf Jung (Jul 15 2020 at 16:22):@Michael Soegtrop we have a new Iris release, and we are happy to join the Coq platform with that. :)
Last updated: Oct 03 2023 at 20:01 UTC