feat: implement grind_annotated command

- Add syntax declaration in Init/Grind/Annotated.lean
- Add elaborator with YYYY-MM-DD date validation in Lean/Elab/Tactic/Grind/Annotated.lean
- Add SimplePersistentEnvExtension to track grind-annotated modules
- Add filterGrindAnnotated wrapper for Selector
- Apply filter to sineQuaNonSelector in default library suggestions
- Set caller field to "grind" when grind tactic calls LibrarySuggestions

src/Init/Data/List/Lemmas.lean

@@ -13,6 +13,10 @@ import all Init.Data.List.BasicAux
 public import Init.Data.List.Control
 import all Init.Data.List.Control
 public import Init.BinderPredicates
+import Init.Grind.Annotated
+
+-- TODO: turn this on after an update-stage0
+-- grind_annotated "2025-01-24"
 
 public section
 

src/Init/Grind.lean

@@ -26,3 +26,4 @@ public import Init.Grind.Injective
 public import Init.Grind.Order
 public import Init.Grind.Interactive
 public import Init.Grind.Lint
+public import Init.Grind.Annotated

src/Init/Grind/Annotated.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+prelude
+public import Init.Tactics
+
+public section
+namespace Lean.Parser.Command
+
+/--
+`grind_annotated "YYYY-MM-DD"` marks the current file as having been manually annotated for `grind`.
+
+When the LibrarySuggestion framework is called with `caller := "grind"` (as happens when using
+`grind +suggestions`), theorems from grind-annotated files are excluded from premise selection.
+This is because these files have already been manually reviewed and annotated with appropriate
+`@[grind]` attributes.
+
+The date argument (in YYYY-MM-DD format) records when the file was annotated. This is currently
+informational only, but may be used in the future to detect files that have been significantly
+modified since annotation and may need re-review.
+
+Example:
+```
+grind_annotated "2025-01-15"
+```
+
+This command should typically appear near the top of a file, after imports.
+-/
+syntax (name := grindAnnotated) "grind_annotated" str : command
+
+end Lean.Parser.Command

src/Lean/Elab/Tactic/Grind.lean

@@ -14,3 +14,4 @@ public import Lean.Elab.Tactic.Grind.Trace
 public import Lean.Elab.Tactic.Grind.Config
 public import Lean.Elab.Tactic.Grind.Lint
 public import Lean.Elab.Tactic.Grind.LintExceptions
+public import Lean.Elab.Tactic.Grind.Annotated

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

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+prelude
+public import Lean.Elab.Command
+import Init.Grind.Annotated
+public import Std.Time.Format
+
+@[expose] public section
+
+namespace Lean.Elab.Tactic.Grind
+open Command Std.Time
+
+/--
+Extension to track modules that have been marked as "grind-annotated".
+These modules contain theorems that have been manually reviewed/annotated for grind,
+so they should be excluded from premise selection when the caller is "grind".
+-/
+builtin_initialize grindAnnotatedExt : SimplePersistentEnvExtension Name NameSet ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn := fun s modName => s.insert modName
+    addImportedFn := fun entries => entries.foldl (fun s arr => arr.foldl NameSet.insert s) ∅
+    asyncMode := .sync
+  }
+
+@[builtin_command_elab Lean.Parser.Command.grindAnnotated]
+def elabGrindAnnotated : CommandElab := fun stx => do
+  let `(grind_annotated $dateStr) := stx | throwUnsupportedSyntax
+
+  -- Extract the date string value
+  let dateValue := dateStr.getString
+
+  -- Validate that the date is in YYYY-MM-DD format using Std.Time
+  match PlainDate.parse dateValue with
+  | .error err =>
+    throwError "Invalid date format: {err}\nExpected format: YYYY-MM-DD (e.g., \"2025-01-15\")"
+  | .ok _ =>
+    -- Date is valid, mark the current module as grind-annotated
+    let modName ← getMainModule
+    modifyEnv (grindAnnotatedExt.addEntry · modName)
+
+end Lean.Elab.Tactic.Grind

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

@@ -164,7 +164,7 @@ def mkGrindParams
   let funCCs ← Grind.getFunCCSet
   let params := { params with ematch, casesTypes, inj, funCCs }
   let suggestions ← if config.suggestions then
-    LibrarySuggestions.select mvarId
+    LibrarySuggestions.select mvarId { caller := some "grind" }
   else
     pure #[]
   let mut params ← elabGrindParamsAndSuggestions params ps suggestions (only := only) (lax := config.lax)

src/Lean/LibrarySuggestions/Basic.lean

@@ -11,6 +11,7 @@ public import Lean.Meta.Eval
 public import Lean.Meta.CompletionName
 public import Lean.Linter.Deprecated
 public import Init.Data.Random
+public import Lean.Elab.Tactic.Grind.Annotated
 
 /-!
 # An API for library suggestion algorithms.
@@ -212,6 +213,31 @@ 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,
+so they should be excluded from automatic premise selection for grind.
+Other callers (like "simp") still receive suggestions from these modules.
+-/
+def filterGrindAnnotated (selector : Selector) : Selector := fun g c => do
+  let suggestions ← selector g c
+  -- Only filter when caller is "grind"
+  if c.caller == some "grind" then
+    let env ← getEnv
+    suggestions.filterM fun s => 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
+  else
+    return suggestions
+
 /--
 Combine two premise selectors by interspersing their results (ignoring scores).
 The parameter `ratio` (defaulting to 0.5) controls the ratio of suggestions from each selector

src/Lean/LibrarySuggestions/Default.lean

@@ -22,6 +22,7 @@ namespace Lean.LibrarySuggestions
 -- Set the default library suggestions engine to
 -- a combination of "Sine Qua Non" and the theorems from the current file.
 -- For now we just intersperse the results, but in future we should re-rank them.
-set_library_suggestions open Lean.LibrarySuggestions in sineQuaNonSelector.intersperse currentFile
+-- Note: We filter out grind-annotated modules from sineQuaNonSelector when caller is "grind".
+set_library_suggestions open Lean.LibrarySuggestions in sineQuaNonSelector.filterGrindAnnotated.intersperse currentFile
 
 end Lean.LibrarySuggestions

src/stdlib_flags.h

@@ -1,5 +1,6 @@
 #include "util/options.h"
 
+// stage0 update needed for grind_annotated command
 namespace lean {
 options get_default_options() {
     options opts;

tests/lean/run/library_suggestions_persistent.lean

@@ -17,7 +17,7 @@ info: ✓ Selector found in imported state: (Term.open
  "open"
  (Command.openSimple [`Lean.LibrarySuggestions])
  "in"
- (Term.app `sineQuaNonSelector.intersperse [`currentFile]))
+ (Term.app `sineQuaNonSelector.filterGrindAnnotated.intersperse [`currentFile]))
 ---
 info:   ✓ Successfully retrieved selector using getSelector!
 -/