Maxime Dénès (Feb 15 2023 at 16:24): Maxime Dénès (Feb 15 2023 at 16:24):Hi there! As discussed during our weekly meeting, I'm going to rename the master branch to vscoq1 and make a new main branch the default, with the VsCoq 2 code.
Maxime Dénès (Feb 15 2023 at 17:47):Ok, I got something wrong. I'll force push main in the next hour. Sorry for the inconvenience.
Karl Palmskog (Feb 15 2023 at 20:27):from the Coq-community view, I think it would be appropriate to list the union of the VsCoq1 and VsCoq2 maintainers as maintainers in the repo description ("About" on GitHub). Then, it would be nice if the default README.md could list both maintainer teams (separately).
Karl Palmskog (Feb 15 2023 at 20:29):the motivation is that we tend to view the README for the default branch as a landing page for the project in general.
Karl Palmskog (Feb 15 2023 at 20:30):I also think most people will be interested in VsCoq1 for the moment, so it would be nice if there is a clearer recommendation for regular users to go to the VsCoq1 branch.
Enrico Tassi (Feb 15 2023 at 20:44):I agree, maybe a sentence saying this is the readme for the dev version and a link to the stable branch would be enough tough
Enrico Tassi (Feb 15 2023 at 20:44):like a warning upfront, so that the two readmes can stay kind of the same, and not have the union in the main branch
Karl Palmskog (Feb 15 2023 at 20:45):yes, there is a link right now to VsCoq1 branch, but it doesn't say that this is recommended for most users [at least currently]
Maxime Dénès (Feb 15 2023 at 20:55):I agree about listing all maintainers on the default branch's README (I was discussing it with @Laurent Théry).
Maxime Dénès (Feb 15 2023 at 20:56):I'm not completely sure what you mean by "this" in "this is recommended for most users". For users, what is recommended is the only version that is published on the marketplace. For developers what is recommended is to rather contribute to the new main branch.
Karl Palmskog (Feb 15 2023 at 20:57):what I mean is that people google for VsCoq or "VsCode Coq" and they find this README.md for main branch on GitHub. How do they get to somewhere where there are instructions about VsCoq installation from marketplace?
Karl Palmskog (Feb 15 2023 at 20:58):personally, I find the extension installation experience in VS Code terrible so I reuse those instructions every time
Maxime Dénès (Feb 15 2023 at 21:00):I may be naive, but isn't it a matter of clicking on "extensions", then looking for vscoq and clicking "install"?
Maxime Dénès (Feb 15 2023 at 21:00):But ok, I understand better, you meant the installation instructions
Karl Palmskog (Feb 15 2023 at 21:01):it's also the critical parts about "interpret to point".
Karl Palmskog (Feb 15 2023 at 21:03):for some reason, VS Code devs think some Tetris symbol is a good way to represent extensions and consequently there is no "Extensions" text in any drop-down menu, anywhere
Karl Palmskog (Feb 15 2023 at 21:04):someone said elsewhere that they also installed some other Coq extension than the maximedenes one (this is easy to do if you search for "coq")
Karl Palmskog (Feb 15 2023 at 21:08):this one has 8100 installs and was last updated in 2016 (sigh): https://marketplace.visualstudio.com/items?itemName=ruoz.coq
Maxime Dénès (Feb 15 2023 at 21:15):navigating GitHub may not be much easier, though ;)
Maxime Dénès (Feb 15 2023 at 21:15):but point taken, I'll try to make the sentence pointing to the VsCoq 1 branch more explicit
Karl Palmskog (Feb 15 2023 at 21:17):you could link people directly to https://github.com/coq-community/vscoq/tree/vscoq1#instructions in my opinion
Hjalte Sorgenfrei Mac Dalland (Feb 17 2023 at 09:52):Could we also have the main branch protected from direct pushes so a PR is needed and we always run CI on commits before merging?
Maxime Dénès (Feb 17 2023 at 10:04):Yes, it seems some accidents do happen :)
Maxime Dénès (Feb 17 2023 at 10:05):But it is strange, it seems I had enabled "Require a pull request before merging"
Maxime Dénès (Feb 17 2023 at 10:05):Probably I should also enable protection bypass by admins
Maxime Dénès (Feb 17 2023 at 10:06):Enabled, we'll see if it works better.
Romain Tetley (Feb 17 2023 at 10:09):Sorry for the cheeky push, it was reckless ! I think I won't be doing that again any time soon :face_palm:
Maxime Dénès (Feb 17 2023 at 10:12):No worries, it happens.
Gaëtan Gilbert (Feb 22 2023 at 15:11):should we switch the branch Coq CI tests? (currently document-manager from the maximedenes/vscoq repo)
Maxime Dénès (Feb 23 2023 at 11:51):only once we can build against Coq's master
Maxime Dénès (Feb 23 2023 at 11:52):I have one more PR to open after the two you merged recently ;)
Maxime Dénès (Feb 23 2023 at 11:53):but yes, that's the goal indeed
Last updated: Jun 04 2023 at 23:30 UTC