Gaëtan Gilbert (Jun 01 2023 at 10:34): Gaëtan Gilbert (Jun 01 2023 at 10:34):Currently if there is a nontrivial issue in CI knowing who to ask is folklore. Maybe we should change the CI policy to require that it be documented, and document it for the already there projects?
I think it would work to put the info in basic-overlay, looking like
########################################################################
# Lean Importer (cc Gaëtan Gilbert @SkySkimmer)
########################################################################
project lean_importer "https://github.com/SkySkimmer/coq-lean-import" "master"
could one use code owners for this? The submitter owns the CI code?
Karl Palmskog (Jun 01 2023 at 10:43):I don't mind putting more documentation in my Coq CI scripts, though, if you specify some format for it
Gaëtan Gilbert (Jun 01 2023 at 10:51):codeowners is more machine oriented imo
Ali Caglayan (Jun 01 2023 at 11:17):This sounds like a good idea to me. What happens when it is outside of GitHub?
Gaëtan Gilbert (Jun 01 2023 at 11:19):you mean if the contact has no github account? we can put their email or zulip name or whatever works
Théo Zimmermann (Jun 02 2023 at 12:59):Sounds like a good idea to me too.
Théo Zimmermann (Jun 02 2023 at 12:59):Code owners are really best suited for people who have write access to a project (otherwise, they do not trigger review requests, for instance).
Karl Palmskog (Jun 02 2023 at 13:01):OK, so bottom line for me is that I'd be happy to document, but please consider first merging some documentation specifying the format with some examples.
Last updated: Nov 29 2023 at 21:01 UTC