fix: revert "set_library_suggestions makes auxiliary def (#11396)" (#11417)

kim-em · claude · web-flow · commit 109ac9520c1e · 2025-11-28T11:03:17.000Z
This PR reverts #11396, which changed `set_library_suggestions` to create an auxiliary definition marked with `@[library_suggestions]`, rather than storing `Syntax` directly in the environment extension. It wasn't tested properly. Co-authored-by: Claude <noreply@anthropic.com>
diff --git a/src/Lean/LibrarySuggestions/Basic.lean b/src/Lean/LibrarySuggestions/Basic.lean
@@ -368,37 +368,38 @@ def currentFile : Selector := fun _ cfg => do
     | _ => continue
   return suggestions
 
-builtin_initialize librarySuggestionsExt : SimplePersistentEnvExtension Name (Option Name) ←
+builtin_initialize librarySuggestionsExt : SimplePersistentEnvExtension Syntax (Option Syntax) ←
   registerSimplePersistentEnvExtension {
-    addEntryFn := fun _ name => some name  -- Last entry wins
+    addEntryFn := fun _ stx => some stx  -- Last entry wins
     addImportedFn := fun entries =>
-      -- Take the last selector name from all imported modules
+      -- Take the last selector syntax from all imported modules
       entries.foldl (init := none) fun acc moduleEntries =>
-        moduleEntries.foldl (init := acc) fun _ name => some name
+        moduleEntries.foldl (init := acc) fun _ stx => some stx
   }
 
-/-- Attribute for registering library suggestions selectors. -/
-builtin_initialize librarySuggestionsAttr : TagAttribute ←
-  registerTagAttribute `library_suggestions "library suggestions selector" fun declName => do
-    let decl ← getConstInfo declName
-    unless decl.type == mkConst ``Selector do
-      throwError "declaration '{declName}' must have type `Selector`"
-    modifyEnv fun env => librarySuggestionsExt.addEntry env declName
+/--
+Helper function to elaborate and evaluate selector syntax.
+This is shared by both validation (`elabSetLibrarySuggestions`) and retrieval (`getSelector`).
+-/
+def elabAndEvalSelector (stx : Syntax) : MetaM Selector :=
+  Elab.Term.TermElabM.run' do
+    let selectorTerm ← Elab.Term.elabTermEnsuringType stx (some (Expr.const ``Selector []))
+    unsafe Meta.evalExpr Selector (Expr.const ``Selector []) selectorTerm
 
 /--
-Get the currently registered library suggestions selector by looking up the stored declaration name.
+Get the currently registered library suggestions selector by evaluating the stored syntax.
 Returns `none` if no selector is registered or if evaluation fails.
+
+Uses `Term.elabTermEnsuringType` to elaborate arbitrary syntax (not just identifiers).
 -/
-unsafe def getSelectorImpl : MetaM (Option Selector) := do
-  let some declName := librarySuggestionsExt.getState (← getEnv) | return none
+def getSelector : MetaM (Option Selector) := do
+  let some stx := librarySuggestionsExt.getState (← getEnv) | return none
   try
-    evalConstCheck Selector ``Selector declName
+    let selector ← elabAndEvalSelector stx
+    return some selector
   catch _ =>
     return none
 
-@[implemented_by getSelectorImpl]
-opaque getSelector : MetaM (Option Selector)
-
 /-- Generate library suggestions for the given metavariable, using the currently registered library suggestions engine. -/
 def select (m : MVarId) (c : Config := {}) : MetaM (Array Suggestion) := do
   let some selector ← getSelector |
@@ -424,11 +425,14 @@ def elabSetLibrarySuggestions : CommandElab
   | `(command| set_library_suggestions $selector) => do
     if `Lean.LibrarySuggestions.Basic ∉ (← getEnv).header.moduleNames then
       logWarning "Add `import Lean.LibrarySuggestions.Basic` before using the `set_library_suggestions` command."
-    -- Generate a fresh name for the selector definition
-    let name ← liftMacroM <| Macro.addMacroScope `_librarySuggestions
-    -- Elaborate the definition with the library_suggestions attribute
-    -- Note: not private, to ensure visibility across module boundaries
-    elabCommand (← `(@[library_suggestions] def $(mkIdent name) : Selector := $selector))
+    -- Validate that the syntax can be elaborated (to catch errors early)
+    liftTermElabM do
+      try
+        discard <| elabAndEvalSelector selector
+      catch _ =>
+        throwError "Failed to elaborate {selector} as a `MVarId → Config → MetaM (Array Suggestion)`."
+    -- Store the syntax (not the evaluated Selector) for persistence
+    modifyEnv fun env => librarySuggestionsExt.addEntry env selector
   | _ => throwUnsupportedSyntax
 
 open Lean.Elab.Tactic in
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
@@ -1,6 +1,6 @@
 #include "util/options.h"
 
-// stage0 update needed for grind_annotated command
+// stage0 update needed: revert library_suggestions aux def
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/run/library_suggestions.lean b/tests/lean/run/library_suggestions.lean
@@ -8,6 +8,8 @@ has type
 of sort `Type 1` but is expected to have type
   Lean.LibrarySuggestions.Selector
 of sort `Type`
+---
+error: Failed to elaborate Nat as a `MVarId → Config → MetaM (Array Suggestion)`.
 -/
 #guard_msgs in
 set_library_suggestions Nat
diff --git a/tests/lean/run/library_suggestions_persistent.lean b/tests/lean/run/library_suggestions_persistent.lean
@@ -1,45 +1,47 @@
--- This will be restored after an update-stage0
--- import Lean.LibrarySuggestions
--- import Lean.Meta.Basic
+import Lean.LibrarySuggestions
+import Lean.Meta.Basic
 
--- /-!
--- # Test that library suggestions persist across file boundaries
+/-!
+# 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`.
+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).
--- -/
+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 registered in imported state
--- ---
--- info:   ✓ getSelector succeeded
--- -/
--- #guard_msgs in
--- open Lean Lean.LibrarySuggestions in
--- run_cmd do
---   -- Check if a selector is registered
---   let hasSelector := (librarySuggestionsExt.getState (← getEnv)).isSome
---   if hasSelector then
---     Lean.logInfo "✓ Selector registered in imported state"
---     -- 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 "  ✓ getSelector succeeded"
---   else
---     Lean.logInfo "❌ No selector registered in imported state!"
+/--
+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)
+-- 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.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
+example {x : Dyadic} {prec : Int} : (x.roundUp prec).precision ≤ some prec := by
+  fail_if_success grind
+  grind +suggestions
diff --git a/tests/lean/run/library_suggestions_persistent_module.lean b/tests/lean/run/library_suggestions_persistent_module.lean
@@ -1,33 +1,36 @@
--- This will be restored after an update-stage0
--- import Lean
+module
+import Lean
 
--- /-!
--- # Test that library suggestions persist across file boundaries
+/-!
+# 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`.
+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).
--- -/
+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 registered in imported state
--- ---
--- info:   ✓ getSelector succeeded
--- -/
--- #guard_msgs in
--- open Lean Lean.LibrarySuggestions in
--- run_cmd do
---   -- Check if a selector is registered
---   let hasSelector := (librarySuggestionsExt.getState (← getEnv)).isSome
---   if hasSelector then
---     Lean.logInfo "✓ Selector registered in imported state"
---     -- 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 "  ✓ getSelector succeeded"
---   else
---     Lean.logInfo "❌ No selector registered in imported state!"
+/--
+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!"
