From a0c8404ab87eb8a75b370fe3f1e343b8bd92b843 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Tue, 2 Dec 2025 11:55:46 +1100 Subject: [PATCH] fix: improve "no library suggestions engine registered" error message (#11464) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR improves the error message when no library suggestions engine is registered to recommend importing `Lean.LibrarySuggestions.Default` for the built-in engine. **Before:** ``` No library suggestions engine registered. (Note that Lean does not provide a default library suggestions engine, these must be provided by a downstream library, and configured using `set_library_suggestions`.) ``` **After:** ``` No library suggestions engine registered. (Add `import Lean.LibrarySuggestions.Default` to use Lean's built-in engine, or use `set_library_suggestions` to configure a custom one.) ``` 🤖 Prepared with Claude Code Co-authored-by: Claude --- src/Lean/LibrarySuggestions/Basic.lean | 5 ++--- tests/lean/run/grind_suggestions.lean | 2 +- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/Lean/LibrarySuggestions/Basic.lean b/src/Lean/LibrarySuggestions/Basic.lean index 86de26cfc6..ba8f1820e6 100644 --- a/src/Lean/LibrarySuggestions/Basic.lean +++ b/src/Lean/LibrarySuggestions/Basic.lean @@ -403,9 +403,8 @@ opaque getSelector : MetaM (Option Selector) def select (m : MVarId) (c : Config := {}) : MetaM (Array Suggestion) := do let some selector ← getSelector | throwError "No library suggestions engine registered. \ - (Note that Lean does not provide a default library suggestions engine, \ - these must be provided by a downstream library, \ - and configured using `set_library_suggestions`.)" + (Add `import Lean.LibrarySuggestions.Default` to use Lean's built-in engine, \ + or use `set_library_suggestions` to configure a custom one.)" selector m c /-! diff --git a/tests/lean/run/grind_suggestions.lean b/tests/lean/run/grind_suggestions.lean index 8bd0c05c50..133e08586b 100644 --- a/tests/lean/run/grind_suggestions.lean +++ b/tests/lean/run/grind_suggestions.lean @@ -1,7 +1,7 @@ import Lean.LibrarySuggestions.Basic /-- -error: No library suggestions engine registered. (Note that Lean does not provide a default library suggestions engine, these must be provided by a downstream library, and configured using `set_library_suggestions`.) +error: No library suggestions engine registered. (Add `import Lean.LibrarySuggestions.Default` to use Lean's built-in engine, or use `set_library_suggestions` to configure a custom one.) -/ #guard_msgs in example : True := by