From 805a1f4c790e36ac6def2900b4c55ec1a7c216af Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Tue, 10 Mar 2026 07:55:02 +0100
Subject: [PATCH] fix: spurious unused variable warnings

Fixes an issue where variables in Lean code blocks would trigger
spurious unused variable warnings.

The issue happens because the unused variable linter inspects info
trees. With embedded Lean blocks, it runs twice: once for the embedded
code, and again on the Verso command. The second time around, the
Verso syntax doesn't match the ignore functions, so it triggers
spurious warnings.

This bug was previously masked by the source span issue that was fixed
in #700.
---
 src/tests/Tests/LeanCode.lean                | 31 +++++++++++++++
 src/verso-manual/VersoManual/InlineLean.lean | 40 ++++++++++++++++++--
 2 files changed, 67 insertions(+), 4 deletions(-)

diff --git a/src/tests/Tests/LeanCode.lean b/src/tests/Tests/LeanCode.lean
index 45cbb1e1b..e58dd339e 100644
--- a/src/tests/Tests/LeanCode.lean
+++ b/src/tests/Tests/LeanCode.lean
@@ -77,3 +77,34 @@ info: (some (Verso.Genre.Manual.InlineLean.Inline.lean, [{"seq":
     | .other code _ => Option.some (code.name, code.data)
     | _ => .none
   | _ => .none
+
+-- Ensure no spurious unused variable warning for `α`
+#docs (Genre.Manual) mutualInductiveTest "Mutual Inductive Test" :=
+:::::::
+```lean
+mutual
+  inductive TreeA (α : Type) where
+    | leafA : TreeA α
+    | nodeA : α → TreeB α → TreeA α
+
+  inductive TreeB (α : Type) where
+    | leafB : TreeB α
+    | nodeB : α → TreeA α → TreeB α
+end
+```
+:::::::
+
+-- Genuinely unused variable in a code block: the inner linter produces a warning that
+-- appears in the generated highlighted output (via `nonSilentMsgs` in `elabCommands`).
+-- `reportMessages` silences non-error messages, so no build warning is emitted.
+#docs (Genre.Manual) unusedVarTest "Unused Var Test" :=
+:::::::
+```lean (name := unusedVar)
+def unusedArgFn (unused : Nat) : Nat := 0
+```
+```leanOutput unusedVar
+unused variable `unused`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
+```
+:::::::
diff --git a/src/verso-manual/VersoManual/InlineLean.lean b/src/verso-manual/VersoManual/InlineLean.lean
index e8b647468..1395917f4 100644
--- a/src/verso-manual/VersoManual/InlineLean.lean
+++ b/src/verso-manual/VersoManual/InlineLean.lean
@@ -219,6 +219,26 @@ private def toHighlightedLeanInline (shouldShow : Bool) (hls : Highlighted) (str
   ``(Inline.other (Verso.Genre.Manual.InlineLean.Inline.lean $(← quoteHighlightViaSerialization hls)) #[Inline.code $(quote str.getString)])
 
 
+/--
+Sets `linter.unusedVariables` to `false` in all `CommandContextInfo.options` within an info tree.
+
+This prevents the outer unused variable linter from re-processing variables that the inner linter
+(running via `elabCommandTopLevel`) has already correctly handled. This is needed to allow the
+unused variable linter to do the right thing for embedded Lean code. On the one hand, the linter
+needs to run, so that its warnings are accurately recorded. But the linter also may run on the Verso
+document, at which time it can inspect the info trees left behind by the embedded Lean and generate
+spurious warnings. Turning it off before saving info trees works around this issue.
+-/
+private partial def disableUnusedVarLinterInInfoTree : InfoTree → InfoTree
+  | .context (.commandCtx ci) child =>
+    .context (.commandCtx { ci with options := Lean.Linter.linter.unusedVariables.set ci.options false })
+      (disableUnusedVarLinterInInfoTree child)
+  | .context pci child =>
+    .context pci (disableUnusedVarLinterInInfoTree child)
+  | .node info children =>
+    .node info (children.map disableUnusedVarLinterInInfoTree)
+  | .hole id => .hole id
+
 def elabCommands (config : LeanBlockConfig) (str : StrLit)
     (toHighlightedLeanContent : (shouldShow : Bool) → (hls : Highlighted) → (str: StrLit) → DocElabM Term)
     (minCommands : Option Nat := none)
@@ -233,9 +253,11 @@ def elabCommands (config : LeanBlockConfig) (str : StrLit)
 
     let origScopes ← if config.fresh then pure [{header := ""}] else getScopes
 
-    -- Turn off async elaboration so that info trees and messages are available when highlighting syntax
+    -- Turn off async elaboration so that info trees and messages are available when highlighting syntax.
     let origScopes := origScopes.modifyHead fun sc =>
-      { sc with opts := pp.tagAppFns.set (Elab.async.set sc.opts false) true }
+      let opts := Elab.async.set sc.opts false
+      let opts := pp.tagAppFns.set opts true
+      { sc with opts }
 
     let altStr ← parserInputString str
 
@@ -255,8 +277,16 @@ def elabCommands (config : LeanBlockConfig) (str : StrLit)
       cmdState := { cmdState with messages := messages }
 
 
+      -- Use elabCommandTopLevel so that linters run after each command (matching Lean's normal
+      -- behavior). Since it resets messages and infoState, save and restore them to accumulate.
+      let savedMsgs := cmdState.messages
+      let savedTrees := cmdState.infoState.trees
       cmdState ← withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.lean, stx := cmd})) <|
-        runCommand (Command.elabCommand cmd) cmd cctx cmdState
+        runCommand (Command.elabCommandTopLevel cmd) cmd cctx cmdState
+      cmdState := { cmdState with
+        messages := savedMsgs ++ cmdState.messages,
+        infoState := { cmdState.infoState with trees := savedTrees ++ cmdState.infoState.trees }
+      }
 
       if Parser.isTerminalCommand cmd then break
 
@@ -275,8 +305,10 @@ def elabCommands (config : LeanBlockConfig) (str : StrLit)
       setEnv cmdState.env
       setScopes cmdState.scopes
 
+      -- The inner linter has already run correctly via elabCommandTopLevel, so we need to avoid
+      -- re-running it.
       for t in cmdState.infoState.trees do
-        pushInfoTree t
+        pushInfoTree (disableUnusedVarLinterInInfoTree t)
 
 
       let mut hls := Highlighted.empty