Skip to content

Ensure all files have designated maintainers#21549

Open
yannl35133 wants to merge 1 commit intorocq-prover:masterfrom
Yann-Leray:codeowners
Open

Ensure all files have designated maintainers#21549
yannl35133 wants to merge 1 commit intorocq-prover:masterfrom
Yann-Leray:codeowners

Conversation

@yannl35133
Copy link
Contributor

@yannl35133 yannl35133 commented Jan 27, 2026

("All files" doesn't include files that shouldn't have a maintainer)

At the end, I only looked for the team I found most suitable, all changes are suggestions and up to discussion.

Proposed changes in decreasing order of justifications (if not mentioned, they were unassigned):

  • /dev/tools/make_git_revision.sh to @rocq-prover/build-maintainers (that appeared to be the case already, but the later assignment of /dev/tools/ overrode it)
  • /kernel/pConstraints.* and /kernel/qGraph.* transferred from @rocq-prover/kernel-maintainers to @rocq-prover/universes-maintainers
  • /config/ to @rocq-prover/build-maintainers
  • /tools/rocqtex* to @silene (as maintainer of /tools/coq_tex.*)
  • /tools/rocqwc* to @rocq-prover/coqdoc-maintainers (as maintainer of /tools/coqwc*)
  • *.mld to @rocq-prover/doc-maintainers (the commit that added them says they exist for documentation; they might have become useless now)
  • /dev/ml_toplevel/ to @rocq-prover/toplevel-maintainers
  • *.opam from @rocq-prover/build-maintainers and @erikmd to @rocq-prover/build-maintainers and @Just0606
  • *.opam.template to @rocq-prover/build-maintainers and @erikmd as maintainers of *.opam
  • /tools/ to @rocq-prover/dev-tools-maintainers (as fallback if no other assignment applies)
  • /dev/ to @rocq-prover/dev-tools-maintainers (as fallback if no other assignment applies, this should only be files in no subfolder)
  • .gitattributes .gitignore .ocp-indent to @rocq-prover/build-maintainers
  • .mailmap CREDITS LICENSE to @rocq-prover/contributing-process-maintainers

I will wait for one person accepting on behalf of a team to consider all concerned changes accepted, and I will probably remove from the PR all propositions that aren't accepted after some time (or those outright refused), I don't intend to push them hard.

@yannl35133 yannl35133 requested a review from a team as a code owner January 27, 2026 17:45
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jan 27, 2026
@SkySkimmer
Copy link
Contributor

SkySkimmer commented Jan 27, 2026

.gitattributes .gitignore .ocp-indent to @rocq-prover/build-maintainers

that doesn't sound right, maybe dev-tools instead

/.ocamlinit @rocq-prover/build-maintainers
*dune* @rocq-prover/build-maintainers
*.opam @rocq-prover/build-maintainers @erikmd
*.opam.template @rocq-prover/build-maintainers @erikmd
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@erikmd isn't maintaining anymore IIUC

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

if @Zimmi48 agrees, I suggest that you replace erikmd with @Justme0606 here

Copy link
Contributor

@erikmd erikmd Jan 27, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FWIW, this mention in the CODEOWNERS was useful for the docker-rocq maintainer(s) to be aware soonish of build changes in rocq master, so that the docker-rocq config can be updated earlier, and not after a docker-rocq:dev rebuild failure

@SkySkimmer SkySkimmer self-assigned this Feb 4, 2026
@SkySkimmer SkySkimmer added kind: meta About the process of developing Coq. and removed needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Feb 4, 2026
@SkySkimmer SkySkimmer added this to the 9.3+rc1 milestone Feb 4, 2026
@SkySkimmer
Copy link
Contributor

SkySkimmer commented Feb 4, 2026

For the teams they can make a PR later if there's a problem but I'd like an explicit ok before merging for people explicitly named: @silene and @Justme0606

@SkySkimmer
Copy link
Contributor

Also for @Justme0606 I think he would need to be part of the organization to get review requests and AFAICT he isn't.

@Justme0606
Copy link

For the teams they can make a PR later if there's a problem but I'd like an explicit ok before merging for people explicitly named: @silene and @Justme0606

Sure, no problem. I had discussed the continuity of docker-rocq with Erik, so this is fine with me.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

kind: meta About the process of developing Coq.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants