fix: make library suggestions available in module files

This PR makes the library suggestions extension state available when
importing from `module` files.

In a `module` file, non-public imports at deeper transitive levels don't
have their data loaded (to support proper encapsulation in the module
system). Since the library suggestions extension stores and evaluates
syntax that references constants from these modules, both the extension
state and the referenced constants need to be publicly exported.

The fix marks `Basic`, `SineQuaNon`, and `Default` as `public import` in
`Lean.LibrarySuggestions`:
- `Basic` defines the `librarySuggestionsExt` environment extension
- `SineQuaNon` defines `sineQuaNonSelector` referenced in the selector syntax
- `Default` sets the selector using `set_library_suggestions`

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>

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

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

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!"