coq
SSProve
We'd like to add https://github.com/SSProve/ssprove to platform. Is there anything we'd need to do?
@spitters : the first step would be to discuss with the authors if they plan to long term maintain this project and if they want it to be included in the Coq Platform in agreement with the charter. It would help if you could initiate and conduct this discussion here. It definitely looks like a very interesting development, but with only two journal publication related tags it is unclear to me what the long term prospect is.
Also I couldn't find an opam package, which makes dependency analysis and initial tests difficult.
Yes, we plan to maintain it for the long term. @haselwarter , @TheoWinterhalter and myself will be likely maintainers. Will create an opam package.
@spitters : did you create the opam package as discussed? I somehow still can't find it. If the opam package is there by Wednesday I can still consider it for the 2022.03 release, otherwise I need t postpone it.
@MSoegtropIMC we have an opam file at https://github.com/SSProve/ssprove/blob/main/ssprove.opam , is that what you had in mind?
@haselwarter No, the opam file should be submitted to the opam-coq-archive (for specific releases).
@haselwarter : a description field in opam would be nice - we generate the readme from it. It can have a few lines (some have a few 10 lines). Please note that you can unfold the package sections by clicking on the tiangles.
@spitters @haselwarter : I would need the tag and the published opam package by tomorrow evening for inclusion in Coq Platform 2022.03.
@spitters @haselwarter : I wanted to ask what the status of the opam packages is. I can delay the release a few days, say until Tuesday next week (that is packages are there on Monday) if you say a few days would help.
It's probably better to not rush things and maybe aim for a later release of the platform. So no need for you to wait for us. Thanks.
Thanks! If you need any help preparing this, please let me know.
FYI: the next official release will be in about 5..6 months, 4..8 weeks after the 8.16.0 release (see https://coq.discourse.group/t/coq-8-16-release-schedule/1598). There will be an 8.16 preview releases short after the 8.16.0 release - that is July or early August) where I would also include it.
@TheoWinterhalter : I started to prepare the next release (2022.09). The first preview will happen soon.
As far as I can tell there is still no opam package in the Coq Opam repo.
It should be there latest in 4 weeks.
Sorry for this, we have been busy with other things so I don't think we will be ready either for the next release.
Thanks for checking with us!
Nothing comes to mind, but we are going to update our dependencies soon so we probably should wait for this. I hope this doesn't create too much workload overhead for you to wait on us like this.
Fine with me. For the 2022.09 release there is still some time - mid of August would be good but I can also live with end of August. Beyond that it starts to produce substantial extra work, so I might postpone it then.
Since there was no progress and the 2022.09 beta is due I delayed this to 2023.03.
@TheoWinterhalter : if you have something by tomorrow, I might reconsider.
Hi, I think this issue is adding unnecessary workload for you, it might be best to close it and reopen it when we are ready to propose something. Unless @spitters or @haselwarter disagree?
I am fine to leave it open to not forget it - the traffic will be about 2...3 pings per release of Coq Platform (6 months).
Let's leave it open then, at least until we evaluate how to merge our work
on Jasmin back into main, upstream compatibility permitting.
On Wed, 14 Sept 2022 at 09:34, MSoegtropIMC @.***> wrote:
I am fine to leave it open to not forget it - the traffic will be about 2...3 pings per release of Coq Platform (6 months).
— Reply to this email directly, view it on GitHub https://github.com/coq/platform/issues/177#issuecomment-1246363683, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAGO4GROXX3MZ55RFRVTAS3V6F5ZBANCNFSM5IGZDYHA . You are receiving this because you were mentioned.Message ID: @.***>