Pretty-printing issue: trailing comments not always trimmed

Stream: lean4

[Thomas Murrills]

In certain cases, trailing comments are not trimmed when formatting syntax:

import Lean
open Lean

elab "fmt " stx:term : tactic => do
  logInfoAt stx (← PrettyPrinter.formatCategory `term stx)

def h {α : Type} : True := trivial

example : True := by
  fmt h (α := Nat)

-- A comment a few lines below

The logged info is

h (α := Nat)
  -- A comment a few lines below

Note that this doesn't happen with just fmt h; the named argument is necessary.

(1) Is this intentional (or at least inevitable)? Should I open an issue?

(2) Is there a simple workaround to trim the comments? (I couldn't find anything with Loogle.)

It has implications for Try this: suggestions, such as #std4 > simp? suggestion includes comments.

[Thomas Murrills]

Re: (2), I've just found Lean.Syntax.unsetTrailing, so I guess the question is really: is removing trailing info the right move when replacing syntax in Try this: suggestions?

[Kyle Miller]

I wonder if there should be some colGt-like-logic for trailing comments, if that's possible? In your example, I don't think anyone would consider that comment as being associated to that term. This is just a side thought I had.

I think using unsetTrailing is sort of right (I've used it for this purpose at least). If you use it for Try this: suggestions though, does it end up deleting that comment?

[Mario Carneiro]

The try this handler is already supposed to support this situation

[Thomas Murrills]

Kyle Miller said:

If you use it for Try this: suggestions though, does it end up deleting that comment?

No, it doesn't; if you insert a suggestion with a trailing comment like this, you get two comments, as in #std4 > simp? suggestion includes comments . I'm a bit confused as to why it considers it part of the syntax for formatting purposes, but not part of the syntax that gets replaced...

[Mario Carneiro]

it half-works: it will not delete the comment, but it will use trailing whitespace from the replacement syntax, so the comment gets duplicated here:

import Std.Tactic.TryThis
open Lean

elab "fmt " stx:term : tactic => do
  Std.Tactic.TryThis.addSuggestion (← getRef) stx

def h {α : Type} : True := trivial

example : True := by
  fmt h (α := Nat)

-- A comment a few lines below

[Mario Carneiro]

you have to call unsetTrailing yourself to get the desired behavior:

elab "fmt " stx:term : tactic => do
  Std.Tactic.TryThis.addSuggestion (← getRef) (⟨stx.raw.unsetTrailing⟩ : TSyntax `term)

[Mario Carneiro]

I'm inclined to say this is working as intended; normally you wouldn't spit an input syntax directly back out as a try this, and even if you do it might be wrapped in other stuff, so I don't think it can be addSuggestion's responsibility to clean it up

[Thomas Murrills]

I don't know; it seems weird that addSuggestion is not idempotent by default

[Mario Carneiro]

e.g.

elab "fmt " stx:term : tactic => do
  Std.Tactic.TryThis.addSuggestion (← getRef) (← `([$stx]))

def h {α : Type} : True := trivial

example : True := by
  fmt h (α := Nat)

which has the even worse result

Try this: [h (α := Nat)
      -- A comment a few lines below]

[Thomas Murrills]

Is there an example where preprocessing the argument to addSuggestion with unsetTrailing produces undesired behavior?

[Mario Carneiro]

well you might want to put a comment in the replacement

[Thomas Murrills]

Ah right

[Mario Carneiro]

in general Syntax lets you put comments anywhere before, inside, or after the tactic

[Mario Carneiro]

although as you can see line comments don't play well with outer syntax (note that the ] is commented out in my example)

[Thomas Murrills]

I think what’s weird to me is the inconsistency between the range we’re replacing (trimmed) and what we’re writing into that range (untrimmed)

[Thomas Murrills]

I’m not sure what the best way to handle it is, but I do worry this will become another minor responsibility for adding suggestions (“oh, you forgot unsetTrailing”)

[Mario Carneiro]

unlike the replacement, the source ref is pretty much always going to be a source span, so comment trimming is more sensible there

[Mario Carneiro]

this is probably true

[Mario Carneiro]

Although we can get a sense of this by auditing all existing uses

[Thomas Murrills]

hmm, what about an argument (trimTrailing := true) to addSuggestion? so if you really need to add a comment at the end, you can, but by default you don’t get bitten

[Mario Carneiro]

Again, what do existing uses look like? How many of them are currently making this mistake?

[Thomas Murrills]

True, I’ll check it out (unless I’m beaten to it) (later, I’m away from my computer)

[Mario Carneiro]

I suspect the issue is not restricted to addSuggestion, almost any place you directly echo user syntax is susceptible (e.g. simp?)

[Thomas Murrills]

Maybe the real question is “why are comments included in the trailing info in some situations but not others”

[Mario Carneiro]

that depends on the situation. For example mathport is one example of echoing user syntax and it absolutely does want to preserve comments

[Thomas Murrills]

(Actually, is it present in the syntax in both cases, but just formatted differently in different cases? I haven’t checked.)

[Mario Carneiro]

Most synthetic tactic exprs don't have any comments to preserve in the first place, and I would expect most addSuggestion calls to be of this form

[Thomas Murrills]

I actually think this might be an underlying pretty-printing issue. I’m not sure what the behavior should be, but it’s inconsistent as is. Check it out:

import Lean

open Lean

elab "show " stx:term : tactic => do
  logInfoAt stx m!"parse:{indentD <| if false then reprPrec stx 0 else "hidden"}
fmt:{indentD <|← PrettyPrinter.formatCategory `term stx}
pp:{indentD <|← PrettyPrinter.ppCategory `term stx}"

example : True := by
  show h
  -- a comment (not included in pp)
  show h ()
  -- a comment (included in pp)
  show h (x)
  -- a comment (included in pp)
  show Id.run do
    return ()
  -- a comment (not included in pp)
  show Id.run (do
    return ())
  -- a comment (included in pp)

(Change the condition after parse: to see the raw syntax.)

Note that trailing info is always present in the formatted versions. It’s just the pretty-printing that sometimes removes trailing info.

Based on the last examples, it seems like maybe the parenthesizer is leaving trailing info if possible, but trimming it if it re-parenthesizes things. But the first example doesn’t appear to involve any re-parenthesization, so maybe this is off base.

[Thomas Murrills]

(I better change the name of the topic…I’ll do so when I’m not on mobile.)