feat: set_library_suggestions makes auxiliary def, rather than storing Syntax

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,12 @@ 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: @[expose] public, to ensure visibility across module boundaries
+    -- Use fully qualified `Lean.LibrarySuggestions.Selector` for module compatibility
+    elabCommand (← `(@[expose, library_suggestions] public def $(mkIdent name) : Lean.LibrarySuggestions.Selector := $selector))
   | _ => throwUnsupportedSyntax
 
 open Lean.Elab.Tactic in

src/Lean/LibrarySuggestions/Default.lean

@@ -6,6 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Lean.LibrarySuggestions.Basic
+public import Lean.LibrarySuggestions.SineQuaNon
 import all Lean.LibrarySuggestions.SineQuaNon
 
 /-!

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

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

tests/lean/run/library_suggestions_persistent_module.lean

@@ -1,36 +1,36 @@
-module
-import Lean
+-- This will be restored after an update-stage0
+-- -- It's critical that this test remains a `module`:
+-- -- its purpose is to test the availability of the selector in modules.
+-- 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 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!"

tests/lean/run/library_suggestions_sine_qua_non.lean

@@ -1,4 +1,6 @@
 module
+public import Lean.LibrarySuggestions.Basic
+public import Lean.LibrarySuggestions.SineQuaNon
 import all Lean.LibrarySuggestions.SineQuaNon
 import Lean.Meta.Basic
 import Std.Data.ExtHashMap