2afca2df43
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.
48 lines
1.7 KiB
Text
48 lines
1.7 KiB
Text
import Lean.LibrarySuggestions
|
|
import Lean.Meta.Basic
|
|
import Std.Data.ExtHashMap
|
|
|
|
/-!
|
|
# Test that library suggestions persist across file boundaries
|
|
|
|
This test verifies that the default library suggestion engine set in
|
|
`Lean.LibrarySuggestions.Default` is correctly persisted when imported via `Lean.LibrarySuggestions`.
|
|
|
|
We do NOT call `set_library_suggestions` in this file - the selector should
|
|
already be set from importing Lean.LibrarySuggestions (which imports Default).
|
|
-/
|
|
|
|
/--
|
|
info: ✓ Selector found in imported state: (Term.open
|
|
"open"
|
|
(Command.openSimple [`Lean.LibrarySuggestions])
|
|
"in"
|
|
(Term.app `sineQuaNonSelector.filterGrindAnnotated.intersperse [`currentFile]))
|
|
---
|
|
info: ✓ Successfully retrieved selector using getSelector!
|
|
-/
|
|
#guard_msgs in
|
|
open Lean Lean.LibrarySuggestions in
|
|
run_cmd do
|
|
let stx? := librarySuggestionsExt.getState (← getEnv)
|
|
match stx? with
|
|
| none => Lean.logInfo "❌ No selector found in imported state!"
|
|
| some stx =>
|
|
Lean.logInfo s!"✓ Selector found in imported state: {stx}"
|
|
-- Try to retrieve the selector using getSelector
|
|
Elab.Command.liftTermElabM do
|
|
let selector? ← getSelector
|
|
match selector? with
|
|
| none => Lean.logInfo " ❌ getSelector returned none"
|
|
| some _ => Lean.logInfo " ✓ Successfully retrieved selector using getSelector!"
|
|
|
|
-- These examples should work with grind +suggestions but not grind alone
|
|
-- (proving that the suggestions engine is active and helping)
|
|
|
|
example {x : Dyadic} {prec : Int} : x.roundDown prec ≤ x := by
|
|
fail_if_success grind
|
|
grind +suggestions
|
|
|
|
example {x : Dyadic} {prec : Int} : (x.roundUp prec).precision ≤ some prec := by
|
|
fail_if_success grind
|
|
grind +suggestions
|