leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
43 stars 15 forks source link

feat: indicate replacements in synport output #198

Closed digama0 closed 2 years ago

digama0 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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

digama0 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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. https://github.com/leanprover/lean4/pull/1744#issuecomment-1282121706

digama0 commented 2 years ago

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.