Karl Palmskog (Sep 21 2022 at 17:53): Karl Palmskog (Sep 21 2022 at 17:53):what we can do from community side is help out with advertising for interim VsCoq maintainers, but we need advice and thumbs-up from core to do this (in my view). It's also going to be potentially unthankful to be an interim maintainer, since a lot of the old code is potentially on the way out via the roadmap
Karl Palmskog (Sep 21 2022 at 17:58):here is the key piece of background/motivation: https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ide-multiple-barplot.png
Paolo Giarrusso (Sep 21 2022 at 18:09):I recall quite a few existing MRs about highlighting/autocompletion/… etc that probably wouldn’t be replaced at first?
Paolo Giarrusso (Sep 21 2022 at 18:10):At least, that’s been my assumption, but hopefully some scope could be identified
Paolo Giarrusso (Sep 21 2022 at 18:12):Either way, there are enough users of older Coq’s and enough work maturing things that I don’t know how soon this work would be superseded.
Paolo Giarrusso (Sep 21 2022 at 18:14):I’m on mobile and can’t fork a thread here, but I’m going to tag @Ramkumar Ramachandra as another of the contributors there
Ramkumar Ramachandra (Sep 21 2022 at 18:21):Yeah, we’ve been waiting for that item for a long time. It’s safe to say that VSCoq is in low-maintenance mode, not accepting new patches now.
Matthieu Sozeau (Sep 22 2022 at 08:34):I think we need to know, how close is coq-lsp to providing the same functionality as VsCoq?
Karl Palmskog (Sep 22 2022 at 08:36):that's important information, for sure. But also, even if the functionality might be there, how far off is appropriate packaging, how stable is it for everyday use, etc.
Karl Palmskog (Sep 22 2022 at 08:37):I think a lot of users might want to stay on the "old but proven" VsCoq version if there are stability problems.
Matthieu Sozeau (Sep 22 2022 at 08:56):Sure, it's quite likely to be case that we won't completely replace VsCoq in the very short term. I'm happy with asking for volunteers to maintain the current VsCoq in the meantime.
Karl Palmskog (Sep 22 2022 at 09:01):OK, that's great! But, I'd like to get permission on this also from the key players: @Maxime Dénès, @Enrico Tassi, @Emilio Jesús Gallego Arias. We don't want to step on people's toes here, we (or at least I) just want there to be basic VsCoq maintenance: review and merging of bugfixes, documentation improvements, bugfix releases, etc., even in the face of the fact that this code might be obsoleted [in the short to medium term].
Matthieu Sozeau (Sep 22 2022 at 09:21):Yes, I want that too :)
Enrico Tassi (Sep 22 2022 at 11:20):I'm OK to ask for help maintaining what we have for the coming months
Enrico Tassi (Sep 22 2022 at 11:21):The only thing I ask is to make the volunteers aware of the roadmap
Karl Palmskog (Sep 23 2022 at 11:57):@Théo Zimmermann our standard mode of advertising for coq-community maintainers is as issues in the manifesto repo. Given the importance of VsCoq to the ecosystem, are you OK with advertising also via Coq Discourse (and potentially Coq-club)? [Assuming we get thumbs up from remaining key people]
Karl Palmskog (Sep 23 2022 at 11:58):I think 2 volunteer maintainers would be ideal
Théo Zimmermann (Sep 23 2022 at 12:23):Yes. I should say that by studying how Elm-community works, I've noticed that they regularly look for new volunteers on their ecosystem Slack when a maintainer is stepping down and this is pretty efficient, so I'm thinking we should take inspiration from them and do that more often.
Karl Palmskog (Sep 23 2022 at 12:28):potential luxury problem, but as a default in Coq-community, if more people volunteer than what is feasible, I think coq-community owners should make the final call on who gets maintainership
Théo Zimmermann (Sep 23 2022 at 12:31):BTW, I don't think you tagged @Fabian Kunze so far. I think we should also get his go ahead, shouldn't we?
Karl Palmskog (Sep 23 2022 at 12:32):right, yes.
Karl Palmskog (Sep 26 2022 at 12:17):How about something like the following for a tentative announcement on interim maintainers:
Announcement: Volunteer interim maintainers needed for VsCoq
The Coq core team and Coq-community are looking for volunteer interim maintainers of the VsCoq project.
VsCoq is an extension of the Visual Studio Code (VS Code) editor to support Coq source files and interaction with Coq. In a recent survey of Coq users, around one third of respondents reported that they use VS Code for Coq.
As described in the public roadmap, VsCoq developers are currently focusing on building a new simplified architecture for VsCoq, which means that the current codebase needs additional maintenance resources.
VsCoq is an open source project under the MIT license developed in the Coq-community organization on GitHub. Volunteer maintainers are expected to implement bugfixes and respond to pull request and issues on GitHub. An important goal is to provide a good transition experience for Coq users relying on VS Code to write Coq code while the new VsCoq architecture is being developed and tested.
Please respond to this GitHub issue with your motivation and summary of relevant experience for becoming an interim maintainer of VsCoq.
Karl Palmskog (Sep 26 2022 at 12:27):I do another ping here of @Maxime Dénès and @Emilio Jesús Gallego Arias to try to build more consensus about an interim maintainer solution for VsCoq according to above.
Enrico Tassi (Sep 26 2022 at 12:33):CC @Fabian Kunze
Karl Palmskog (Sep 26 2022 at 12:35):Fabian was pinged more recently than the others, so I figured the figurative timeout for new ping hadn't come
Enrico Tassi (Sep 26 2022 at 12:36):Oops, the UI tricked me
Fabian Kunze (Sep 26 2022 at 12:38):Hi, Sorry but I don't have any capacities to maintain VsCoq in the near future, I'm happy if others are found who can step in for me.
Maxime Dénès (Sep 26 2022 at 18:03):I don't have a strong opinion. More manpower for maintenance is of course nice. On the other hand, I think the message should probably be a bit more explicit about the fact that the current VsCoq is planned to be thrown away soon (extension code included). So that these contributors don't feel after the fact that they have wasted their time.
Karl Palmskog (Sep 26 2022 at 18:04):sure, I'll include a note about the status of the current code, and this should be part of the whole "interim" concept
Karl Palmskog (Sep 26 2022 at 18:07):For example:
Interim maintainers should be aware that the code implementing the new simplified architecture is planned to replace the current code of VsCoq.
Karl Palmskog (Sep 26 2022 at 18:08):but ping @Paolo Giarrusso who I believe had some insights that some VsCoq parts, not least documentation, could carry over regardless of protocol changes
Karl Palmskog (Sep 26 2022 at 18:12):personally, I think the motivation for interim maintenance is pretty solid even if the new VsCoq comes out Jan 1, 2023. That's at least 3 months where we can reduce bug count, whole paper formalizations get written in this time.
Paolo Giarrusso (Sep 26 2022 at 19:29):I don't think I know better than @Maxime Dénès, but I understand the existing Coq versions won't support the new VsCoq? I also I thought the plan was based on "throw away the XML protocol", and that's not 100% of what the extension does
Maxime Dénès (Sep 26 2022 at 19:31):Yes, keeping around the current VsCoq for older versions of Coq will probably make sense for a while.
Paolo Giarrusso (Sep 26 2022 at 19:34):That also decreases pressure on stabilizing the new version
Théo Zimmermann (Sep 27 2022 at 06:32):LGTM, but I think that we could emphasize even more that the Coq core team is lacking maintenance resources to allocate to the current main branch because of work on the new roadmap (it is not so clear that this is what "which means that the current codebase needs additional maintenance resources" means currently) and that Fabian Kunze, which is already an interim VSCoq maintainer lacks time for this as well.
Karl Palmskog (Sep 27 2022 at 06:55):OK, I'll do another iteration of the announcement text to fix this and what was mentioned above
Karl Palmskog (Sep 27 2022 at 08:07):on the flip side, can we offer credits for interim maintenance as part of the (extended) Coq Team? For example, "Related person(s)" in the Zenodo?
Théo Zimmermann (Sep 27 2022 at 08:11):Sounds reasonable, and also on https://coq.inria.fr/coq-team.html. But we should also do it for maintainers of other editor support packages (PG, Coqtail) and for Fabian then.
Karl Palmskog (Sep 27 2022 at 08:16):New attempt, what do you think?
Announcement: Volunteer interim maintainers needed for VsCoq
The Coq core team and Coq-community are looking for volunteer interim maintainers of the VsCoq project.
VsCoq is an extension of the Visual Studio Code (VS Code) editor to support Coq source files and interaction with Coq. In a recent survey of Coq users, around one third of respondents reported that they use VS Code for Coq.
As described in a public roadmap, VsCoq developers are currently focusing on building a new simplified architecture for VsCoq. This means that there are no longer any resources available for maintaining the current codebase.
VsCoq is an open source project available under the MIT license developed in the Coq-community organization on GitHub. Interim maintainers are expected to implement bugfixes, respond to pull request and issues on GitHub, and release new versions of VsCoq on Visual Studio Marketplace and Open VSX.
An important goal of interim maintenance is to provide a good experience for Coq users relying on VS Code for Coq while the new VsCoq architecture (and support for this architecture in Coq itself) is being developed and tested. However, interim maintainers should be aware that substantial parts of the current codebase are due to be replaced as the roadmap is implemented.
During their tenure, interim maintainers will be considered part of the Coq Team and credited for their work in release notes for Coq, for example on Zenodo.
Please respond to this GitHub issue with your motivation, and summary of relevant experience, for becoming an interim maintainer of VsCoq.
Karl Palmskog (Sep 27 2022 at 09:53):I think I've gathered enough consensus about the general direction, so if @Théo Zimmermann is fine with it, I'll post the announcement as a Coq-community manifesto issue and on the Coq Discourse by tonight (feedback welcome in the meantime)
Théo Zimmermann (Sep 27 2022 at 15:27):As described in a public roadmap
Add link? https://github.com/coq-community/vscoq/wiki/VsCoq-1.0-Roadmap
respond to pull request and issues
-> respond to pull requests and issues (missing s)
Possibly worth mentioning that VsCoq is in Typescript and bridges with Coq's XML protocol (which is going to be bypassed in the 1.0 roadmap)?
Please respond to this GitHub issue with your motivation, and summary of relevant experience, for becoming an interim maintainer of VsCoq.
Maybe add encouragement not to self-censor and specify that the Coq-community managers and the Coq team will decide who to appoint as maintainer(s) and that the other volunteers will still be encouraged to contribute?
Karl Palmskog (Sep 27 2022 at 15:37):OK, full version with links:
Announcement: Volunteer interim maintainers needed for VsCoq
The Coq core team and Coq-community are looking for volunteer interim maintainers of the VsCoq project.
VsCoq is an extension of the Visual Studio Code (VS Code) editor to support Coq source files and interaction with Coq. In a recent survey of Coq users, around one third of respondents reported that they use VS Code for Coq.
As described in the public roadmap, VsCoq developers are currently focusing on building a new simplified architecture for VsCoq. This means that there are no longer any resources available for maintaining the current codebase.
VsCoq is an open source project available under the MIT license and developed in the Coq-community organization on GitHub. VsCoq is written in TypeScript and uses an XML-based protocol to communicate with Coq. Interim maintainers are expected to implement bugfixes, respond to pull requests and issues on GitHub, and release new versions of VsCoq on the Visual Studio Marketplace and Open VSX.
An important goal of interim maintenance is to provide a good experience for Coq users relying on VS Code for Coq while the new VsCoq architecture (and support for this architecture in Coq itself) is being developed and tested. However, interim maintainers should be aware that substantial parts of the current codebase are due to be replaced as the roadmap is implemented.
During their tenure, interim maintainers will be considered part of the Coq Team and credited for their work in release notes for Coq releases, for example on Zenodo.
Please respond to this GitHub issue with your motivation, and summary of relevant experience, for becoming an interim maintainer of VsCoq. The interim maintainer(s) will be selected from the issue responders by the Coq core team and Coq-community owners. Those not selected will still be encouraged to contribute to VsCoq by working with the new maintainer(s).
Karl Palmskog (Sep 27 2022 at 18:51):https://github.com/coq-community/manifesto/issues/140 (also see announcements on Discourse)
Karl Palmskog (Sep 27 2022 at 19:04):Here is suggestion for a tweet:
The Coq Team needs volunteer interim maintainers of the open-source VsCoq extension for using Coq with @code while a new architecture is developed. If you have TypeScript experience, consider responding to the GitHub issue: https://github.com/coq-community/manifesto/issues/140
Karl Palmskog (Sep 28 2022 at 08:23):we didn't set any fixed deadline for the call for volunteers, but we could say informally that we [myself and at least one person from Core such as Théo] discuss maintainer selection in about a week (Oct 5 or so)?
Karl Palmskog (Sep 28 2022 at 19:45):many thanks to the people who already responded to the issue, I admit I was mentally preparing for a long "maintainer-wanted" period...
Maxime Dénès (Sep 28 2022 at 19:50):Impressive indeed!
Last updated: Oct 13 2024 at 01:02 UTC