feat: lean CLI option to print messages as JSON #3939
Conversation
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
tydeu
added
will-merge-soon
src/Lean/Message.lean
Outdated
| @[inline] def toMessage (msg : SerialMessage) : Message := | ||
| {msg with data := msg.data} | ||
|
|
||
| instance : Coe SerialMessage Message := ⟨SerialMessage.toMessage⟩ |
There was a problem hiding this comment.
Is this used? Seems like a slightly strange direction
There was a problem hiding this comment.
No, but this is potentially useful for Lean consumers of the JSON messages as they can report them back as normal messages. Since it sounds like we are unsure of this direction, I will remove the coercion.
src/Lean/Message.lean
Outdated
| return {msg with data := ← msg.data.toString} | ||
|
|
||
| protected def toString (msg : Message) (includeEndPos := false) : IO String := do | ||
| -- Remark: We inline here to avoid a copy in the case were `msg` is shared |
There was a problem hiding this comment.
I don't understand this comment. A copy of what? Should we care, what use case are we talking about that could make this relevant?
There was a problem hiding this comment.
If msg is not shared, Lean can just replace its data with its serialized version before applying toString. However, If the msg is shared, serializing it will require constructing (and allocating) and new BaseMessage with the same fields but serialized data (i.e., the "copy"). This will then be immediately deconstructed by the toString function. With the inline, we avoid this temporary allocation (as the serialization and destruction occur in the same function and thus Lean is smart enough to optimize it away).
Fixes a mixed up between the parameter and global variable for `json_output` the occurred during some name juggling in #3939.
Adds a
--jsonoption to theleanCLI. When used, the Lean frontend will print messages as JSON objects using the defaultToJsonencoding for theMessagestructure. This allows consumers (such as Lake) to handle Lean output in a more intelligent, well-structured way.Messagehas been refactored intoBaseMessage,Message, andSerialMessageto enable derivingToJson/FromJsoninstances automatically forBaseMessage/SerialMessage.SerialMessageis aMessagewith itsMessageDataeagerly serialized to aString.