feat: support MessageData in #eval #1967
Conversation
| h : p ∧ q | ||
| hAux : ¬p | ||
| ⊢ q ∧ q | ||
| [Meta.debug] case inl p q : Prop h : p ∧ q hAux : p ⊢ q ∧ q ------ case inr p q : Prop h : p ∧ q hAux : ¬p ⊢ q ∧ q |
There was a problem hiding this comment.
I don't really know why this PR changed the output here, but none of the spaces here were hard linebreaks (and everything fits on one line). ppGoal uses Format.line, and trace[foo] "bar\n" also uses Format.line (because the String→MessageData coercion replaces newlines by Format.line).
I've changed ppGoal to use hard newlines.
| @@ -1 +1 @@ | |||
| Except.ok Lean.Name.anonymous | |||
| Except.ok ([anonymous]) | |||
There was a problem hiding this comment.
Something that's consistently confusing is whether the output of #eval should be valid code via Repr, or if it can be any string representation whatsoever via ToString too. In any case the output here is a bit weird because it is mixing the valid code Except.ok (..) representation with ToString Name. Both the previous version and ok: [anonymous] seem to make more sense. I thought the new scoped instance (priority := low - 10) [ToString α] : Repr α where was causing this but it still appears after removing the instance so I am not sure about the reason.
There was a problem hiding this comment.
Indeed, it's not completely what the output of #eval should be. It used to take either a ToString or a Repr instance, so you already weren't guaranteed to get a "valid code" output.
The "culprit" here is the new instance:
scoped instance [ToMessageData ε] [ToMessageData α] : ToMessageData (Except ε α)Which raises another related question: should MessageData be more like Repr or like ToString?
There was a problem hiding this comment.
As for what it should be: for me the most important part is to get some output, and that expressions are clickable. None of the ToMessageData/Repr/ToString classes have instances for everything, so we'll need to mix them for some time.
There was a problem hiding this comment.
Which raises another related question: should MessageData be more like Repr or like ToString?
I'm afraid the answer is that we want both. We use the class for many specific types like Expr and Syntax where it is like ToString, but then there are instance like for List, and Except above, that should definitely be Repr-like (which would also properly handle the parentheses).
There was a problem hiding this comment.
that should definitely be Repr-like (which would also properly handle the parentheses).
Are you suggesting that toMessageData should have a precedence argument?
There was a problem hiding this comment.
I think we would a new, separate typeclass ReprToMessageData (or whatever), which should have a precedence argument, yeah
| let inst ← Meta.transform inst fun e => do | ||
| if let .app (.const ``EvalInstances.typeInfo [v]) α := e then | ||
| let ppE := (← ppExpr α).pretty | ||
| return .done (.app (.app (.const ``EvalInstances.TypeInfo.mk [v]) α) (toExpr ppE)) | ||
| else | ||
| return .continue |
There was a problem hiding this comment.
I think this block deserves a short comment
| @@ -1 +1 @@ | |||
| Except.ok Lean.Name.anonymous | |||
| Except.ok ([anonymous]) | |||
There was a problem hiding this comment.
Which raises another related question: should MessageData be more like Repr or like ToString?
I'm afraid the answer is that we want both. We use the class for many specific types like Expr and Syntax where it is like ToString, but then there are instance like for List, and Except above, that should definitely be Repr-like (which would also properly handle the parentheses).
The goal syntax is indentation-sensitive. If we leave out the newlines in goals like `h : p a b : Nat ⊢ a = b` then it's ambiguous what the free variables are.
gebner
force-pushed
the
evalmsgdata
branch
2 times, most recently
from
db69327
to
53821cb
Compare
| @@ -42,4 +42,4 @@ def sefFn (x_1 : obj) (x_2 : obj) : obj := | |||
| Lean.Expr.mdata._impl → | |||
| ret x_1 | |||
| Lean.Expr.proj._impl → | |||
| ret x_1 | |||
| ret x_1 | |||
There was a problem hiding this comment.
Why did this test lose an EOF newline?
This function uses soft newlines in many places where hard newlines are more appropriate. Pointed out by @gebner in leanprover#1967.
This adds two features to
#evalthat I've wanted for a long time.Repr/etc. instances.#eval (Except.ok (42, Bar.mk) : Except Foo (Nat × Bar))now works and prints 42 even if there are no instances forFooandBar.