Skip to content

Commit a0c8404

Browse files
kim-emclaude
andauthored
fix: improve "no library suggestions engine registered" error message (#11464)
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 <[email protected]>
1 parent c0d5b9b commit a0c8404

File tree

2 files changed

+3
-4
lines changed

2 files changed

+3
-4
lines changed

src/Lean/LibrarySuggestions/Basic.lean

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -403,9 +403,8 @@ opaque getSelector : MetaM (Option Selector)
403403
def select (m : MVarId) (c : Config := {}) : MetaM (Array Suggestion) := do
404404
let some selector ← getSelector |
405405
throwError "No library suggestions engine registered. \
406-
(Note that Lean does not provide a default library suggestions engine, \
407-
these must be provided by a downstream library, \
408-
and configured using `set_library_suggestions`.)"
406+
(Add `import Lean.LibrarySuggestions.Default` to use Lean's built-in engine, \
407+
or use `set_library_suggestions` to configure a custom one.)"
409408
selector m c
410409

411410
/-!

tests/lean/run/grind_suggestions.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
import Lean.LibrarySuggestions.Basic
22

33
/--
4-
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`.)
4+
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.)
55
-/
66
#guard_msgs in
77
example : True := by

0 commit comments

Comments
 (0)