fix: non-incremental command blocking further incremental reporting i…

…n macro (#4407)

As [reported on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/v4.2E9.2E0-rc1.20discussion/near/443356495).

src/Lean/Elab/Command.lean

@@ -393,15 +393,15 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
                   return oldSnap
                 let oldCmds? := oldSnap?.map fun old =>
                   if old.newStx.isOfKind nullKind then old.newStx.getArgs else #[old.newStx]
-                Language.withAlwaysResolvedPromises cmds.size fun promises => do
+                Language.withAlwaysResolvedPromises cmds.size fun cmdPromises => do
                   snap.new.resolve <| .ofTyped {
                     diagnostics := .empty
                     macroDecl := decl
                     newStx := stxNew
                     newNextMacroScope := nextMacroScope
                     hasTraces
-                    next := promises.zipWith cmds fun promise arg =>
-                      { range? := arg.getRange?, task := promise.result }
+                    next := cmdPromises.zipWith cmds fun cmdPromise cmd =>
+                      { range? := cmd.getRange?, task := cmdPromise.result }
                     : MacroExpandedSnapshot
                   }
                   -- After the first command whose syntax tree changed, we must disable
@@ -410,16 +410,20 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
                   let opts ← getOptions
                   -- For each command, associate it with new promise and old snapshot, if any, and
                   -- elaborate recursively
-                  for cmd in cmds, promise in promises, i in [0:cmds.size] do
+                  for cmd in cmds, cmdPromise in cmdPromises, i in [0:cmds.size] do
                     let oldCmd? := oldCmds?.bind (·[i]?)
                     withReader ({ · with snap? := some {
-                      new := promise
+                      new := cmdPromise
                       old? := do
                         guard reusedCmds
                         let old ← oldSnap?
                         return { stx := (← oldCmd?), val := (← old.next[i]?) }
                     } }) do
                       elabCommand cmd
+                      -- Resolve promise for commands not supporting incrementality; waiting for
+                      -- `withAlwaysResolvedPromises` to do this could block reporting by later
+                      -- commands
+                      cmdPromise.resolve default
                     reusedCmds := reusedCmds && oldCmd?.any (·.eqWithInfoAndTraceReuse opts cmd)
               else
                 elabCommand stxNew
@@ -441,6 +445,10 @@ register_builtin_option showPartialSyntaxErrors : Bool := {
   descr    := "show elaboration errors from partial syntax trees (i.e. after parser recovery)"
 }
 
+builtin_initialize
+  registerTraceClass `Elab.info
+  registerTraceClass `Elab.snapshotTree
+
 /--
 `elabCommand` wrapper that should be used for the initial invocation, not for recursive calls after
 macro expansion etc.
@@ -463,6 +471,12 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
     let mut msgs := (← get).messages
     for tree in (← getInfoTrees) do
       trace[Elab.info] (← tree.format)
+    if let some snap := (← read).snap? then
+      -- We can assume that the root command snapshot is not involved in parallelism yet, so this
+      -- should be true iff the command supports incrementality
+      if (← IO.hasFinished snap.new.result) then
+        trace[Elab.snapshotTree]
+          Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.format
     modify fun st => { st with
       messages := initMsgs ++ msgs
       infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees }

src/Lean/Elab/Frontend.lean

@@ -132,9 +132,6 @@ def process (input : String) (env : Environment) (opts : Options) (fileName : Op
   let s ← IO.processCommands inputCtx { : Parser.ModuleParserState } (Command.mkState env {} opts)
   pure (s.commandState.env, s.commandState.messages)
 
-builtin_initialize
-  registerTraceClass `Elab.info
-
 @[export lean_run_frontend]
 def runFrontend
     (input : String)

src/Lean/Language/Basic.lean

@@ -202,6 +202,16 @@ abbrev SnapshotTree.element : SnapshotTree → Snapshot
 abbrev SnapshotTree.children : SnapshotTree → Array (SnapshotTask SnapshotTree)
   | mk _ children => children
 
+/-- Produces debug tree format of given snapshot tree, synchronously waiting on all children. -/
+partial def SnapshotTree.format : SnapshotTree → Format := go none
+where go range? s :=
+  let range := match range? with
+    | some range => f!"{range.start}..{range.stop}"
+    | none => ""
+  let children := Std.Format.prefixJoin .line <|
+    s.children.toList.map fun c => go c.range? c.get
+  .nestD f!"• {range}{children}"
+
 /--
   Helper class for projecting a heterogeneous hierarchy of snapshot classes to a homogeneous
   representation. -/