fix: some ExtraModUses

[Rob23oba]

This PR records extra mod uses that previously caused wrong unnecessary import reports from shake.

[Rob23oba]

cc @Kha
I didn't quite know what kind of tests to add for compilation; and do we not need to add any extraModUses in Lean.Compiler.LCNF.checkMeta?

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fd3f51012f0411701e1f1b7aa64eb1a2f09df6ad --onto ac0b82933f6eac9914011ca2caf38d0e4e991160. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-29 18:11:30)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5a2e46b0211ad353399b21af4be9edbe65c32b72 --onto 0b2193c7715a55246d0596a4db548c1b5b81562a. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-02 15:32:30)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase fd3f51012f0411701e1f1b7aa64eb1a2f09df6ad --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-29 18:11:32)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5a2e46b0211ad353399b21af4be9edbe65c32b72 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-02 15:32:31)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit d7b57ce.
The entire run failed.
Found no significant differences.

[Kha]

!bench

[leanprover-radar]

Failed to find a commit to compare against.

[leanprover-bot]

Here are the benchmark results for commit c30b4ff.
There were significant changes against commit 5a2e46b:

  Benchmark      Metric         Change
  ====================================
- channel.lean   boundedn_seq     2.3%

[Rob23oba]

Before we merge this, I'm currently working out which other problems we have after a lake exe shake --fix (many of which being related to ExtraModUses)

[Rob23oba]

Okay, here we go (format module: \ <fix / workaround> \ <problem / error>):

• Lean.Elab.MatchAltView:
  import Init.Data.Array.Basic -> public import Init.Data.Array.Basic
  This seems to be a fault of the Inhabited deriving handler not exposing the definition.
• Lean.Data.Trie, Lean.Widget.TaggedText, Lean.Data.Json.Printer:
  Format -> Std.Format / open Std (Format ToFormat)
export Std (Format) not being imported. (work-around probably fine?)
• Lean.Log:
  add back public import Lean.ErrorExplanations
  import not being used directly
• Lean.Elab.Util:
  add back meta import Lean.Parser.Command
  Parser (lhs) in syntax quotations not being recorded.
• Lean.Parser.Tactic.Doc:
  add back meta import Lean.Parser.Attr
  Parser (lhs) in syntax quotations not being recorded.
• Lean.PrettyPrinter.Formatter:
  add back public import Lean.Parser.StrInterpolation
combinator_formatter attribute not being recorded.
• Lean.PrettyPrinter.Parenthesizer:
  add back public import Lean.Parser.StrInterpolation
combinator_parenthesizer attribute not being recorded.
• Lean.Parser.Term.Basic:
  add back meta import Lean.Parser.Basic
  Syntax quotations not being recorded & maybe more complicated meta chains (non-meta def binderDefault being evaluated which depends on def leadingNode from Lean.Parser.Basic)
• Lean.Parser.Module:
  add back meta import Lean.Parser.Extra
  Same kind of meta chains for syntax quotations (e.g. Lean.Parser.Module.header -> Lean.Parser.leadingNode & Lean.Parser.optional etc.).
• Lean.PrettyPrinter.Delaborator.Builtins:
  add back meta import Lean.Parser.Command
  Again some meta chains.
• Lean.Elab.Tactic.Do.ProofMode.Assumption, ...ProofMode.Basic, Constructor, Exfalso, Frame, LeftRight:
  add back public import Std.Tactic.Do.Syntax
builtin_tactic attribute not being recorded.
• Lean.Data.Json.Elab:
  add back public import Lean.Data.Json.FromToJson
  resolved identifiers from syntax quotations not being recorded.
• Lean.Meta.Tactic.SolveByElim:
  add open Lean.Elab.Term
export Term (TermElabM) not being imported.
• Lean.Elab.Tactic.Monotonicity:
  add import Init.Internal.Order.Tactic
builtin_tactic attribute not being recorded.
• Lean.Elab.DocString.Builtin.Scopes:
  add meta import Lean.Parser.Extra
  Parser (lhs) in syntax quotations not being recorded.
• Lean.Elab.AuxDef:
  add meta import Lean.Parser.Command
  Syntax node kinds not being recorded in syntax declarations.
• Lean.Linter.UnusedVariables:
  add meta import Lean.Parser.Command
  Again some meta chains:
  Cannot evaluate constant Lean.Parser.Command.declModifiersT as it uses Lean.Parser.Command.declModifiers which is neither marked nor imported as meta
• Lean.Linter.MissingDocs:
  add back public import Lean.Parser.Syntax, public import Lean.Meta.Tactic.Simp.RegisterCommand
builtin_missing_docs_handler attribute not being recorded.
• Lean.Server.Completion.CompletionCollectors
  remove open FuzzyMatching
  nothing really wrong here, that open was simply not necessary
• Lean.Elab.DocString.Builtin.Keywords:
  remove open Lean.EditDistance
  again, nothing wrong, just an unnecessary open
• Lean.Elab.Tactic.Config:
  add back public import Lean.Meta.Eval
  resolved identifiers from syntax quotations not being recorded.
• Lean.Server.Rpc.Deriving:
  add meta import Lean.Parser.Term
  Again some meta chains in syntax quotations.
• Lean.Elab.Quotation:
  add meta import Lean.Parser.Term
  "Declaration Parser.Term.ident must be marked or imported as meta to be used as parser"
• Lean.Meta.Tactic.TryThis:
  add back meta import Lean.Meta.Hint
  "Cannot evaluate constant [email protected]._hygCtx._hyg.3 as it uses Lean.Meta.Hint.tryThisDiffWidget which is neither marked nor imported as meta"
• Lean.Elab.MutualInductive:
  add meta import Lean.Parser.Command
  Again some meta stuff in syntax quotations.
• Lean.Elab.Tactic.BVDecide.Frontend.BVCheck:
  remove open Std.Tactic.BVDecide.Reflect
  again, genuinely unnecessary open
• Lean.Elab.Declaration:
  add meta import Lean.Parser.Command
  Again some meta chains in syntax quotation stuff
• Lean.Meta.Tactic.Grind.Order.Internalize:
  remove open Arith.Cutsat, natToInt -> Arith.Cutsat.natToInt
  namespace not being imported (private import, in private scope)

[Kha]

@Rob23oba Thanks so much, that's an awesome list. I'd suggest for now though to get the parts already covered by the tests merged first in order to establish the test file. I'm also now wondering whether we should record the result of realizeGlobalConstCore by default, with an opt out for performance/false positives.

[Rob23oba]

Is it also fine if I just add tests for the new ones?

[Kha]

Sure, let's just not add even more fixes to this PR :) . Also if we go the realizeGlobalConstCore way, I'd argue everything covered by it may not need tests as the call is unlikely to vanish.

[Rob23oba]

Yeah, right, let's keep it at that. For some of the remaining stuff we might need to do something in evalCheckMeta and maybe introduce notation for keeping an import for unrelated reasons (e.g. to keep the public meta import Lean.Parser.Command in Lean.Elab.Command and public import Lean.ErrorExplanations in Lean.Log) but I'll let you do that in other PRs. Anyways, I'll be away until sunday, if you want anything changed about this PR, I'll let you commit it yourself.

[Kha]

I'm also now wondering whether we should record the result of realizeGlobalConstCore by default

One hitch here is that we still need to pass isMeta which may not have a sensible default. Or maybe a default of false would still be better than not recording anything.