generating syntax with comments?

Stream: lean4

[Scott Morrison]

How can I produce Syntax that contains a comment?

I'd like to build something like rw [h] -- t as a Syntax, starting from h t : Expr, by delaborating both h and t. The intention here is to generate a "Try this" that shows the type of the result after the rewrite.

[Anand Rao Tadipatri]

@Scott Morrison I have been working on something related, though I am using trace messages rather than comments: https://github.com/siddhartha-gadgil/LeanAide/blob/main/LeanCodePrompts/TacticExtraction.lean.

The code works by stepping through the sequence of tactics and tracing the result of their application each time, making special provisions for some tactics like simp (to output the full simp only message) and rw (to output the goal state after each rewrite in a sequence of rewrites). I am also intercepting Lean's by tactic to output trace messages by default (an idea due to Leo de Moura and Mac), so any file that imports this one will have tactic proofs with trace messages.

[Scott Morrison]

I'm doing something else: not analyzing existing tactic blocks, but making suggestions from scratch, in another analogue of library_search.

[Siddhartha Gadgil]

Here is what seems the correct code:

def rwCommentSyntax (h t: Expr) : MetaM Syntax := do
  let hStx ← PrettyPrinter.delab h
  let tpp ← ppExpr t
  let stx1 ← `(tactic| rw [$hStx:term])
  let stx2 := mkAtom s!"-- {tpp}"
  let stx' := Syntax.node2 (SourceInfo.none) ``Lean.Parser.Tactic.rwSeq stx1 stx2
  return stx'

[Siddhartha Gadgil]

Sorry, the above is wrong in a couple of places.

[Scott Morrison]

I'm just getting

failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)

or with that option

[Error pretty printing syntax: parenthesize: uncaught backtrack exception. Falling back to raw printer.]
(Tactic.rwSeq
 (Tactic.rwSeq "rw" [] (Tactic.rwRuleSeq "[" [(Tactic.rwRule [] (Term.explicit "@" `List.map_append))] "]") [])
 "-- @List.map_append")

when I try your code.

[Siddhartha Gadgil]

Yes, it is wrong. I am trying to make the syntax match to that of the expression you need. Will try a bit more.

[Siddhartha Gadgil]

Sorry, this is beyond me.

[Sebastian Ullrich]

Untested:

  return stx1.raw.updateTrailing s!"-- {tpp}".toSubstring

[Siddhartha Gadgil]

It compiles but the comment does not seem to be in the result.

[Sebastian Ullrich]

Oh, yes, if you then feed that into the pretty printer, it currently discards all comments and whitespace...

[Siddhartha Gadgil]

Sebastian Ullrich said:

Oh, yes, if you then feed that into the pretty printer, it currently discards all comments and whitespace...

Can you point out where in the code this is done in the Lean 4 source? I need to do the same for async tactics (to pick up the tactic without trailing comments for code actions).

[Sebastian Ullrich]

My bad, this should indeed work https://github.com/leanprover/lean4/blob/8a302e6135bc1b0f1f2901702664c56cd424ebc2/src/Lean/PrettyPrinter/Formatter.lean#L332-L340

[Siddhartha Gadgil]

Thanks @Sebastian Ullrich
This may solve @Scott Morrison 's problem but I have the opposite problem - I want to get rid of trailing comments. Probably matching substrings will do this for me (using Lean.Syntax.getSubstring?).

[Sebastian Ullrich]

I had to do something similar recently - https://github.com/leanprover/lean4/commit/f9dcc9ca1bdf79a67220119daeda74ce3e821520

[Siddhartha Gadgil]

Thanks. I wanted to also discard comments. Is there a quick way?

[Sebastian Ullrich]

They are discarded as well (except for doc-comments)