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.
Ok, I got something wrong. I'll force push
main in the next hour. Sorry for the inconvenience.
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).
the motivation is that we tend to view the README for the default branch as a landing page for the project in general.
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.
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
like a warning upfront, so that the two readmes can stay kind of the same, and not have the union in the main branch
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]
I agree about listing all maintainers on the default branch's README (I was discussing it with @Laurent Théry).
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.
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?
personally, I find the extension installation experience in VS Code terrible so I reuse those instructions every time
I may be naive, but isn't it a matter of clicking on "extensions", then looking for vscoq and clicking "install"?
But ok, I understand better, you meant the installation instructions
it's also the critical parts about "interpret to point".
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
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")
this one has 8100 installs and was last updated in 2016 (sigh): https://marketplace.visualstudio.com/items?itemName=ruoz.coq
navigating GitHub may not be much easier, though ;)
but point taken, I'll try to make the sentence pointing to the VsCoq 1 branch more explicit
you could link people directly to https://github.com/coq-community/vscoq/tree/vscoq1#instructions in my opinion
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?
Yes, it seems some accidents do happen :)
But it is strange, it seems I had enabled "Require a pull request before merging"
Probably I should also enable protection bypass by admins
Enabled, we'll see if it works better.
Sorry for the cheeky push, it was reckless ! I think I won't be doing that again any time soon :face_palm:
No worries, it happens.
should we switch the branch Coq CI tests? (currently document-manager from the maximedenes/vscoq repo)
only once we can build against Coq's master
I have one more PR to open after the two you merged recently ;)
but yes, that's the goal indeed
Last updated: Jun 04 2023 at 23:30 UTC