Stream: coq-community devs & users

Topic: Editing Descriptions


view this post on Zulip Jason Gross (Jul 21 2020 at 18:17):

I just transferred run-coq-bug-minimizer to coq-community, but now I can't seem to edit the description to include [maintainer=@JasonGross]

view this post on Zulip Karl Palmskog (Jul 21 2020 at 18:34):

I can fix this. And while we always welcome new projects, we appreciate if you could go through the standard process (opening an issue in the manifesto repo) next time before you transfer a repo.

view this post on Zulip Karl Palmskog (Jul 21 2020 at 18:38):

@Jason Gross is the following description reasonably accurate for the repo:

Scripts for running the Coq minimizer on GitHub Actions

("A repo for ..." is not all that informative, and we always want to use "Coq" in the description somewhere)

view this post on Zulip Jason Gross (Jul 21 2020 at 18:41):

@Karl Palmskog It's half-accurate. I think one important point is that the repo itself is used for running the Coq Bug Minimizer (maybe reference https://github.com/JasonGross/coq-tools/#coq-bug-minimizer in the description?) on GH actions, in particular as it's the repo where coqbot will push branches to trigger the runs. So the interesting thing isn't so much the scripts as the actions that are actually run.

view this post on Zulip Jason Gross (Jul 21 2020 at 18:42):

(The scripts themselves are kind-of boring, as it's just about installing coq, cloning the minimizer repo, running it, and communicating with coqbot. I don't think the repo is of much interest to anyone who's not looking to actually run the minimizer on a concrete example, or looking to help with the coqbot infrastructure.)

view this post on Zulip Karl Palmskog (Jul 21 2020 at 18:43):

hmm, I don't think plain links will work in descriptions or they will take up all allowed space. How about:

Repository for triggering runs of the Coq bug minimizer using GitHub Actions


Last updated: Feb 05 2023 at 13:02 UTC