diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean index bb3047b06f3d..2af14fc623f4 100644 --- a/src/Lean/Data/Position.lean +++ b/src/Lean/Data/Position.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich -/ prelude import Lean.Data.Format +import Lean.Data.Json import Lean.ToExpr namespace Lean @@ -12,7 +13,7 @@ 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 diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean index 1e5992ae4572..b07fd9b47da9 100644 --- a/src/Lean/Elab/Frontend.lean +++ b/src/Lean/Elab/Frontend.lean @@ -107,6 +107,7 @@ def runFrontend (mainModuleName : Name) (trustLevel : UInt32 := 0) (ileanFileName? : Option String := none) + (jsonOutput : Bool := false) : IO (Environment × Bool) := do let inputCtx := Parser.mkInputContext input fileName -- TODO: replace with `#lang` processing @@ -125,8 +126,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 @@ -141,7 +141,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) diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index e09fad85236c..2b1a20fc9ea1 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -135,6 +135,16 @@ class ToSnapshotTree (α : Type) where toSnapshotTree : α → SnapshotTree export ToSnapshotTree (toSnapshotTree) +/-- + 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. -/ @@ -142,25 +152,24 @@ 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 @@ -213,7 +222,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 diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 3414b5c3b98b..012c8c187bdb 100644 --- a/src/Lean/Message.lean +++ b/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 @@ -205,9 +205,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 @@ -216,24 +222,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. -/ diff --git a/src/util/shell.cpp b/src/util/shell.cpp index 9ed796413b7a..1209672b4a9f 100644 --- a/src/util/shell.cpp +++ b/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,6 +349,7 @@ 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 run_new_frontend( @@ -353,7 +357,8 @@ pair_ref run_new_frontend( options const & opts, std::string const & file_name, name const & main_module_name, uint32_t trust_level, - optional const & ilean_file_name + optional const & ilean_file_name, + uint8_t json ) { object * oilean_file_name = mk_option_none(); if (ilean_file_name) { @@ -366,6 +371,7 @@ pair_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 r = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl, ilean_fn); + pair_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());