Automatic review requests on the lean4 repo

Stream: lean4

[Thomas Murrills]

I noticed that on one recent PR I made (lean4#3654) I automatically “requested a review” on the PR (without deliberately doing anything). However, on another PR (lean4#3698), this didn’t happen.

I’m not sure how code ownership is working here, but I just thought I ought to report the inconsistency in case it’s unintentional. :)

[Kim Morrison]

Yes, it's just a file not covered by any code owners.

[Thomas Murrills]

Ah, ok. Is every file meant to be covered by some code owner? Is code ownership only for “critical” files? (Just curious.)

[Kim Morrison]

I think the practical effect of code owners is that code owners should consider themselves able to unilaterally merge without consulting anyone else about it.

There are gaps, and often things get merged by a non-code owner, but ideally in those cases there's been some discussion.