perf: avoid re-exporting Std.Time from grind_annotated (#11372)

This PR makes the `Std.Time.Format` import in
`Lean.Elab.Tactic.Grind.Annotated` private rather than public,
preventing the entire `Std.Time` infrastructure (including timezone
databases) from being re-exported through `import Lean`.

The `grindAnnotatedExt` extension is kept private, with a new public
accessor function `isGrindAnnotatedModule` exposed for use by
`LibrarySuggestions.Basic`.

This should address the +2.5% instruction increase on `import Lean`
observed after merging #11332.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude <[email protected]>

Author: kim-em

src/Lean/Elab/Tactic/Grind/Annotated.lean

@@ -7,9 +7,7 @@ module
 prelude
 public import Lean.Elab.Command
 import Init.Grind.Annotated
-public import Std.Time.Format
-
-@[expose] public section
+import Std.Time.Format
 
 namespace Lean.Elab.Tactic.Grind
 open Command Std.Time
@@ -26,6 +24,12 @@ builtin_initialize grindAnnotatedExt : SimplePersistentEnvExtension Name NameSet
     asyncMode := .sync
   }
 
+/-- Check if a module has been marked as grind-annotated. -/
+public def isGrindAnnotatedModule (env : Environment) (modIdx : ModuleIdx) : Bool :=
+  let state := grindAnnotatedExt.getState env
+  let moduleName := env.header.moduleNames[modIdx.toNat]!
+  state.contains moduleName
+
 @[builtin_command_elab Lean.Parser.Command.grindAnnotated]
 def elabGrindAnnotated : CommandElab := fun stx => do
   let `(grind_annotated $dateStr) := stx | throwUnsupportedSyntax

src/Lean/LibrarySuggestions/Basic.lean

@@ -213,12 +213,6 @@ def combine (selector₁ selector₂ : Selector) : Selector := fun g c => do
 
   return sorted.take c.maxSuggestions
 
-/-- Check if a module has been marked as grind-annotated. -/
-def isGrindAnnotatedModule (env : Environment) (modIdx : ModuleIdx) : Bool :=
-  let state := Lean.Elab.Tactic.Grind.grindAnnotatedExt.getState env
-  let moduleName := env.header.moduleNames[modIdx.toNat]!
-  state.contains moduleName
-
 /--
 Filter out theorems from grind-annotated modules when the caller is "grind".
 Modules marked with `grind_annotated` contain manually reviewed/annotated theorems,
@@ -234,7 +228,7 @@ def filterGrindAnnotated (selector : Selector) : Selector := fun g c => do
       -- Check if the suggestion's module is grind-annotated
       match env.getModuleIdxFor? s.name with
       | none => return true  -- Keep suggestions with no module info
-      | some modIdx => return !isGrindAnnotatedModule env modIdx
+      | some modIdx => return !Lean.Elab.Tactic.Grind.isGrindAnnotatedModule env modIdx
   else
     return suggestions
 

tests/lean/run/grind_annotated.lean

@@ -25,12 +25,17 @@ Expected format: YYYY-MM-DD (e.g., "2025-01-15")
 #guard_msgs in
 grind_annotated "invalid-date"
 
-/-- info: Extension state contains `Init.Data.List.Lemmas: true -/
+/-- info: Init.Data.List.Lemmas is grind-annotated: true -/
 #guard_msgs in
 #eval do
   let env ← getEnv
-  let state := Lean.Elab.Tactic.Grind.grindAnnotatedExt.getState env
-  logInfo m!"Extension state contains `Init.Data.List.Lemmas: {state.contains `Init.Data.List.Lemmas}"
+  -- Use the public API to check if a module is grind-annotated
+  -- First we need to get the module index for a theorem from Init.Data.List.Lemmas
+  match env.getModuleIdxFor? `List.eq_nil_of_length_eq_zero with
+  | none => logInfo "Could not find module"
+  | some modIdx =>
+    let isAnnotated := Lean.Elab.Tactic.Grind.isGrindAnnotatedModule env modIdx
+    logInfo m!"Init.Data.List.Lemmas is grind-annotated: {isAnnotated}"
 
 /-! ## Filtering logic -/
 
@@ -58,9 +63,9 @@ example : True := by
     match env.getModuleIdxFor? theoremName with
     | none => logInfo "Theorem has no module index"
     | some modIdx =>
-      let moduleName := env.header.moduleNames[modIdx.toNat]!
-      let isAnnotated := Selector.isGrindAnnotatedModule env modIdx
-      let state := Lean.Elab.Tactic.Grind.grindAnnotatedExt.getState env
+      let _moduleName := env.header.moduleNames[modIdx.toNat]!
+      let _isAnnotated := Grind.isGrindAnnotatedModule env modIdx
+      pure ()
 
     -- Test 1: Without filter, suggestion should be returned
     let suggestions1 ← testSelector mvarId {}