Style: Backticks in messages?

Stream: mathlib4

[Thomas Murrills]

Lean core seems to have adopted backticks around inline expressions and data in messages (e.g. m!"`{foo}` must have type `{bar}`"; see for instance lean4#10143. From what I can see, the convention is "names and interpolated data in messages should always be either inline and surrounded by backticks or on their own line and indented (via e.g. indentD)".

If I've interpreted it correctly, should Mathlib also adopt this as a style convention (and write it down in the style guide)?

(Our current noncompliance with this convention is partially from using quotes instead of backticks, but mostly from interpolating expressions and data inline without anything surrounding them at all.)

[Thomas Murrills]

(Also, have there been any prior discussions on this? I've looked but haven't been able to find anything.)

[Kenny Lau]

what's the advantage of writing backticks? they're printed in a monospace font anyway and when i quote an error message i put the message in backticks anyway...

[Thomas Murrills]

I guess I can think of two things:

1. clearly delineate the text which represents code/potentially hoverable expressions from the rest of the message's text
2. given that lean core does it, make the message feel the same as existing messages from lean core (i.e. like it's "supposed to be that way")

[Kim Morrison]

Sounds good to me.

[Kyle Miller]

I seem to remember that Mathlib was using backticks mostly, and this made its way into core eventually—then core liked it and decided it would be its convention this year.

One point in favor of backticks is that `x'` looks better than 'x'' .

Another (weak) advantage of backticks is that people are generally familiar with markdown so it's a hint that it's quoting code.

[Michael Rothgang]

This also makes test output for error messages nicer to read in VS Code.

[Michael Rothgang]

https://github.com/leanprover-community/leanprover-community.github.io/pull/705 documents this