function to strip comments from `Syntax`?

Stream: lean4

[Scott Morrison]

Is there an existing function that will strip out any comments from a Syntax?

This is needed for says, which is making mistake when verifying whenever there is a comment on the next line.

[Sebastian Ullrich]

Running the syntax through the formatter will do that as a side effect (but not give you back Syntax). If you want to strip comments while preserving all indentation, that's a bit harder. Could you say more about the use case?

[Scott Morrison]

During CI, X says Y runs the tactic X, and checks to see if it produces a "Try this: A" info message, and then checks that A = Y. Specifically it current checks:

(← Lean.PrettyPrinter.ppTactic ⟨A⟩).pretty = (← Lean.PrettyPrinter.ppTactic ⟨Y⟩).pretty

When the source code reads:

X says
  Y
-- Some comment

the -- Some comment is picked up as part of Y. (In fact, this is perhaps a "bug" in itself: the syntax for says includes a colGt.)

Thus I'd like to strip out that comment before comparing with A.

[Scott Morrison]

This leaves me confused, however, as this is running through the formatter!

[Sebastian Ullrich]

Oh, we are more advanced than I remembered: https://github.com/leanprover/lean4/blob/254582c00040609f7012fa4c2e0b26b289fe3842/src/Lean/PrettyPrinter/Formatter.lean#L369. So removing all SourceInfo should be sufficient. I see Gabriel has docs#Lean.Syntax.stripPos

[Scott Morrison]

Perfect, stripPos does the trick. #6381