feat: lean CLI option to print messages as JSON (#3939)

Adds a `--json` option to the `lean` CLI. When used, the Lean frontend
will print messages as JSON objects using the default `ToJson` encoding
for the `Message` structure. This allows consumers (such as Lake) to
handle Lean output in a more intelligent, well-structured way.

`Message` has been refactored into `BaseMessage`, `Message`, and
`SerialMessage` to enable deriving `ToJson`/ `FromJson` instances
automatically for `BaseMessage` / `SerialMessage`. `SerialMessage` is a
`Message` with its `MessageData` eagerly serialized to a `String`.

src/Lean/Data/Position.lean

@@ -5,14 +5,15 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Lean.Data.Format
+import Lean.Data.Json
 import Lean.ToExpr
 
 namespace Lean
 
 structure Position where
   line   : Nat
   column : Nat
-  deriving Inhabited, DecidableEq, Repr
+  deriving Inhabited, DecidableEq, Repr, ToJson, FromJson
 
 namespace Position
 protected def lt : Position → Position → Bool

src/Lean/Elab/Frontend.lean

@@ -109,6 +109,7 @@ def runFrontend
     (mainModuleName : Name)
     (trustLevel : UInt32 := 0)
     (ileanFileName? : Option String := none)
+    (jsonOutput : Bool := false)
     : IO (Environment × Bool) := do
   let startTime := (← IO.monoNanosNow).toFloat / 1000000000
   let inputCtx := Parser.mkInputContext input fileName
@@ -129,8 +130,7 @@ def runFrontend
       commandState := { commandState with infoState.enabled := true }
 
     let s ← IO.processCommands inputCtx parserState commandState
-    for msg in s.commandState.messages.toList do
-      IO.print (← msg.toString (includeEndPos := Language.printMessageEndPos.get opts))
+    Language.reportMessages s.commandState.messages opts jsonOutput
 
     if let some ileanFileName := ileanFileName? then
       let trees := s.commandState.infoState.trees.toArray
@@ -158,7 +158,7 @@ def runFrontend
   let processor := Language.Lean.process
   let snap ← processor none ctx
   let snaps := Language.toSnapshotTree snap
-  snaps.runAndReport opts
+  snaps.runAndReport opts jsonOutput
   if let some ileanFileName := ileanFileName? then
     let trees := snaps.getAll.concatMap (match ·.infoTree? with | some t => #[t] | _ => #[])
     let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false)

src/Lean/Language/Basic.lean

@@ -209,32 +209,41 @@ def DynamicSnapshot.toTyped? (α : Type) [TypeName α] (snap : DynamicSnapshot)
     Option α :=
   snap.val.get? α
 
+/--
+  Runs a tree of snapshots to conclusion, incrementally performing `f` on each snapshot in tree
+  preorder. -/
+@[specialize] partial def SnapshotTree.forM [Monad m] (s : SnapshotTree)
+    (f : Snapshot → m PUnit) : m PUnit := do
+  match s with
+  | mk element children =>
+    f element
+    children.forM (·.get.forM f)
+
 /--
   Option for printing end position of each message in addition to start position. Used for testing
   message ranges in the test suite. -/
 register_builtin_option printMessageEndPos : Bool := {
   defValue := false, descr := "print end position of each message in addition to start position"
 }
 
+/-- Reports messages on stdout. If `json` is true, prints messages as JSON (one per line). -/
+def reportMessages (msgLog : MessageLog) (opts : Options) (json := false) : IO Unit := do
+  if json then
+    msgLog.forM (·.toJson <&> (·.compress) >>= IO.println)
+  else
+    msgLog.forM (·.toString (includeEndPos := printMessageEndPos.get opts) >>= IO.print)
+
 /--
   Runs a tree of snapshots to conclusion and incrementally report messages on stdout. Messages are
   reported in tree preorder.
   This function is used by the cmdline driver; see `Lean.Server.FileWorker.reportSnapshots` for how
   the language server reports snapshots asynchronously.  -/
-partial def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) : IO Unit := do
-  s.element.diagnostics.msgLog.forM
-    (·.toString (includeEndPos := printMessageEndPos.get opts) >>= IO.print)
-  for t in s.children do
-    t.get.runAndReport opts
+def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) (json := false) : IO Unit := do
+  s.forM (reportMessages ·.diagnostics.msgLog opts json)
 
 /-- Waits on and returns all snapshots in the tree. -/
