uninstall: always yes

[liyishuai]

in case after_script installed some dependants

[erikmd]

Thanks @liyishuai, LGTM… but the PR is incomplete → you should also update:

docker-coq-action/README.md

Line 83 in 44a09e0

opam remove coq-proj

docker-coq-action/README.md

Line 307 in 44a09e0

opam remove $PACKAGE

docker-coq-action/README.md

Line 338 in 44a09e0

the string `opam remove $PACKAGE`).

Then, I'll do a release.

[erikmd]

And even if some changes are very small like these, I prefer that the PRs are merged by the maintainers (@Zimmi48 @erikmd), as it is the standard practice in coq-community (?)

[Zimmi48]

And even if some changes are very small like these, I prefer that the PRs are merged by the maintainers (@Zimmi48 @erikmd), as it is the standard practice in coq-community (?)

Some repositories are more lax than others. We could set up branch protection rules here. WDYT?

[erikmd]

I thought every master branch of every coq-community project was protected like this, so it appears this is not the case;
so yes, I will configure this now. [Edit: done]

[Zimmi48]

Maybe we should document somewhere (manifesto FAQ?) what the default is and what the options are? cc @palmskog

[palmskog]

My view: branch protection is definitely something that maintainers can decide about, and we should probably set it up for all "critical" projects, such as this and the other Docker projects (and maybe use it for all Coq Platform projects as well?).

But good to document this, and also best practices regarding merging PRs.

[erikmd]

@palmskog Yes;

FTR, here is the screenshot of the settings currently applied for coq-community/docker-coq-action's master branch:

[palmskog]

@erikmd do you really have to add people explicitly under "People, teams or apps with push access"? I thought we could have the convention that everyone that is supposed to have push access is either an Admin or a Coq-community member with the Maintain role [for the repo in question].

[Zimmi48]

It's actually useless to repeat people here since the list already includes all organization or repository admins.

It is also not useful to check "Restrict pushes that create matching branches" for a pattern which is the branch name of an already existing branch. This is more useful when you want to prevent any other branch, or any new release branch from being created on the repository, like we do in Coq. Here this would be useful for instance if you transformed the v1 rule into v[0-9].* or something like this (I don't recall the exact syntax).

Anyway, this highlights even more the need to document this.

[erikmd]

@palmskog @Zimmi48 thanks for your comments, yes I was already aware that the crossed checkboxes of the config I shared were sub-optimal, but it didn't induce any bug… admittedly, if we want to document a standard, cross-organization configuration, we should better have a polished one.
Anyway while we are on it, I refactored the config of docker-coq-action accordingly, and replaced v1 with v* (doc1),(doc2)

Regarding the checkbox Require signed commits, it looked important to me for docker-coq-action, but I wouldn't put it forth for other coq-community projects at first sight.