Stream: VsCoq devs & users

Topic: New default branch


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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"?

view this post on Zulip Maxime Dénès (Feb 15 2023 at 21:00):

But ok, I understand better, you meant the installation instructions

view this post on Zulip Karl Palmskog (Feb 15 2023 at 21:01):

it's also the critical parts about "interpret to point".

view this post on Zulip 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

view this post on Zulip 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")

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Feb 15 2023 at 21:15):

navigating GitHub may not be much easier, though ;)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Maxime Dénès (Feb 17 2023 at 10:04):

Yes, it seems some accidents do happen :)

view this post on Zulip 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"

view this post on Zulip Maxime Dénès (Feb 17 2023 at 10:05):

Probably I should also enable protection bypass by admins

view this post on Zulip Maxime Dénès (Feb 17 2023 at 10:06):

Enabled, we'll see if it works better.

view this post on Zulip 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:

view this post on Zulip Maxime Dénès (Feb 17 2023 at 10:12):

No worries, it happens.

view this post on Zulip 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)

view this post on Zulip Maxime Dénès (Feb 23 2023 at 11:51):

only once we can build against Coq's master

view this post on Zulip Maxime Dénès (Feb 23 2023 at 11:52):

I have one more PR to open after the two you merged recently ;)

view this post on Zulip Maxime Dénès (Feb 23 2023 at 11:53):

but yes, that's the goal indeed


Last updated: Mar 28 2024 at 19:02 UTC