From 4323507b9105c2e0eb0ed4e2b47a6771eefcfe9e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 26 Apr 2025 13:36:21 +0200 Subject: [PATCH] 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 --- src/Lean/Elab/Command.lean | 35 +++++++++++++------ tests/lean/linterUnusedVariables.lean | 1 + .../linterUnusedVariables.lean.expected.out | 9 +++-- 3 files changed, 32 insertions(+), 13 deletions(-) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index aed9978afe..dc79c91326 100644 --- a/src/Lean/Elab/Command.lean +++ b/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 diff --git a/tests/lean/linterUnusedVariables.lean b/tests/lean/linterUnusedVariables.lean index 5f9cf56ae7..1def2ca5f7 100644 --- a/tests/lean/linterUnusedVariables.lean +++ b/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 diff --git a/tests/lean/linterUnusedVariables.lean.expected.out b/tests/lean/linterUnusedVariables.lean.expected.out index 4842d0c986..5a59655339 100644 --- a/tests/lean/linterUnusedVariables.lean.expected.out +++ b/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`