From 2afca2df4306c96f96fc49c29dd7ae59f8cc19ab Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Tue, 25 Nov 2025 13:12:35 +1100 Subject: [PATCH] feat: implement grind_annotated command (#11332) This PR adds a `grind_annotated "YYYY-MM-DD"` command that marks files as manually annotated for grind. When LibrarySuggestions is called with `caller := "grind"` (as happens with `grind +suggestions`), theorems from grind-annotated files are filtered out from premise selection. The date argument validates using Std.Time and is informational only for now, but could be used later to detect files that need re-review. There's no need for the library suggestions tools to suggest `grind` theorems from files that have already been carefully annotated by hand. --- src/Init/Data/List/Lemmas.lean | 4 ++ src/Init/Grind.lean | 1 + src/Init/Grind/Annotated.lean | 34 ++++++++++++++ src/Lean/Elab/Tactic/Grind.lean | 1 + src/Lean/Elab/Tactic/Grind/Annotated.lean | 45 +++++++++++++++++++ src/Lean/Elab/Tactic/Grind/Main.lean | 2 +- src/Lean/LibrarySuggestions/Basic.lean | 26 +++++++++++ src/Lean/LibrarySuggestions/Default.lean | 3 +- src/stdlib_flags.h | 1 + .../run/library_suggestions_persistent.lean | 2 +- 10 files changed, 116 insertions(+), 3 deletions(-) create mode 100644 src/Init/Grind/Annotated.lean create mode 100644 src/Lean/Elab/Tactic/Grind/Annotated.lean diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index c719cd4b92..341de59c97 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/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 diff --git a/src/Init/Grind.lean b/src/Init/Grind.lean index aa7ed691f8..af0601e517 100644 --- a/src/Init/Grind.lean +++ b/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 diff --git a/src/Init/Grind/Annotated.lean b/src/Init/Grind/Annotated.lean new file mode 100644 index 0000000000..cb329fc404 --- /dev/null +++ b/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 diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean index e15ca2fab8..b431b92e50 100644 --- a/src/Lean/Elab/Tactic/Grind.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Grind/Annotated.lean b/src/Lean/Elab/Tactic/Grind/Annotated.lean new file mode 100644 index 0000000000..f92e7d9618 --- /dev/null +++ b/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 diff --git a/src/Lean/Elab/Tactic/Grind/Main.lean b/src/Lean/Elab/Tactic/Grind/Main.lean index 52fab04568..ff3e6afdb7 100644 --- a/src/Lean/Elab/Tactic/Grind/Main.lean +++ b/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) diff --git a/src/Lean/LibrarySuggestions/Basic.lean b/src/Lean/LibrarySuggestions/Basic.lean index c053da9599..b92b337b77 100644 --- a/src/Lean/LibrarySuggestions/Basic.lean +++ b/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 diff --git a/src/Lean/LibrarySuggestions/Default.lean b/src/Lean/LibrarySuggestions/Default.lean index 976155419d..03c6be4108 100644 --- a/src/Lean/LibrarySuggestions/Default.lean +++ b/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 diff --git a/src/stdlib_flags.h b/src/stdlib_flags.h index 79a0e58edd..108af479bc 100644 --- a/src/stdlib_flags.h +++ b/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; diff --git a/tests/lean/run/library_suggestions_persistent.lean b/tests/lean/run/library_suggestions_persistent.lean index 767cc1863e..de8db28d43 100644 --- a/tests/lean/run/library_suggestions_persistent.lean +++ b/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! -/