Skip to content

Commit bb04169

Browse files
kim-emkim-em
committed
feat: set_library_suggestions makes auxiliary def, rather than storing Syntax
1 parent eb82984 commit bb04169

File tree

6 files changed

+98
-101
lines changed

6 files changed

+98
-101
lines changed

‎src/Lean/LibrarySuggestions/Basic.lean‎

Lines changed: 24 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -368,38 +368,37 @@ def currentFile : Selector := fun _ cfg => do
368368
| _ => continue
369369
return suggestions
370370

371-
builtin_initialize librarySuggestionsExt : SimplePersistentEnvExtension Syntax (Option Syntax) ←
371+
builtin_initialize librarySuggestionsExt : SimplePersistentEnvExtension Name (Option Name) ←
372372
registerSimplePersistentEnvExtension {
373-
addEntryFn := fun _ stx => some stx -- Last entry wins
373+
addEntryFn := fun _ name => some name -- Last entry wins
374374
addImportedFn := fun entries =>
375-
-- Take the last selector syntax from all imported modules
375+
-- Take the last selector name from all imported modules
376376
entries.foldl (init := none) fun acc moduleEntries =>
377-
moduleEntries.foldl (init := acc) fun _ stx => some stx
377+
moduleEntries.foldl (init := acc) fun _ name => some name
378378
}
379379

