Paolo Giarrusso (Dec 15 2020 at 14:32): Paolo Giarrusso (Dec 15 2020 at 14:32):Can I vote for giving commit rights to more people, e.g. @Fabian Kunze ? I understand @Maxime Dénès is otherwise busy, but expanding commit bits might make sense anyway
Paolo Giarrusso (Dec 15 2020 at 14:33):and VsCoq is in coq-community which has a process for that
Michael Soegtrop (Dec 15 2020 at 15:44):That might be a good idea. On CUDW some people said that VSCoq works quite well meanwhile, but you have to use branch X of VSCoq expert Y. it would be good to have a proper release soon. Some background info: as you might know Apple now sells MacBooks with ARM CPU. OCaml and Coq works fine there (I did some first tests), but I have little hope to get CoqIDE compiled before the first students hit a university Coq course with a brand new M1 Mac found under the Christmas tree.
Gaëtan Gilbert (Dec 15 2020 at 15:47):wasn't there some emulation layer?
Théo Zimmermann (Dec 15 2020 at 17:47):Technically speaking, @Fabian Kunze does already have commit rights because he's a coq-community member and the master branch of VsCoq is not protected. However, it would be better to get an explicit go ahead from @Maxime Dénès so that Fabian knows he can merge his own PRs / others' PRs. This can be done with or without making Fabian an official co-maintainer.
Fabian Kunze (Dec 15 2020 at 17:48):the problem is not only the access to the git, but I'm not sure how to publish the extension on the vscode-marketplace: I might need permission/ a token/something from Maxime.
Théo Zimmermann (Dec 15 2020 at 17:49):That's correct. This is something that worries me BTW, because in some extreme situation were Maxime would become completely unavailable for a long time, we would have no solution but to "fork" the extension again on the marketplace (even if we wouldn't lose control of the repo).
Fabian Kunze (Dec 15 2020 at 17:52):i skimmed the documentation and it seems that this process is dependent on "Azure DevOps", and accounts/organisations from there are the ones allowed to publish. Isn't part of CI also organized on azure? So isn't there a central coq-azure account?
Fabian Kunze (Dec 15 2020 at 17:53):(see https://code.visualstudio.com/api/working-with-extensions/publishing-extension#publishing-extensions and https://code.visualstudio.com/api/working-with-extensions/continuous-integration )
Fabian Kunze (Dec 15 2020 at 17:53):it seems that we could set it up so that github releases automatically become marketplace-releases
Théo Zimmermann (Dec 15 2020 at 17:57):Fabian Kunze said:
it seems that we could set it up so that github releases automatically become marketplace-releases
That would be great!
Théo Zimmermann (Dec 15 2020 at 17:58):Fabian Kunze said:
i skimmed the documentation and it seems that this process is dependent on "Azure DevOps", and accounts/organisations from there are the ones allowed to publish. Isn't part of CI also organized on azure? So isn't there a central coq-azure account?
Yes and no. There is no Coq organization on the Azure side, but we could create a coq-community one. We have recently left the Azure platform for testing the master branch of Coq BTW (in favor of GitHub Actions).
Théo Zimmermann (Dec 15 2020 at 18:00):There seem to be some GitHub Actions for doing VsCode release publication BTW: https://github.com/marketplace?type=actions&query=vscode
Fabian Kunze (Dec 15 2020 at 18:01):yes, see also https://code.visualstudio.com/api/working-with-extensions/continuous-integration#github-actions
Enrico Tassi (Dec 15 2020 at 18:14):IIRC the silly thing is that "vscoq" is called "maximedenes.vscoq" in the market and there was no way to get something less "personal" when @Maxime Dénès forked the project to coq-community. Maybe things changed now.
I'm sure that "authorization tokens" can come from an organizations, but I failed as well in naming my code extensions following the organization name and not my user name :-(
Maxime Dénès (Dec 15 2020 at 18:18):I would be very happy if Fabian becomes a co-maintainer. If not, I'm also very happy to let him merge patches.
Maxime Dénès (Dec 15 2020 at 18:21):IIRC, indeed there was some mess around personal vs group access and namespaces that made me have to pick maximedenes.vscoq. Not sure if the situation improved since then. I would obviously prefer something like coq-community.vscoq, as I don't plan to register the VsCoq trademark or transfer it to a Maxime Denes company ;)
Maxime Dénès (Dec 15 2020 at 18:25):And btw, I'm very sorry for not having found the time to make a VsCoq release, because of my current involment in other projects. I would also be very happy if Fabian prepares a release. I can prioritize any task involving a transfer / addition of privileges required for the release process.
Théo Zimmermann (Dec 15 2020 at 18:26):@Fabian Kunze would you like to be officially listed as a co-maintainer of VsCoq on the coq-community repo?
Fabian Kunze (Dec 15 2020 at 18:26):I would co-maintain, yes
Théo Zimmermann (Dec 15 2020 at 18:26):OK, I'll do the update to the description and add you as an admin.
Maxime Dénès (Dec 15 2020 at 18:27):To be also fully transparent, my involvement in VsCoq should come back to normal at the latest when the public health situation stabilizes, as my other commitments are related to that.
Maxime Dénès (Dec 15 2020 at 18:28):Mentioning it so that users understand that VsCoq is still a very important project to my eyes.
Fabian Kunze (Dec 15 2020 at 18:29):I understand that things are a bit messy right now
Fabian Kunze (Dec 15 2020 at 18:30):I don't currently understand what would be needed for me to publish on the marketplace. Maxime, did you upload there "by hand" before? I think the goal should be to set up https://code.visualstudio.com/api/working-with-extensions/continuous-integration#github-actions such that every release on github just get's a marketplace release, do you agree @Maxime Dénès ?
Maxime Dénès (Dec 15 2020 at 18:32):I agree. Previous uploads were done manually. Unfortunately, I don't recall the exact process. The documentation was not very clear, AFAIR. Let me check if I had some notes on the topic, but I doubt it.
Fabian Kunze (Dec 15 2020 at 18:32):ok, if not I will dig and, if i need a token or something, @-summon you again ;)
Maxime Dénès (Dec 15 2020 at 18:34):Just checked, I don't think I have notes. The thing is that the process itself is very simple, just write the changelog, tag the release, and use the dedicated vsix command.
Maxime Dénès (Dec 15 2020 at 18:34):Complexity is more in the way you authenticate, and stuff like that.
Fabian Kunze (Dec 15 2020 at 18:34):Yes, that is what I assume
Maxime Dénès (Dec 15 2020 at 18:35):But you do it once and forall.
Maxime Dénès (Dec 15 2020 at 18:35):In any case, if you are stuck somewhere in the process, let me know, I'll find a slot somehow.
Maxime Dénès (Dec 15 2020 at 18:37):And thanks again for your work :)
Michael Soegtrop (Dec 16 2020 at 09:02):@Gaëtan Gilbert : yes, there is an emulation layer. The main issue is that neither MacPorts not Homebrew work, so it would be quite hard to even install the Intel shared libraries one would need to run CoqIDE so that they could be emulated. Gut feeling I would say CoqIDE requires between 50 and 100 system packages to run (gtk, gtksourcview, cairo, pango, freetype, ...). Also OCaml and Opam work fine natively so it makes more sense to compile CoqIDE natively but then I need native shared libraries.
Thinking about it: what might work is to create an Intel installer for Mac and install this on a M1 Mac. I will look into that.
Last updated: Sep 30 2023 at 14:01 UTC