feat: set_library_suggestions makes auxiliary def, rather than storing Syntax (#11396)

kim-em · web-flow · commit 157fbd08b450 · 2025-11-28T04:36:31.000Z
This PR changes `set_library_suggestions` to create an auxiliary definition marked with `@[library_suggestions]`, rather than storing `Syntax` directly in the environment extension. This enables better persistence and consistency of library suggestions across modules. The change requires a stage0 update before tests can be restored. After CI updates stage0, a follow-up PR will restore the test cases. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
diff --git a/src/Lean/LibrarySuggestions/Basic.lean b/src/Lean/LibrarySuggestions/Basic.lean
@@ -368,38 +368,37 @@ def currentFile : Selector := fun _ cfg => do
     | _ => continue
   return suggestions
 
-builtin_initialize librarySuggestionsExt : SimplePersistentEnvExtension Syntax (Option Syntax) ←
+builtin_initialize librarySuggestionsExt : SimplePersistentEnvExtension Name (Option Name) ←
   registerSimplePersistentEnvExtension {
-    addEntryFn := fun _ stx => some stx  -- Last entry wins
+    addEntryFn := fun _ name => some name  -- Last entry wins
     addImportedFn := fun entries =>
-      -- Take the last selector syntax from all imported modules
+      -- Take the last selector name from all imported modules
       entries.foldl (init := none) fun acc moduleEntries =>
-        moduleEntries.foldl (init := acc) fun _ stx => some stx
+        moduleEntries.foldl (init := acc) fun _ name => some name
   }
 
-/--
-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
+/-- 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
 
 /--
-Get the currently registered library suggestions selector by evaluating the stored syntax.
+Get the currently registered library suggestions selector by looking up the stored declaration name.
 Returns `none` if no selector is registered or if evaluation fails.
-
-Uses `Term.elabTermEnsuringType` to elaborate arbitrary syntax (not just identifiers).
 -/
-def getSelector : MetaM (Option Selector) := do
-  let some stx := librarySuggestionsExt.getState (← getEnv) | return none
+unsafe def getSelectorImpl : MetaM (Option Selector) := do
+  let some declName := librarySuggestionsExt.getState (← getEnv) | return none
   try
-    let selector ← elabAndEvalSelector stx
-    return some selector
+    evalConstCheck Selector ``Selector declName
   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 |
@@ -425,14 +424,11 @@ 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."
-    -- 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
+    -- 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))
   | _ => 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 for set_library_suggestions auxiliary 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,8 +8,6 @@ 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,47 +1,45 @@
-import Lean.LibrarySuggestions
-import Lean.Meta.Basic
+-- This will be restored after an update-stage0
+-- 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 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!"
+-- /--
+-- 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!"
 
--- 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,36 +1,33 @@
-module
-import Lean
+-- This will be restored after an update-stage0
+-- 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 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!"
+-- /--
+-- 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!"