380-
/--
381-
Helper function to elaborate and evaluate selector syntax.
382-
This is shared by both validation (`elabSetLibrarySuggestions`) and retrieval (`getSelector`).
383-
-/
384-
def elabAndEvalSelector (stx : Syntax) : MetaM Selector :=
385-
Elab.Term.TermElabM.run' do
386-
let selectorTerm ← Elab.Term.elabTermEnsuringType stx (some (Expr.const ``Selector []))
387-
unsafe Meta.evalExpr Selector (Expr.const ``Selector []) selectorTerm
380+
/-- Attribute for registering library suggestions selectors. -/
381+
builtin_initialize librarySuggestionsAttr : TagAttribute ←
382+
registerTagAttribute `library_suggestions "library suggestions selector" fun declName => do
383+
let decl ← getConstInfo declName
384+
unless decl.type == mkConst ``Selector do
385+
throwError "declaration '{declName}' must have type `Selector`"
386+
modifyEnv fun env => librarySuggestionsExt.addEntry env declName
388387

389388
/--
390-
Get the currently registered library suggestions selector by evaluating the stored syntax.
389+
Get the currently registered library suggestions selector by looking up the stored declaration name.
391390
Returns `none` if no selector is registered or if evaluation fails.
392-
393-
Uses `Term.elabTermEnsuringType` to elaborate arbitrary syntax (not just identifiers).
394391
-/
395-
def getSelector : MetaM (Option Selector) := do
396-
let some stx := librarySuggestionsExt.getState (← getEnv) | return none
392+
unsafe def getSelectorImpl : MetaM (Option Selector) := do
393+
let some declName := librarySuggestionsExt.getState (← getEnv) | return none
397394
try
398-
let selector ← elabAndEvalSelector stx
399-
return some selector
395+
evalConstCheck Selector ``Selector declName
400396
catch _ =>
401397
return none
402398

399+
@[implemented_by getSelectorImpl]
400+
opaque getSelector : MetaM (Option Selector)
401+
403402
/-- Generate library suggestions for the given metavariable, using the currently registered library suggestions engine. -/
404403
def select (m : MVarId) (c : Config := {}) : MetaM (Array Suggestion) := do
405404
let some selector ← getSelector |
@@ -425,14 +424,12 @@ def elabSetLibrarySuggestions : CommandElab
425424
| `(command| set_library_suggestions $selector) => do
426425
if `Lean.LibrarySuggestions.Basic ∉ (← getEnv).header.moduleNames then
427426
logWarning "Add `import Lean.LibrarySuggestions.Basic` before using the `set_library_suggestions` command."
428-
-- Validate that the syntax can be elaborated (to catch errors early)
429-
liftTermElabM do
430-
try
431-
discard <| elabAndEvalSelector selector
432-
catch _ =>
433-
throwError "Failed to elaborate {selector} as a `MVarId → Config → MetaM (Array Suggestion)`."
434-
-- Store the syntax (not the evaluated Selector) for persistence
435-
modifyEnv fun env => librarySuggestionsExt.addEntry env selector
427+
-- Generate a fresh name for the selector definition
428+
let name ← liftMacroM <| Macro.addMacroScope `_librarySuggestions
429+
-- Elaborate the definition with the library_suggestions attribute
430+
-- Note: @[expose] public, to ensure visibility across module boundaries
431+
-- Use fully qualified `Lean.LibrarySuggestions.Selector` for module compatibility
432+
elabCommand (← `(@[expose, library_suggestions] public def $(mkIdent name) : Lean.LibrarySuggestions.Selector := $selector))
436433
| _ => throwUnsupportedSyntax
437434

438435
open Lean.Elab.Tactic in

‎src/Lean/LibrarySuggestions/Default.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,8 @@ Authors: Kim Morrison
66
module
77

88
prelude
9+
public import Lean.LibrarySuggestions.Basic
10+
public import Lean.LibrarySuggestions.SineQuaNon
911
import all Lean.LibrarySuggestions.SineQuaNon
1012

1113
/-!

‎tests/lean/run/library_suggestions.lean‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,6 @@ has type
88
of sort `Type 1` but is expected to have type
99
Lean.LibrarySuggestions.Selector
1010
of sort `Type`
11-
---
12-
error: Failed to elaborate Nat as a `MVarId → Config → MetaM (Array Suggestion)`.
1311
-/
1412
#guard_msgs in
1513
set_library_suggestions Nat

‎tests/lean/run/library_suggestions_persistent.lean‎

Lines changed: 38 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -1,47 +1,45 @@
1-
import Lean.LibrarySuggestions
2-
import Lean.Meta.Basic
1+
-- This will be restored after an update-stage0
2+
-- import Lean.LibrarySuggestions
3+
-- import Lean.Meta.Basic
34

4-
/-!
5-
# Test that library suggestions persist across file boundaries
5+
-- /-!
6+
-- # Test that library suggestions persist across file boundaries
67

7-
This test verifies that the default library suggestion engine set in
8-
`Lean.LibrarySuggestions.Default` is correctly persisted when imported via `Lean.LibrarySuggestions`.
8+
-- This test verifies that the default library suggestion engine set in
9+
-- `Lean.LibrarySuggestions.Default` is correctly persisted when imported via `Lean.LibrarySuggestions`.
910

10-
We do NOT call `set_library_suggestions` in this file - the selector should
11-
already be set from importing Lean.LibrarySuggestions (which imports Default).
12-
-/
11+
-- We do NOT call `set_library_suggestions` in this file - the selector should
12+
-- already be set from importing Lean.LibrarySuggestions (which imports Default).
13+
-- -/
1314

14-
/--
15-
info: ✓ Selector found in imported state: (Term.open
16-
"open"
17-
(Command.openSimple [`Lean.LibrarySuggestions])
18-
"in"
19-
(Term.app `sineQuaNonSelector.filterGrindAnnotated.intersperse [`currentFile]))
20-
---
21-
info: ✓ Successfully retrieved selector using getSelector!
22-
-/
23-
#guard_msgs in
24-
open Lean Lean.LibrarySuggestions in
25-
run_cmd do
26-
let stx? := librarySuggestionsExt.getState (← getEnv)
27-
match stx? with
28-
| none => Lean.logInfo "❌ No selector found in imported state!"
29-
| some stx =>
30-
Lean.logInfo s!"✓ Selector found in imported state: {stx}"
31-
-- Try to retrieve the selector using getSelector
32-
Elab.Command.liftTermElabM do
33-
let selector? ← getSelector
34-
match selector? with
35-
| none => Lean.logInfo " ❌ getSelector returned none"
36-
| some _ => Lean.logInfo " ✓ Successfully retrieved selector using getSelector!"
15+
-- /--
16+
-- info: ✓ Selector registered in imported state
17+
-- ---
18+
-- info: ✓ getSelector succeeded
19+
-- -/
20+
-- #guard_msgs in
21+
-- open Lean Lean.LibrarySuggestions in
22+
-- run_cmd do
23+
-- -- Check if a selector is registered
24+
-- let hasSelector := (librarySuggestionsExt.getState (← getEnv)).isSome
25+
-- if hasSelector then
26+
-- Lean.logInfo "✓ Selector registered in imported state"
27+
-- -- Try to retrieve the selector using getSelector
28+
-- Elab.Command.liftTermElabM do
29+
-- let selector? ← getSelector
30+
-- match selector? with
31+
-- | none => Lean.logInfo " ❌ getSelector returned none"
32+
-- | some _ => Lean.logInfo " ✓ getSelector succeeded"
33+
-- else
34+
-- Lean.logInfo "❌ No selector registered in imported state!"
3735