-partial def SnapshotTree.getAll (s : SnapshotTree) : Array Snapshot :=
-  go s |>.run #[] |>.2
-where
-  go s : StateM (Array Snapshot) Unit := do
-    modify (·.push s.element)
-    for t in s.children do
-      go t.get
+def SnapshotTree.getAll (s : SnapshotTree) : Array Snapshot :=
+  s.forM (m := StateM _) (fun s => modify (·.push s)) |>.run #[] |>.2
 
 /-- Metadata that does not change during the lifetime of the language processing process. -/
 structure ModuleProcessingContext where
@@ -287,7 +296,7 @@ end Language
 /--
   Builds a function for processing a language using incremental snapshots by passing the previous
   snapshot to `Language.process` on subsequent invocations. -/
-partial def Language.mkIncrementalProcessor (process : Option InitSnap → ProcessingM InitSnap)
+def Language.mkIncrementalProcessor (process : Option InitSnap → ProcessingM InitSnap)
     (ctx : ModuleProcessingContext) : BaseIO (Parser.InputContext → BaseIO InitSnap) := do
   let oldRef ← IO.mkRef none
   return fun ictx => do

src/Lean/Message.lean

@@ -23,7 +23,7 @@ def mkErrorStringWithPos (fileName : String) (pos : Position) (msg : String) (en
 
 inductive MessageSeverity where
   | information | warning | error
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, ToJson, FromJson
 
 structure MessageDataContext where
   env  : Environment
@@ -209,9 +209,15 @@ instance : Coe (List Expr) MessageData := ⟨fun es => ofList <| es.map ofExpr
 
 end MessageData
 
-/-- A `Message` is a richly formatted piece of information emitted by Lean.
-They are rendered by client editors in the infoview and in diagnostic windows. -/
-structure Message where
+/--
+A `BaseMessage` is a richly formatted piece of information emitted by Lean.
+They are rendered by client editors in the infoview and in diagnostic windows.
+There are two varieties in the Lean core:
+* `Message`: Uses structured, effectful `MessageData` for formatting content.
+* `SerialMessage`: Stores pure `String` data. Obtained by running the effectful
+`Message.serialize`.
+-/
+structure BaseMessage (α : Type u) where
   fileName      : String
   pos           : Position
   endPos        : Option Position := none
@@ -220,24 +226,53 @@ structure Message where
   severity      : MessageSeverity := MessageSeverity.error
   caption       : String          := ""
   /-- The content of the message. -/
-  data          : MessageData
-  deriving Inhabited
+  data          : α
+  deriving Inhabited, ToJson, FromJson
 
-namespace Message
+/-- A `Message` is a richly formatted piece of information emitted by Lean.
+They are rendered by client editors in the infoview and in diagnostic windows. -/
+abbrev Message := BaseMessage MessageData
 
-protected def toString (msg : Message) (includeEndPos := false) : IO String := do
-  let mut str ← msg.data.toString
+/-- A `SerialMessage` is a `Message` whose `MessageData` has been eagerly
+serialized and is thus appropriate for use in pure contexts where the effectful
+`MessageData.toString` cannot be used. -/
+abbrev SerialMessage := BaseMessage String
+
+namespace SerialMessage
+
+@[inline] def toMessage (msg : SerialMessage) : Message :=
+  {msg with data := msg.data}
+
+protected def toString (msg : SerialMessage) (includeEndPos := false) : String := Id.run do
+  let mut str := msg.data
   let endPos := if includeEndPos then msg.endPos else none
   unless msg.caption == "" do
     str := msg.caption ++ ":\n" ++ str
   match msg.severity with
-  | MessageSeverity.information => pure ()
-  | MessageSeverity.warning     => str := mkErrorStringWithPos msg.fileName msg.pos (endPos := endPos) "warning: " ++ str
-  | MessageSeverity.error       => str := mkErrorStringWithPos msg.fileName msg.pos (endPos := endPos) "error: " ++ str
+  | .information => pure ()
+  | .warning     => str := mkErrorStringWithPos msg.fileName msg.pos (endPos := endPos) "warning: " ++ str
+  | .error       => str := mkErrorStringWithPos msg.fileName msg.pos (endPos := endPos) "error: " ++ str
   if str.isEmpty || str.back != '\n' then
     str := str ++ "\n"
   return str
 
+instance : ToString SerialMessage := ⟨SerialMessage.toString⟩
+
+end SerialMessage
+
+namespace Message
+
+@[inline] def serialize (msg : Message) : IO SerialMessage := do
+  return {msg with data := ← msg.data.toString}
+
+protected def toString (msg : Message) (includeEndPos := false) : IO String := do
+  -- Remark: The inline here avoids a new message allocation when `msg` is shared
+  return inline <| (← msg.serialize).toString includeEndPos
+
+protected def toJson (msg : Message) : IO Json := do
+  -- Remark: The inline here avoids a new message allocation when `msg` is shared
+  return inline <| toJson (← msg.serialize)
+
 end Message
 
 /-- A persistent array of messages. -/

src/util/shell.cpp

@@ -217,6 +217,7 @@ static void display_help(std::ostream & out) {
 #endif
     std::cout << "  --plugin=file      load and initialize Lean shared library for registering linters etc.\n";
     std::cout << "  --load-dynlib=file load shared library to make its symbols available to the interpreter\n";
+    std::cout << "  --json             report Lean output (e.g., messages) as JSON (one per line)\n";
     std::cout << "  --deps             just print dependencies of a Lean input\n";
     std::cout << "  --print-prefix     print the installation prefix for Lean and exit\n";
     std::cout << "  --print-libdir     print the installation directory for Lean's built-in libraries and exit\n";
@@ -230,6 +231,7 @@ static void display_help(std::ostream & out) {
 
 static int print_prefix = 0;
 static int print_libdir = 0;
+static int json_output = 0;
 
 static struct option g_long_options[] = {
     {"version",      no_argument,       0, 'v'},
@@ -260,6 +262,7 @@ static struct option g_long_options[] = {
 #endif
     {"plugin",       required_argument, 0, 'p'},
     {"load-dynlib",  required_argument, 0, 'l'},
+    {"json",         no_argument,       &json_output, 1},
     {"print-prefix", no_argument,       &print_prefix, 1},
     {"print-libdir", no_argument,       &print_libdir, 1},
 #ifdef LEAN_DEBUG
@@ -346,14 +349,16 @@ extern "C" object * lean_run_frontend(
     object * main_module_name,
     uint32_t trust_level,
     object * ilean_filename,
+    uint8_t  json_output,
     object * w
 );
 pair_ref<environment, object_ref> run_new_frontend(
     std::string const & input,
     options const & opts, std::string const & file_name,
     name const & main_module_name,
     uint32_t trust_level,
-    optional<std::string> const & ilean_file_name
+    optional<std::string> const & ilean_file_name,
+    uint8_t json
 ) {
     object * oilean_file_name = mk_option_none();
     if (ilean_file_name) {
@@ -366,6 +371,7 @@ pair_ref<environment, object_ref> run_new_frontend(
         main_module_name.to_obj_arg(),
         trust_level,
         oilean_file_name,
+        json_output,
         io_mk_world()
     ));
 }
@@ -716,7 +722,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
 
         if (!main_module_name)
             main_module_name = name("_stdin");
-        pair_ref<environment, object_ref> r = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl, ilean_fn);
+        pair_ref<environment, object_ref> r = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl, ilean_fn, json_output);
         env = r.fst();
         bool ok = unbox(r.snd().raw());