Adding comments to commands

Stream: metaprogramming / tactics

[Damiano Testa]

I would like to generate the syntax for a command including a comment. Below is an example, but it seems that all comments get erased in the process.

import Mathlib.Tactic.RunCmd

open Lean in
run_cmd
  logInfo (← `(command|
    /-- doc-strings are ok -/
    def $(mkIdent `newOne) := 1
    -- but comments are not
  ))

prints

/-- doc-strings are ok -/
def newOne :=
  1

and my comment is gone.

[Jon Eugster]

I might be wrong here, but aren't comments already removed at the parsing step, so that Syntax doesn't know about them at all?

(doc comments on the other hand are parsed as Lean.Parser.Command.docComment)

[Thomas Murrills]

Are you trying to preserve comments from existing code or just generate new comments? I think there are at least ways to do the latter that may have been discussed here…

[Damiano Testa]

You are right: I would like to preserve existing comments. I have a hacky way of inserting comments as strings. You can see the actual code in #10864.

[Damiano Testa]

Although it seems that existing comments are preserved.

[Damiano Testa]

After a very small amount of testing, it seems that using `(command| ...) any comments in ... get parsed away. However, if your function takes a TSyntax `command as input and the command has embedded comments, then the comments are preserved.