Stream: Coq devs & plugin devs

Topic: document people to contact for CI projects


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

view this post on Zulip Karl Palmskog (Jun 01 2023 at 10:42):

could one use code owners for this? The submitter owns the CI code?

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

view this post on Zulip Gaëtan Gilbert (Jun 01 2023 at 10:51):

codeowners is more machine oriented imo

view this post on Zulip Ali Caglayan (Jun 01 2023 at 11:17):

This sounds like a good idea to me. What happens when it is outside of GitHub?

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

view this post on Zulip Théo Zimmermann (Jun 02 2023 at 12:59):

Sounds like a good idea to me too.

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

view this post on Zulip 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: May 18 2024 at 08:40 UTC