feat: indicate replacements in synport output

[digama0]

Definitions that align are now printed like so:

#print Function.injective_id /-
theorem injective_id : Injective (@id α) := fun a₁ a₂ h => h
-/

The comment is the output mathport would have produced, if the definition Function.injective_id had not already existed in the environment. This is intended to make it easier to survey an already ported file and quickly identify any new definitions that have been introduced.

[gebner]

Is there an easy way to move the newline after the comment?

+#print PosPart /-
 /-- The positive part of an element admiting a decomposition into positive and negative parts.
 -/
 class PosPart (α : Type _) where
   Pos : α → α

+-/
+#print NegPart /-
 /-- The negative part of an element admiting a decomposition into positive and negative parts.
 -/
 class NegPart (α : Type _) where
   neg : α → α

+-/

[gebner]

We also get lots of parenthesization errors now, not sure which commit introduced them.

[digama0]

No, at least not if you mean fixing some \n in a string literal. We could add an extra newline but the trailing -/ would still be two lines away from the end of the command. To fix it properly we would need to either consume a newline from the string (which I suppose isn't crazy, since we can be fairly certain it has been emitted), or buffer command strings in a more structured way and use intersperse to avoid an extra trailing newline.

[digama0]

The parenthesization errors look like an uncaught issue from the last bump. Mathport is generating the following for rw [<- foo]:

(Tactic.rwSeq "rw" [] (Tactic.rwRuleSeq "[" [(Tactic.rwRule ["←"] `bind_map_eq_seq)] "]") [])

but lean now wants it to be:

(Tactic.rwSeq "rw" [] (Tactic.rwRuleSeq "[" [(Tactic.rwRule [(patternIgnore (token.«← » "←"))] `foo)] "]") [])

Are these additional nodes intentional? It looks like it will cause a lot of problems since I'm sure there are many other similar instances.

[gebner]

Oh yes, they are intentional. But they show up in the syntax definition, like group, etc. They tell the syntax pattern matching compiler to ignore that subterm. leanprover/lean4#1744 (comment)

[digama0]

The patternIgnore part looks unfortunate to me. Ideally the pattern match compiler would know that the original parser has a patternIgnore in it and so the runtime syntax wouldn't need it. In any case, I fixed the issue with rwRule and it fixed all the errors in core, although I haven't checked mathlib. I also added the aforementioned hack to get them printing like so instead:

+#print PosPart /-
 /-- The positive part of an element admiting a decomposition into positive and negative parts.
 -/
 class PosPart (α : Type _) where
   Pos : α → α
+-/

+#print NegPart /-
 /-- The negative part of an element admiting a decomposition into positive and negative parts.
 -/
 class NegPart (α : Type _) where
   neg : α → α
+-/

I can also take off another newline if you want, and have the -/ at the end of the last line of the command, but I thought this version would be more easily copy-paste-able.