Announcing policy decisions better

Stream: mathlib4

[Michael Rothgang]

(Case in point: at some point, it was decided (apparently, somewhere in this thread) that PRs renaming lemmas should also add deprecation aliases. TTBOMK, this was never announced; I'm not sure if it's documented anywhere. I agree with that policy; in any case, it's just an example.)

Right now,

• policy changes in mathlib often pass me by, until I read all of zulip (which feels pretty impossible until that's my full-time job) or randomly notice it during review or my PR

• reasons for a change are hard to find, often buried in long zulip discussions
  (These threads are good, they have additional context. But often, a short summary in addition would help a great deal.)

• these are (often) documented little: it's all on zulip, and finding a topic in such long threads can be hard.

I guess my primary audience (whom I'm doing this for) are contributors with not lots of time (i.e., who don't follow all details but the big picture), who want to stay somewhat up to date. This is hard right now, you learn about new policies during review (if at all). Sometimes, this makes your life harder than necessary. (For example, creating deprecation aliases after renaming lemmas is quite more tedious than doing it at the same time as the renames.)

Idea/proposed solution. Can/should there be a "public service announcements" thread for policy mathlib decisions made --- containing the decision and perhaps short summary of the reasons (but not meant for discussion)? As an extension, these decisions could then be reflected elsewhere as appropriate (to e.g., the style or reviewing guide on github).

[Michael Rothgang]

I know, this is project management work; such work often seems unsexy and needs a volunteer. (It's also really useful for open source projects: this talk by Alice Cecile articulates this very well.)
Perhaps, let's first talk about would people think this is useful?

[Yaël Dillies]

The relevant thread for your case is https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Backward.20compatibility

[Johan Commelin]

Thanks for linking to that talk by Alice Cecile. It contained some interesting ideas!

[Moritz Doll]

I would be very much in favor of having a design guide. I feel like best practices change quite often and it would be great if these get documented so that feature PRs could be requested to check whether they touch something that is in the design guide and for refactor PRs to say that they update some part of the mathlib to adhere to the current design, which should make reviewing refactor PRs way easier.

[Patrick Massot]

There is clearly a big need here, but it’s a lot of work, although it would be beneficial in the long run.