38-
-- These examples should work with grind +suggestions but not grind alone
39-
-- (proving that the suggestions engine is active and helping)
36+
-- -- These examples should work with grind +suggestions but not grind alone
37+
-- -- (proving that the suggestions engine is active and helping)
4038

41-
example {x : Dyadic} {prec : Int} : x.roundDown prec ≤ x := by
42-
fail_if_success grind
43-
grind +suggestions
39+
-- example {x : Dyadic} {prec : Int} : x.roundDown prec ≤ x := by
40+
-- fail_if_success grind
41+
-- grind +suggestions
4442

45-
example {x : Dyadic} {prec : Int} : (x.roundUp prec).precision ≤ some prec := by
46-
fail_if_success grind
47-
grind +suggestions
43+
-- example {x : Dyadic} {prec : Int} : (x.roundUp prec).precision ≤ some prec := by
44+
-- fail_if_success grind
45+
-- grind +suggestions

‎tests/lean/run/library_suggestions_persistent_module.lean‎

Lines changed: 32 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -1,36 +1,36 @@
1-
module
2-
import Lean
1+
-- This will be restored after an update-stage0
2+
-- -- It's critical that this test remains a `module`:
3+
-- -- its purpose is to test the availability of the selector in modules.
4+
-- module
5+
-- import Lean
36

4-
/-!
5-
# Test that library suggestions persist across file boundaries
7+
-- /-!
8+
-- # Test that library suggestions persist across file boundaries
69

7-
This test verifies that the default library suggestion engine set in
8-
`Lean.LibrarySuggestions.Default` is correctly persisted when imported via `Lean.LibrarySuggestions`.
10+
-- This test verifies that the default library suggestion engine set in
11+
-- `Lean.LibrarySuggestions.Default` is correctly persisted when imported via `Lean.LibrarySuggestions`.
912

10-
We do NOT call `set_library_suggestions` in this file - the selector should
11-
already be set from importing Lean.LibrarySuggestions (which imports Default).
12-
-/
13+
-- We do NOT call `set_library_suggestions` in this file - the selector should
14+
-- already be set from importing Lean.LibrarySuggestions (which imports Default).
15+
-- -/
1316

14-
/--
15-
info: ✓ Selector found in imported state: (Term.open
16-
"open"
17-
(Command.openSimple [`Lean.LibrarySuggestions])
18-
"in"
19-
(Term.app `sineQuaNonSelector.filterGrindAnnotated.intersperse [`currentFile]))
20-
---
21-
info: ✓ Successfully retrieved selector using getSelector!
22-
-/
23-
#guard_msgs in
24-
open Lean Lean.LibrarySuggestions in
25-
run_cmd do
26-
let stx? := librarySuggestionsExt.getState (← getEnv)
27-
match stx? with
28-
| none => Lean.logInfo "❌ No selector found in imported state!"
29-
| some stx =>
30-
Lean.logInfo s!"✓ Selector found in imported state: {stx}"
31-
-- Try to retrieve the selector using getSelector
32-
Elab.Command.liftTermElabM do
33-
let selector? ← getSelector
34-
match selector? with
35-
| none => Lean.logInfo " ❌ getSelector returned none"
36-
| some _ => Lean.logInfo " ✓ Successfully retrieved selector using getSelector!"
17+
-- /--
18+
-- info: ✓ Selector registered in imported state
19+
-- ---
20+
-- info: ✓ getSelector succeeded
21+
-- -/
22+
-- #guard_msgs in
23+
-- open Lean Lean.LibrarySuggestions in
24+
-- run_cmd do
25+
-- -- Check if a selector is registered
26+
-- let hasSelector := (librarySuggestionsExt.getState (← getEnv)).isSome
27+
-- if hasSelector then
28+
-- Lean.logInfo "✓ Selector registered in imported state"
29+
-- -- Try to retrieve the selector using getSelector
30+
-- Elab.Command.liftTermElabM do
31+
-- let selector? ← getSelector
32+
-- match selector? with
33+
-- | none => Lean.logInfo " ❌ getSelector returned none"
34+
-- | some _ => Lean.logInfo " ✓ getSelector succeeded"
35+
-- else
36+
-- Lean.logInfo "❌ No selector registered in imported state!"

‎tests/lean/run/library_suggestions_sine_qua_non.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
11
module
2+
public import Lean.LibrarySuggestions.Basic
3+
public import Lean.LibrarySuggestions.SineQuaNon
24
import all Lean.LibrarySuggestions.SineQuaNon
35
import Lean.Meta.Basic
46
import Std.Data.ExtHashMap

0 commit comments

Comments
 (0)