style guidelines for grind

Stream: mathlib4

[Chris Henson]

A couple of months ago I asked:

Chris Henson said:

I'm sure it's in the works, but I would like to second the request for more information about the grind interactive mode, especially anchors. For instance, grind? now uses anchors in the suggestions it makes and it is unclear to me what are the style guidelines are around these.

I think in general (as I mentioned in #mathlib4 > Mathlib: the Missing Manuals @ 💬 ) that it would be helpful to have a style guide entry about grind. One I don't mention there is if grind only is analogous to simp only for squeezing purposes, and I am not sure how grind? suggesting interactive mode fits into that.

with the response understandably being that this was too early to consider at the time. However, Mathlib now has uses of interactive grind by @Jovan Gerbscheid in #34478 and a handful of squeezed terminal grind. There has also been some recent discussion about when it is preferable not to use grind, such as in #PR reviews > #34013 chore: golf with grind to reduce explicit lemma refer .

Is anyone already working on compiling these emerging standards (not just for the interactive mode, but grind in general) into a section for the style guidelines page? If not, is it still too early or would it be welcome if I started drafting a PR synthesizing what seems to be the consensus so far?