Stream: coqbot devs & users

Topic: fiat_crypto_legacy messages


view this post on Zulip Ali Caglayan (Mar 28 2022 at 15:38):

@Jason Gross Are the fiat_crypto_legacy pings actually useful? I don't think they are particularly useful to keep around in the main PR. Aside from getting rid of it, could we redirect those comments to a dedicated thread on your fork to reduce the frequency of minimizer messages.

view this post on Zulip Théo Zimmermann (Mar 28 2022 at 15:41):

I also wonder if it could work to do the ping in the job summary (in the checks tab). Would GitHub create a notification in this case?

view this post on Zulip Ali Caglayan (Mar 28 2022 at 15:43):

On a force push the summary will (eventually) be lost, so I think a comment is a more persistent way to keep things around.

view this post on Zulip Ali Caglayan (Mar 28 2022 at 15:44):

We can add links to the original PR, commit and GitLab job too to make the comment more informative.

view this post on Zulip Jason Gross (Mar 28 2022 at 15:48):

Sure, feel free to comment on my fork instead with a link to the PR. It's most useful in cases where the allowed-failure tag would result in a merge that breaks fcl, i.e., cases where fcl fails but everything else that succeeds on master also succeeds on the PR

view this post on Zulip Théo Zimmermann (Mar 28 2022 at 15:49):

Doing this filtering would already reduce the noise a lot. (But Ali's idea is good as well.)


Last updated: Jan 31 2023 at 10:01 UTC