diff --git a/src/Lean/LibrarySuggestions.lean b/src/Lean/LibrarySuggestions.lean index fcdeec0a39..fab52b4eb6 100644 --- a/src/Lean/LibrarySuggestions.lean +++ b/src/Lean/LibrarySuggestions.lean @@ -6,8 +6,8 @@ Authors: Kim Morrison module prelude -import Lean.LibrarySuggestions.Basic +public import Lean.LibrarySuggestions.Basic import Lean.LibrarySuggestions.SymbolFrequency import Lean.LibrarySuggestions.MePo -import Lean.LibrarySuggestions.SineQuaNon -import Lean.LibrarySuggestions.Default +public import Lean.LibrarySuggestions.SineQuaNon +public import Lean.LibrarySuggestions.Default diff --git a/tests/lean/run/library_suggestions_persistent.lean b/tests/lean/run/library_suggestions_persistent.lean index de8db28d43..16ecb38e91 100644 --- a/tests/lean/run/library_suggestions_persistent.lean +++ b/tests/lean/run/library_suggestions_persistent.lean @@ -1,6 +1,5 @@ import Lean.LibrarySuggestions import Lean.Meta.Basic -import Std.Data.ExtHashMap /-! # Test that library suggestions persist across file boundaries diff --git a/tests/lean/run/library_suggestions_persistent_module.lean b/tests/lean/run/library_suggestions_persistent_module.lean new file mode 100644 index 0000000000..2dbabeb429 --- /dev/null +++ b/tests/lean/run/library_suggestions_persistent_module.lean @@ -0,0 +1,36 @@ +module +import Lean + +/-! +# 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!"