Mini-RFC: optional position reporting in #guard_msgs

Stream: lean4

[Thomas Murrills]

I'm writing a draft PR (lean4#10125) to allow position reporting in #guard_msgs. This has come up before, e.g. here, and would recently be useful in #28919 (fixing an issue where messages were being reported on the wrong range).

Currently it's intended to be activated with #guard_msgs (positions := true), and to produce output formatted as

/--
@ +3:7...+3:11
info: foo
-/
#guard_msgs (positions := true) in
...

The line is relative to the line of the #guard_msgs token, which allows us to insert text above and below a position-sensitive test without breaking it. (The column, however, is absolute, which I think is fair.)

I'm pretty happy with this notation for the range: it's easy to pick up and distinguish visually due to the initial @ and spacing; it's relatively uncluttered; the + gestures at the fact that the line is relative; and the ... is vaguely consonant with the new PRange syntax. However, there are other possibilities, e.g.

• no @
• brackets, e.g. {+3:7...+3:11}
• parentheses around the line to group with +, e.g. (+3):7
• no +
• different range syntax, e.g. +3:7::+3:11 or (+3:7)-(+3:11)

Do we think that this is reasonable and useful in general? If so, should any of the terminology or formatting be tweaked?

[Kyle Miller]

There's a short accepted RFC about this: lean4#8265

(pinging @Joachim Breitner)

[Thomas Murrills]

Oh, thank you for finding that! (I searched, but missed it.)

[Thomas Murrills]

In that case, with the main build green, I'll allow discussion to happen on the PR and put it out for review. :)