fix: linter should have access to complete command message log (#8101)

This PR fixes a parallelism regression where linters that e.g. check for
errors in the command would no longer find such messages.

---------

Co-authored-by: damiano <adomani@gmail.com>

src/Lean/Elab/Command.lean

@@ -364,15 +364,26 @@ def runLintersAsync (stx : Syntax) : CommandElabM Unit := do
       runLinters stx
     return
 
+  -- linters should have access to the complete info tree and message log
+  let mut snaps := (← get).snapshotTasks
+  if let some elabSnap := (← read).snap? then
+    snaps := snaps.push { stx? := none, cancelTk? := none, task := elabSnap.new.result!.map (sync := true) toSnapshotTree }
+  let tree := SnapshotTree.mk { diagnostics := .empty } snaps
+  let treeTask ← tree.waitAll
+
   -- We only start one task for all linters for now as most linters are fast and we simply want
   -- to unblock elaboration of the next command
   let cancelTk ← IO.CancelToken.new
   let lintAct ← wrapAsyncAsSnapshot (cancelTk? := cancelTk) fun infoSt => do
+    let messages := tree.getAll.map (·.diagnostics.msgLog) |>.foldl (· ++ ·) .empty
+    -- do not double-report
+    modify ({ · with messages := messages.markAllReported })
     modifyInfoState fun _ => infoSt
     runLinters stx
 
-  -- linters should have access to the complete info tree
-  let task ← BaseIO.mapTask (t := (← getInfoState).substituteLazy) lintAct
+  let task ← BaseIO.bindTask (sync := true) (t := (← getInfoState).substituteLazy) fun infoSt =>
+    BaseIO.mapTask (t := treeTask) fun _ =>
+      lintAct infoSt
   logSnapshotTask { stx? := none, task, cancelTk? := cancelTk }
 
 protected def getCurrMacroScope : CommandElabM Nat  := do pure (← read).currMacroScope
@@ -579,10 +590,17 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
   let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
   let initInfoTrees ← getResetInfoTrees
   try
-    -- We should *not* factor out `elabCommand`'s `withLogging` to here since it would make its error
-    -- recovery more coarse. In particular, If `c` in `set_option ... in $c` fails, the remaining
-    -- `end` command of the `in` macro would be skipped and the option would be leaked to the outside!
-    elabCommand stx
+    try
+      -- We should *not* factor out `elabCommand`'s `withLogging` to here since it would make its error
+      -- recovery more coarse. In particular, if `c` in `set_option ... in $c` fails, the remaining
+      -- `end` command of the `in` macro would be skipped and the option would be leaked to the outside!
+      elabCommand stx
+    finally
+      -- Make sure `snap?` is definitely resolved; we do not use it for reporting as `#guard_msgs` may
+      -- be the caller of this function and add new messages and info trees
+      if let some snap := (← read).snap? then
+        snap.new.resolve default
+
     -- Run the linters, unless `#guard_msgs` is present, which is special and runs `elabCommandTopLevel` itself,
     -- so it is a "super-top-level" command. This is the only command that does this, so we just special case it here
     -- rather than engineer a general solution.
@@ -590,11 +608,6 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
       withLogging do
         runLintersAsync stx
   finally
-    -- Make sure `snap?` is definitely resolved; we do not use it for reporting as `#guard_msgs` may
-    -- be the caller of this function and add new messages and info trees
-    if let some snap := (← read).snap? then
-      snap.new.resolve default
-
     let msgs := (← get).messages
     modify fun st => { st with
       messages := initMsgs ++ msgs

tests/lean/linterUnusedVariables.lean

@@ -244,6 +244,7 @@ example (a : Nat) : Nat := _
 example (a : Nat) : Nat := sorry
 example (a : sorry) : Nat := 0
 example (a : Nat) : Nat := by
+theorem async (a : Nat) : Nat := by skip
 
 theorem Fin.eqq_of_val_eq {n : Nat} : ∀ {x y : Fin n}, x.val = y.val → x = y
   | ⟨_, _⟩, _, rfl => rfl

tests/lean/linterUnusedVariables.lean.expected.out

@@ -58,9 +58,14 @@ a : Nat
 ⊢ Nat
 linterUnusedVariables.lean:244:0-244:7: warning: declaration uses 'sorry'
 linterUnusedVariables.lean:245:0-245:7: warning: declaration uses 'sorry'
-linterUnusedVariables.lean:246:29-248:7: error: unexpected token 'theorem'; expected '{' or tactic
+linterUnusedVariables.lean:246:29-247:7: error: unexpected token 'theorem'; expected '{' or tactic
 linterUnusedVariables.lean:246:27-246:29: error: unsolved goals
 a : Nat
 ⊢ Nat
-linterUnusedVariables.lean:281:41-281:43: warning: unused variable `ha`
+linterUnusedVariables.lean:247:33-247:40: error: unsolved goals
+a : Nat
+⊢ Nat
+linterUnusedVariables.lean:247:0-247:40: error: type of theorem 'async' is not a proposition
+  Nat → Nat
+linterUnusedVariables.lean:282:41-282:43: warning: unused variable `ha`
 note: this linter can be disabled with `set_option linter.unusedVariables false`