Discussions on github for PR, issues etc

Stream: general

[Johannes Hölzl]

I think there are a lot of discussions at Zulip, which result in a PR. But often the discussion is missing in the pull request description. I have a hard time to follow all the discussions on Zulip, so I'm often missing why a parch in a PR is done in the specific way. Is it possible to have the discussions witch are PR specific on github itself?

For example for https://github.com/leanprover/mathlib/pull/339 I remember skimming over Zulip and that there was a discussion about the coeff map instead of using coercion to functions.

The advantage of linking of copying the discussion to the PR itself is that we can later see why a certain change was done. And I try to reference the github PR in the git commit message.

[Bryan Gin-ge Chen]

You could add a place in the "TO CONTRIBUTORS" text for links to any relevant zulip thread(s).

[Johannes Hölzl]

Oh, good idea!

[Scott Morrison]

Links back to Zulip are a start, but Johannes is right that for the longer term conversations archived on github are more useful. Unclear where the balance is!