Michael Soegtrop (Sep 29 2021 at 09:42): Michael Soegtrop (Sep 29 2021 at 09:42):The picking for 2021.09 8.13 is from my point of view finished. Despite the fact that the final amount of information is just a few 100 bytes, it was quite a bit of work to get everything aligned. There are some final changes for 8.13 in (https://github.com/coq/platform/pull/146) currently in CI.
The next step is to do the 8.14+beta pick based on the 8.13 pick - I will do this quickly and include what works. I will name it +beta and not +rc1 because from a Coq Platform point of view it is not a release candidate. The release for 8.14 will happen in November and be a separate release (as discussed for Snap it doesn't work in another way).
If I have time I will also add a 8.11 and 8.10 pick (should be trivial).
Besides that there will be a 8.15 based pick with @Jim Fehrle `s Ltac debugger preview, but only with very few packages otherwise. I think about including just VST and its dependencies because it is an excellent playground for an Ltac debugger, but other suggestions are welcome. Since it is 8.15 based, it is a bit of work to include other stuff.
I will switch the default branch to "main" after doing the 8.14+beta pick and some rework of the readme files.
Comment welcome, including feedback on the process.
Karl Palmskog (Sep 29 2021 at 09:59):I wasn't too thrilled about the wording in some issues. "X requested inclusion" can easily be read as "X demands you to make changes to your project".
There seems to be no give/get breakdown for being in the platform, i.e., here are the benefits for your project, and to get this you have to do A, B, C...
The charter answers some of this in the abstract, between the lines. But I think there needs to be a marketing-level bullet point breakdown.
Théo Zimmermann (Sep 29 2021 at 10:30):The next step is to do the 8.14+beta pick based on the 8.13 pick - I will do this quickly and include what works. I will name it +beta and not +rc1 because from a Coq Platform point of view it is not a release candidate. The release for 8.14 will happen in November and be a separate release (as discussed for Snap it doesn't work in another way).
That makes sense. And you could even call the 8.14 pick 2021.11+beta~8.14 then, to indicate that this is a beta pick for the release that will happen in November.
Théo Zimmermann (Sep 29 2021 at 10:31):Besides that there will be a 8.15 based pick with @Jim Fehrle `s Ltac debugger preview, but only with very few packages otherwise. I think about including just VST and its dependencies because it is an excellent playground for an Ltac debugger, but other suggestions are welcome. Since it is 8.15 based, it is a bit of work to include other stuff.
No, the plan was not to make it 8.15 based but 8.14 based. Jim has already prepared a branch rebased on top of v8.14 for the debugger preview. See: https://github.com/coq/coq/pull/14913
Michael Soegtrop (Sep 29 2021 at 10:39):@Théo Zimmermann : thanks for the note regarding the debugger preview - this makes things easier. I will then include the same packages as in 8.14+beta.
Michael Soegtrop (Sep 29 2021 at 10:45):@Karl Palmskog : thanks for the feedback - indeed I found it difficult to find a good compromise between being concise and informative. My assumption was that most people know what the Coq Platform is about.
It would have helped a bit, if you would have talked to the package maintainers yourself at the time of your request - you know the packages better and it might have been easier for you to find some more personal words.
But I guess adding such a large amount of packages en batch is an exception.
And indeed the charter also needs some improvement. Maybe I should put in some personal words similar to the closing post in (https://github.com/math-comp/multinomials/issues/44).
Karl Palmskog (Sep 29 2021 at 10:57):one example is CoqEAL. My main interest was to get CoqEAL itself into the platform, but then we have dependencies that take a lot of discussion like multinomials. Probably not the last time this happens. It's a bit much ask of a proposer of a package inclusion to be an overall shepherder for 4-5 dependencies at once. It has to be a gradual process.
Michael Soegtrop (Sep 29 2021 at 11:49):I hope the number of missing dependencies will be less in the future, but we will see. Also I don't ask to shepherd the process, but I think some initial contact creation would have helped.
Bas Spitters (Sep 29 2021 at 12:39):@Karl Palmskog could you remind me about the issues around multinomials?
Karl Palmskog (Sep 29 2021 at 12:51):see long discussion here that seems to be converged now: https://github.com/coq/platform/issues/25 https://github.com/math-comp/multinomials/issues/44
Enrico Tassi (Sep 29 2021 at 12:51):none, AFAICT: https://github.com/math-comp/multinomials/issues/44#issuecomment-930050859
Michael Soegtrop (Sep 29 2021 at 12:54):@Bas Spitters : the issue was that I was not sure if the authors understand the concept of the Coq Platform and the expected maintenance intervals. There was no reason to assume they don't understand it, but I insist on a written confirmation.
Enrico Tassi (Sep 29 2021 at 13:00):If I can bring 2C from my experience in Debian: packaging without the consent of the author is a good recipe for disaster. On the contrary, once the authors are aware of the benefits they tend to like you (as a packager).
Jim Fehrle (Sep 29 2021 at 19:33):Besides that there will be a 8.15 based pick with @Jim Fehrle `s Ltac debugger preview, but only with very few packages otherwise.
As @Théo Zimmermann already noted, the debugger preview should be on 8.14. Easier for you and a better user experience for those try the preview--they'll have all the same packages in an 8.14+debugger_preview as in 8.14.
Karl Palmskog (Sep 30 2021 at 07:44):my 2C is that I think we should outline in detail a proposal process for the platform, like what Coq-community has:
This should minimize risk of "packaging without consent" and other issues raised above.
Michael Soegtrop (Sep 30 2021 at 08:03):@Karl Palmskog : indeed we should have a proposal guideline and issue template and the links you provided are a good starting point - I am going to steal from it a bit. In general I need to do some documentation rework.
Last updated: Jun 03 2023 at 05:01 UTC