From 0db89d65b27b56ea911add501cf041dfc44976a1 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Fri, 31 Oct 2025 15:07:49 +1100
Subject: [PATCH] chore: use 'library suggestions' rather than 'premise
 selection' (#11029)

This PR changes the terminology used from "premise selection" to
"library suggestions". This will be more understandable to users (we
don't assume anyone is familiar with the premise selection literature),
and avoids a conflict with the existing use of "premise" in Lean
terminology (e.g. "major premise" in induction, as well as generally the
synonym for "hypothesis"/"argument").
---
 src/Init/Grind/Config.lean                    |  6 +-
 src/Init/Notation.lean                        |  8 +--
 src/Init/Tactics.lean                         |  5 +-
 src/Lean.lean                                 |  2 +-
 src/Lean/Elab/Tactic/Grind/Main.lean          | 39 ++++++------
 src/Lean/Elab/Tactic/Try.lean                 |  2 +-
 ...Selection.lean => LibrarySuggestions.lean} |  8 +--
 .../Basic.lean                                | 59 ++++++++++---------
 .../MePo.lean                                 |  6 +-
 .../SineQuaNon.lean                           |  8 +--
 .../SymbolFrequency.lean                      |  4 +-
 .../run/grind_question_mark_premises.lean     | 12 ----
 .../run/grind_question_mark_suggestions.lean  | 12 ++++
 ...d_premises.lean => grind_suggestions.lean} | 22 +++----
 tests/lean/run/library_suggestions.lean       | 39 ++++++++++++
 .../lean/run/library_suggestions_import.lean  |  5 ++
 tests/lean/run/library_suggestions_mepo.lean  | 21 +++++++
 ... => library_suggestions_sine_qua_non.lean} | 10 ++--
 tests/lean/run/premise_selection.lean         | 39 ------------
 tests/lean/run/premise_selection_import.lean  |  5 --
 tests/lean/run/premise_selection_mepo.lean    | 21 -------
 tests/lean/run/symbolFrequency.lean           |  4 +-
 .../symbolFrequency_foldRelevantConsts.lean   |  4 +-
 23 files changed, 171 insertions(+), 170 deletions(-)
 rename src/Lean/{PremiseSelection.lean => LibrarySuggestions.lean} (50%)
 rename src/Lean/{PremiseSelection => LibrarySuggestions}/Basic.lean (83%)
 rename src/Lean/{PremiseSelection => LibrarySuggestions}/MePo.lean (96%)
 rename src/Lean/{PremiseSelection => LibrarySuggestions}/SineQuaNon.lean (98%)
 rename src/Lean/{PremiseSelection => LibrarySuggestions}/SymbolFrequency.lean (98%)
 delete mode 100644 tests/lean/run/grind_question_mark_premises.lean
 create mode 100644 tests/lean/run/grind_question_mark_suggestions.lean
 rename tests/lean/run/{grind_premises.lean => grind_suggestions.lean} (54%)
 create mode 100644 tests/lean/run/library_suggestions.lean
 create mode 100644 tests/lean/run/library_suggestions_import.lean
 create mode 100644 tests/lean/run/library_suggestions_mepo.lean
 rename tests/lean/run/{premise_selection_sine_qua_non.lean => library_suggestions_sine_qua_non.lean} (84%)
 delete mode 100644 tests/lean/run/premise_selection.lean
 delete mode 100644 tests/lean/run/premise_selection_import.lean
 delete mode 100644 tests/lean/run/premise_selection_mepo.lean

diff --git a/src/Init/Grind/Config.lean b/src/Init/Grind/Config.lean
index 4cd548c995..f540dcde4e 100644
--- a/src/Init/Grind/Config.lean
+++ b/src/Init/Grind/Config.lean
@@ -18,9 +18,9 @@ structure Config where
   /-- If `lax` is `true`, `grind` will silently ignore any parameters referring to non-existent theorems
   or for which no patterns can be generated. -/
   lax : Bool := false
-  /-- If `premises` is `true`, `grind` will invoke the currently configured premise selecor on the current goal,
-  and add attempt to use the resulting suggestions as premises to the `grind` tactic. -/
-  premises : Bool := false
+  /-- If `suggestions` is `true`, `grind` will invoke the currently configured library suggestion engine on the current goal,
+  and add attempt to use the resulting suggestions as additional parameters to the `grind` tactic. -/
+  suggestions : Bool := false
   /-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
   splits : Nat := 9
   /-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 504b1ede61..1d9b67e751 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -863,12 +863,12 @@ syntax (name := infoTreesCmd)
   "#info_trees" " in" ppLine command : command
 
 /--
-Specify a premise selection engine.
-Note that Lean does not ship a default premise selection engine,
+Specify a library suggestion engine.
+Note that Lean does not ship a default library suggestion engine,
 so this is only useful in conjunction with a downstream package which provides one.
 -/
-syntax (name := setPremiseSelectorCmd)
-  "set_premise_selector" term : command
+syntax (name := setLibrarySuggestionsCmd)
+  "set_library_suggestions" term : command
 
 namespace Parser
 
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index a652186103..04013cd5e3 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -1759,11 +1759,12 @@ as well as tactics such as `next`, `case`, and `rename_i`.
 syntax (name := exposeNames) "expose_names" : tactic
 
 /--
-`#suggest_premises` will suggest premises for the current goal, using the currently registered premise selector.
+`#suggestions` will suggest relevant theorems from the library for the current goal,
+using the currently registered library suggestion engine.
 
 The suggestions are printed in the order of their confidence, from highest to lowest.
 -/
-syntax (name := suggestPremises) "suggest_premises" : tactic
+syntax (name := suggestions) "suggestions" : tactic
 
 /--
 Close fixed-width `BitVec` and `Bool` goals by obtaining a proof from an external SAT solver and
diff --git a/src/Lean.lean b/src/Lean.lean
index bf561cb653..c708d08fb7 100644
--- a/src/Lean.lean
+++ b/src/Lean.lean
@@ -40,7 +40,7 @@ public import Lean.LabelAttribute
 public import Lean.AddDecl
 public import Lean.Replay
 public import Lean.PrivateName
-public import Lean.PremiseSelection
+public import Lean.LibrarySuggestions
 public import Lean.Namespace
 public import Lean.EnvExtension
 public import Lean.ErrorExplanation
diff --git a/src/Lean/Elab/Tactic/Grind/Main.lean b/src/Lean/Elab/Tactic/Grind/Main.lean
index a252093241..cceb049932 100644
--- a/src/Lean/Elab/Tactic/Grind/Main.lean
+++ b/src/Lean/Elab/Tactic/Grind/Main.lean
@@ -9,7 +9,7 @@ public import Lean.Meta.Tactic.Grind.Main
 public import Lean.Meta.Tactic.TryThis
 public import Lean.Elab.Command
 public import Lean.Elab.Tactic.Config
-public import Lean.PremiseSelection.Basic
+public import Lean.LibrarySuggestions.Basic
 import Lean.Meta.Tactic.Grind.SimpUtil
 import Lean.Meta.Tactic.Grind.EMatchTheoremParam
 import Lean.Elab.Tactic.Grind.Basic
@@ -77,11 +77,11 @@ private def parseModifier (s : String) : CoreM Grind.AttrKind := do
   | .ok stx => Grind.getAttrKindCore stx
   | _ => throwError "unexpected modifier {s}"
 
-open PremiseSelection in
-def elabGrindPremises
-    (params : Grind.Params) (premises : Array Suggestion := #[]) : MetaM Grind.Params := do
+open LibrarySuggestions in
+def elabGrindSuggestions
+    (params : Grind.Params) (suggestions : Array Suggestion := #[]) : MetaM Grind.Params := do
   let mut params := params
-  for p in premises do
+  for p in suggestions do
     let attr ← match p.flag with
     | some flag => parseModifier flag
     | none => pure <| .ematch (.default false)
@@ -89,23 +89,23 @@ def elabGrindPremises
     | .ematch kind =>
       try
         params ← addEMatchTheorem params (mkIdent p.name) p.name kind false (warn := false)
-      catch _ => pure () -- Don't worry if premise suggestion gave bad suggestions.
+      catch _ => pure () -- Don't worry if library suggestions gave bad theorems.
     | _ =>
       -- We could actually support arbitrary grind modifiers,
       -- and call `processParam` rather than `addEMatchTheorem`,
       -- but this would require a larger refactor.
-      -- Let's only do this if there is a prospect of a premise selector supporting this.
+      -- Let's only do this if there is a prospect of a library suggestion engine supporting this.
       throwError "unexpected modifier {p.flag}"
   return params
 
-open PremiseSelection in
-def elabGrindParamsAndPremises
+open LibrarySuggestions in
+def elabGrindParamsAndSuggestions
     (params : Grind.Params)
     (ps : TSyntaxArray ``Parser.Tactic.grindParam)
-    (premises : Array Suggestion := #[])
+    (suggestions : Array Suggestion := #[])
     (only : Bool) (lax : Bool := false) : MetaM Grind.Params := do
   let params ← elabGrindParams params ps (lax := lax) (only := only)
-  elabGrindPremises params premises
+  elabGrindSuggestions params suggestions
 
 def mkGrindParams
     (config : Grind.Config) (only : Bool) (ps : TSyntaxArray ``Parser.Tactic.grindParam) (mvarId : MVarId) :
@@ -119,12 +119,11 @@ def mkGrindParams
   -/
   let casesTypes ← Grind.getCasesTypes
   let params := { params with ematch, casesTypes, inj }
-  let premises ← if config.premises then
-    let suggestions ← PremiseSelection.select mvarId
-    pure suggestions
+  let suggestions ← if config.suggestions then
+    LibrarySuggestions.select mvarId
   else
     pure #[]
-  let params ← elabGrindParamsAndPremises params ps premises (only := only) (lax := config.lax)
+  let params ← elabGrindParamsAndSuggestions params ps suggestions (only := only) (lax := config.lax)
   trace[grind.debug.inj] "{params.inj.getOrigins.map (·.pp)}"
   return params
 
@@ -201,16 +200,16 @@ def setGrindParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `ta
 def getGrindParams (stx : TSyntax `tactic) : Array Syntax :=
   stx.raw[grindParamsPos][1].getSepArgs
 
-/-- Filter out `+premises` from the config syntax -/
-def filterPremisesFromConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig) : TSyntax ``Lean.Parser.Tactic.optConfig :=
+/-- Filter out `+suggestions` from the config syntax -/
+def filterSuggestionsFromConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig) : TSyntax ``Lean.Parser.Tactic.optConfig :=
   let configItems := config.raw.getArgs
   let filteredItems := configItems.filter fun item =>
-    -- Keep all items except +premises
+    -- Keep all items except +suggestions
     -- Structure: null node -> configItem -> posConfigItem -> ["+", ident]
     match item[0]? with
     | some configItem => match configItem[0]? with
       | some posConfigItem => match posConfigItem[1]? with
-        | some ident => !(posConfigItem.getKind == ``Lean.Parser.Tactic.posConfigItem && ident.getId == `premises)
+        | some ident => !(posConfigItem.getKind == ``Lean.Parser.Tactic.posConfigItem && ident.getId == `suggestions)
         | none => true
       | none => true
     | none => true
@@ -232,7 +231,7 @@ def mkGrindOnly
       else
         let param ← Grind.globalDeclToGrindParamSyntax declName kind minIndexable
         params := params.push param
-  let filteredConfig := filterPremisesFromConfig config
+  let filteredConfig := filterSuggestionsFromConfig config
   let result ← `(tactic| grind $filteredConfig:optConfig only)
   return setGrindParams result params
 
diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean
index 6cc667778e..d73715be31 100644
--- a/src/Lean/Elab/Tactic/Try.lean
+++ b/src/Lean/Elab/Tactic/Try.lean
@@ -673,7 +673,7 @@ private def mkTryEvalSuggestStx (info : Try.Info) : MetaM (TSyntax `tactic) := d
 
 -- TODO: vanilla `induction`.
 -- TODO: make it extensible.
--- TODO: premise selection.
+-- TODO: library suggestions.
 
 @[builtin_tactic Lean.Parser.Tactic.tryTrace] def evalTryTrace : Tactic := fun stx => do
   match stx with
diff --git a/src/Lean/PremiseSelection.lean b/src/Lean/LibrarySuggestions.lean
similarity index 50%
rename from src/Lean/PremiseSelection.lean
rename to src/Lean/LibrarySuggestions.lean
index bc6af08a22..d187fb9d27 100644
--- a/src/Lean/PremiseSelection.lean
+++ b/src/Lean/LibrarySuggestions.lean
@@ -6,7 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-import Lean.PremiseSelection.Basic
-import Lean.PremiseSelection.SymbolFrequency
-import Lean.PremiseSelection.MePo
-import Lean.PremiseSelection.SineQuaNon
+import Lean.LibrarySuggestions.Basic
+import Lean.LibrarySuggestions.SymbolFrequency
+import Lean.LibrarySuggestions.MePo
+import Lean.LibrarySuggestions.SineQuaNon
diff --git a/src/Lean/PremiseSelection/Basic.lean b/src/Lean/LibrarySuggestions/Basic.lean
similarity index 83%
rename from src/Lean/PremiseSelection/Basic.lean
rename to src/Lean/LibrarySuggestions/Basic.lean
index 5efeeef304..c6dcc493fa 100644
--- a/src/Lean/PremiseSelection/Basic.lean
+++ b/src/Lean/LibrarySuggestions/Basic.lean
@@ -12,19 +12,20 @@ public import Lean.Meta.CompletionName
 public import Init.Data.Random
 
 /-!
-# An API for premise selection algorithms.
+# An API for library suggestion algorithms.
 
-This module provides a basic API for premise selection algorithms,
-which are used to suggest identifiers that should be introduced in a proof.
+This module provides a basic API for library suggestion algorithms,
+which are used to suggest relevant theorems from the library for the current goal.
+In the literature this is usually known as "premise selection",
+but we mostly avoid that term as most of our users will not be familiar with the term.
 
 The core interface is the `Selector` type, which is a function from a metavariable
 and a configuration to a list of suggestions.
+The `Selector` is registered as an environment extension,
+and the trivial (no suggestions) implementation is `Lean.LibrarySuggestions.empty`.
 
-The `Selector` is registered as an environment extension, and the trivial (no suggestions) implementation
-is `Lean.PremiseSelection.empty`.
-
-Lean does not provide a default premise selector, so this module is intended to be used in conjunction
-with a downstream package which registers a premise selector.
+Lean does not provide a default library suggestion engine, so this module is intended to be used in conjunction
+with a downstream package which registers a library suggestion engine.
 -/
 
 namespace Lean.Expr.FoldRelevantConstantsImpl
@@ -113,7 +114,7 @@ public def Lean.MVarId.getRelevantConstants (g : MVarId) : MetaM NameSet := with
 
 @[expose] public section
 
-namespace Lean.PremiseSelection
+namespace Lean.LibrarySuggestions
 
 /--
 A `Suggestion` is essentially just an identifier and a confidence score that the identifier is relevant.
@@ -285,52 +286,52 @@ def random (gen : StdGen := ⟨37, 59⟩) : Selector := fun _ cfg => do
       suggestions := suggestions.push { name := name, score := 1.0 / consts.size.toFloat }
   return suggestions
 
-builtin_initialize premiseSelectorExt : EnvExtension (Option Selector) ←
+builtin_initialize librarySuggestionsExt : EnvExtension (Option Selector) ←
   registerEnvExtension (pure none)
 
-/-- Generate premise suggestions for the given metavariable, using the currently registered premise selector. -/
+/-- Generate library suggestions for the given metavariable, using the currently registered library suggestions engine. -/
 def select (m : MVarId) (c : Config := {}) : MetaM (Array Suggestion) := do
-  let some selector := premiseSelectorExt.getState (← getEnv) |
-    throwError "No premise selector registered. \
-      (Note that Lean does not provide a default premise selector, \
+  let some selector := librarySuggestionsExt.getState (← getEnv) |
+    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_premise_selector`.)"
+      and configured using `set_library_suggestions`.)"
   selector m c
 
 /-!
 Currently the registration mechanism is just global state.
-This means that if multiple modules register premise selectors,
+This means that if multiple modules register library suggestions engines,
 the behaviour will be dependent on the order of loading modules.
 
 We should replace this with a mechanism so that
-premise selectors are configured via options in the `lakefile`, and
+library suggestions engines are configured via options in the `lakefile`, and
 commands are only used to override in a single declaration or file.
 -/
 
-/-- Set the current premise selector.-/
-def registerPremiseSelector (selector : Selector) : CoreM Unit := do
-  modifyEnv fun env => premiseSelectorExt.setState env (some selector)
+/-- Set the current library suggestions engine.-/
+def registerLibrarySuggestions (selector : Selector) : CoreM Unit := do
+  modifyEnv fun env => librarySuggestionsExt.setState env (some selector)
 
 open Lean Elab Command in
-@[builtin_command_elab setPremiseSelectorCmd, inherit_doc setPremiseSelectorCmd]
-def elabSetPremiseSelector : CommandElab
-  | `(command| set_premise_selector $selector) => do
-    if `Lean.PremiseSelection.Basic ∉ (← getEnv).header.moduleNames then
-      logWarning "Add `import Lean.PremiseSelection.Basic` before using the `set_premise_selector` command."
+@[builtin_command_elab setLibrarySuggestionsCmd, inherit_doc setLibrarySuggestionsCmd]
+def elabSetLibrarySuggestions : CommandElab
+  | `(command| set_library_suggestions $selector) => do
+    if `Lean.LibrarySuggestions.Basic ∉ (← getEnv).header.moduleNames then
+      logWarning "Add `import Lean.LibrarySuggestions.Basic` before using the `set_library_suggestions` command."
     let selector ← liftTermElabM do
       try
         let selectorTerm ← Term.elabTermEnsuringType selector (some (Expr.const ``Selector []))
         unsafe Meta.evalExpr Selector (Expr.const ``Selector []) selectorTerm
       catch _ =>
         throwError "Failed to elaborate {selector} as a `MVarId → Config → MetaM (Array Suggestion)`."
-    liftCoreM (registerPremiseSelector selector)
+    liftCoreM (registerLibrarySuggestions selector)
   | _ => throwUnsupportedSyntax
 
 open Lean.Elab.Tactic in
-@[builtin_tactic Lean.Parser.Tactic.suggestPremises] def evalSuggestPremises : Tactic := fun _ =>
+@[builtin_tactic Lean.Parser.Tactic.suggestions] def evalSuggestions : Tactic := fun _ =>
   liftMetaTactic1 fun mvarId => do
     let suggestions ← select mvarId
-    logInfo m!"Premise suggestions: {suggestions.map (·.name)}"
+    logInfo m!"Library suggestions: {suggestions.map (·.name)}"
     return mvarId
 
-end Lean.PremiseSelection
+end Lean.LibrarySuggestions
diff --git a/src/Lean/PremiseSelection/MePo.lean b/src/Lean/LibrarySuggestions/MePo.lean
similarity index 96%
rename from src/Lean/PremiseSelection/MePo.lean
rename to src/Lean/LibrarySuggestions/MePo.lean
index 531afca6ab..d4ad7859ec 100644
--- a/src/Lean/PremiseSelection/MePo.lean
+++ b/src/Lean/LibrarySuggestions/MePo.lean
@@ -6,8 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Lean.PremiseSelection.Basic
-import Lean.PremiseSelection.SymbolFrequency
+public import Lean.LibrarySuggestions.Basic
+import Lean.LibrarySuggestions.SymbolFrequency
 import Lean.Meta.Basic
 
 /-!
@@ -21,7 +21,7 @@ It needs to be tuned and evaluated for Lean.
 
 open Lean
 
-namespace Lean.PremiseSelection.MePo
+namespace Lean.LibrarySuggestions.MePo
 
 builtin_initialize registerTraceClass `mepo
 
diff --git a/src/Lean/PremiseSelection/SineQuaNon.lean b/src/Lean/LibrarySuggestions/SineQuaNon.lean
similarity index 98%
rename from src/Lean/PremiseSelection/SineQuaNon.lean
rename to src/Lean/LibrarySuggestions/SineQuaNon.lean
index a8ca7521da..9100abcde2 100644
--- a/src/Lean/PremiseSelection/SineQuaNon.lean
+++ b/src/Lean/LibrarySuggestions/SineQuaNon.lean
@@ -9,8 +9,8 @@ prelude
 public import Lean.CoreM
 public import Lean.Meta.Basic
 import Lean.Meta.Instances
-import Lean.PremiseSelection.SymbolFrequency
-public import Lean.PremiseSelection.Basic
+import Lean.LibrarySuggestions.SymbolFrequency
+public import Lean.LibrarySuggestions.Basic
 
 /-!
 # Sine Qua Non premise selection
@@ -21,7 +21,7 @@ This is an implementation of the "Sine Qua Non" premise selection algorithm, fro
 It needs to be tuned and evaluated for Lean.
 -/
 
-namespace Lean.PremiseSelection.SineQuaNon
+namespace Lean.LibrarySuggestions.SineQuaNon
 
 builtin_initialize registerTraceClass `sineQuaNon
 
@@ -193,4 +193,4 @@ public def sineQuaNonSelector (depthFactor : Float := 1.5) : Selector := fun g c
   let suggestions ← sineQuaNon constants config.maxSuggestions depthFactor
   return suggestions.take config.maxSuggestions
 
-end Lean.PremiseSelection
+end Lean.LibrarySuggestions
diff --git a/src/Lean/PremiseSelection/SymbolFrequency.lean b/src/Lean/LibrarySuggestions/SymbolFrequency.lean
similarity index 98%
rename from src/Lean/PremiseSelection/SymbolFrequency.lean
rename to src/Lean/LibrarySuggestions/SymbolFrequency.lean
index 3290c4e359..1b40938066 100644
--- a/src/Lean/PremiseSelection/SymbolFrequency.lean
+++ b/src/Lean/LibrarySuggestions/SymbolFrequency.lean
@@ -11,7 +11,7 @@ public import Lean.Meta.Basic
 import Lean.Meta.InferType
 import Lean.Meta.FunInfo
 import Lean.AddDecl
-import Lean.PremiseSelection.Basic
+import Lean.LibrarySuggestions.Basic
 
 /-!
 # Symbol frequency
@@ -19,7 +19,7 @@ import Lean.PremiseSelection.Basic
 This module provides a persistent environment extension for computing the frequency of symbols in the environment.
 -/
 
-namespace Lean.PremiseSelection
+namespace Lean.LibrarySuggestions
 
 /--
 Collect the frequencies for constants occurring in declarations defined in the current module,
diff --git a/tests/lean/run/grind_question_mark_premises.lean b/tests/lean/run/grind_question_mark_premises.lean
deleted file mode 100644
index a329bf8cd3..0000000000
--- a/tests/lean/run/grind_question_mark_premises.lean
+++ /dev/null
@@ -1,12 +0,0 @@
-import Lean
-
-set_premise_selector Lean.PremiseSelection.sineQuaNonSelector
-
--- Test that grind? +premises does NOT include +premises in its output
-/--
-info: Try this:
-  [apply] grind only
--/
-#guard_msgs in
-example {x y : Nat} (h : x = y) : y = x := by
-  grind? +premises
diff --git a/tests/lean/run/grind_question_mark_suggestions.lean b/tests/lean/run/grind_question_mark_suggestions.lean
new file mode 100644
index 0000000000..9568a6a2ce
--- /dev/null
+++ b/tests/lean/run/grind_question_mark_suggestions.lean
@@ -0,0 +1,12 @@
+import Lean
+
+set_library_suggestions Lean.LibrarySuggestions.sineQuaNonSelector
+
+-- Test that grind? +suggestions does NOT include +suggestions in its output
+/--
+info: Try this:
+  [apply] grind only
+-/
+#guard_msgs in
+example {x y : Nat} (h : x = y) : y = x := by
+  grind? +suggestions
diff --git a/tests/lean/run/grind_premises.lean b/tests/lean/run/grind_suggestions.lean
similarity index 54%
rename from tests/lean/run/grind_premises.lean
rename to tests/lean/run/grind_suggestions.lean
index d623be5ae5..36eb16bdde 100644
--- a/tests/lean/run/grind_premises.lean
+++ b/tests/lean/run/grind_suggestions.lean
@@ -1,17 +1,17 @@
-import Lean.PremiseSelection.Basic
+import Lean.LibrarySuggestions.Basic
 
 /--
-error: No premise selector registered. (Note that Lean does not provide a default premise selector, these must be provided by a downstream library, and configured using `set_premise_selector`.)
+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`.)
 -/
 #guard_msgs in
 example : True := by
-  grind +premises
+  grind +suggestions
 
-set_premise_selector (fun _ _ => pure #[])
+set_library_suggestions (fun _ _ => pure #[])
 
 #guard_msgs in
 example : True := by
-  grind +premises
+  grind +suggestions
 
 def P (_ : Nat) := True
 theorem p : P 7 := trivial
@@ -34,23 +34,23 @@ example : P 37 := by
 example : P 7 := by
   grind [p]
 
-set_premise_selector (fun _ _ => pure #[{ name := `p, score := 1.0 }])
+set_library_suggestions (fun _ _ => pure #[{ name := `p, score := 1.0 }])
 
 example : P 7 := by
-  grind +premises
+  grind +suggestions
 
-set_premise_selector (fun _ _ => pure #[{ name := `List.append_assoc, score := 1.0 }])
+set_library_suggestions (fun _ _ => pure #[{ name := `List.append_assoc, score := 1.0 }])
 
 -- Make sure there is no warning about the redundant theorem.
 #guard_msgs in
 example (x y z : List Nat) : x ++ (y ++ z) = (x ++ y) ++ z := by
-  grind +premises
+  grind +suggestions
 
 theorem f : True := trivial
 
-set_premise_selector (fun _ _ => pure #[{ name := `f, score := 1.0 }])
+set_library_suggestions (fun _ _ => pure #[{ name := `f, score := 1.0 }])
 
 -- Make sure that bad suggestions (e.g. not patterns) from premise selection are dropped silently.
 #guard_msgs in
 example (x y z : List Nat) : x ++ (y ++ z) = (x ++ y) ++ z := by
-  grind +premises
+  grind +suggestions
diff --git a/tests/lean/run/library_suggestions.lean b/tests/lean/run/library_suggestions.lean
new file mode 100644
index 0000000000..e3ab1b5cb6
--- /dev/null
+++ b/tests/lean/run/library_suggestions.lean
@@ -0,0 +1,39 @@
+import Lean.LibrarySuggestions
+
+/--
+error: Type mismatch
+  Nat
+has type
+  Type
+of sort `Type 1` but is expected to have type
+  Lean.LibrarySuggestions.Selector
+of sort `Type`
+---
+error: Failed to elaborate Nat as a `MVarId → Config → MetaM (Array Suggestion)`.
+-/
+#guard_msgs in
+set_library_suggestions Nat
+
+/--
+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`.)
+-/
+#guard_msgs in
+example : True := by
+  suggestions
+  trivial
+
+set_library_suggestions (fun _ _ => pure #[])
+
+/-- info: Library suggestions: [] -/
+#guard_msgs in
+example : True := by
+  suggestions
+  trivial
+
+set_library_suggestions Lean.LibrarySuggestions.random ⟨1,1⟩
+
+-- This would be an extremely fragile test (select 10 random constants!)
+-- so we do not use #guard_msgs.
+example : True := by
+  suggestions
+  trivial
diff --git a/tests/lean/run/library_suggestions_import.lean b/tests/lean/run/library_suggestions_import.lean
new file mode 100644
index 0000000000..8a9e67aa63
--- /dev/null
+++ b/tests/lean/run/library_suggestions_import.lean
@@ -0,0 +1,5 @@
+/--
+warning: Add `import Lean.LibrarySuggestions.Basic` before using the `set_library_suggestions` command.
+-/
+#guard_msgs (warning, drop error) in
+set_library_suggestions (fun _ _ => pure #[])
diff --git a/tests/lean/run/library_suggestions_mepo.lean b/tests/lean/run/library_suggestions_mepo.lean
new file mode 100644
index 0000000000..783096ba55
--- /dev/null
+++ b/tests/lean/run/library_suggestions_mepo.lean
@@ -0,0 +1,21 @@
+import Lean.LibrarySuggestions.MePo
+
+set_library_suggestions Lean.LibrarySuggestions.mepoSelector (useRarity := false)
+
+example (a b : Int) : a + b = b + a := by
+  suggestions
+  sorry
+
+example (x y z : List Int) : x ++ y ++ z = x ++ (y ++ z) := by
+  suggestions
+  sorry
+
+set_library_suggestions Lean.LibrarySuggestions.mepoSelector (useRarity := true)
+
+example (a b : Int) : a + b = b + a := by
+  suggestions
+  sorry
+
+example (x y z : List Int) : x ++ y ++ z = x ++ (y ++ z) := by
+  suggestions
+  sorry
diff --git a/tests/lean/run/premise_selection_sine_qua_non.lean b/tests/lean/run/library_suggestions_sine_qua_non.lean
similarity index 84%
rename from tests/lean/run/premise_selection_sine_qua_non.lean
rename to tests/lean/run/library_suggestions_sine_qua_non.lean
index 6c45d7f271..eb63789a70 100644
--- a/tests/lean/run/premise_selection_sine_qua_non.lean
+++ b/tests/lean/run/library_suggestions_sine_qua_non.lean
@@ -1,19 +1,19 @@
 module
-import all Lean.PremiseSelection.SineQuaNon
+import all Lean.LibrarySuggestions.SineQuaNon
 import Lean.Meta.Basic
 import Std.Data.ExtHashMap
 
-open Lean PremiseSelection SineQuaNon
+open Lean LibrarySuggestions SineQuaNon
 
-set_premise_selector Lean.PremiseSelection.sineQuaNonSelector
+set_library_suggestions Lean.LibrarySuggestions.sineQuaNonSelector
 
 example {x : Dyadic} {prec : Int} : x.roundDown prec ≤ x := by
   fail_if_success grind
-  grind +premises
+  grind +suggestions
 
 example {x : Dyadic} {prec : Int} : (x.roundUp prec).precision ≤ some prec := by
   fail_if_success grind
-  grind +premises
+  grind +suggestions
 
 /-- info: [(HAppend.hAppend, 1.000000)] -/
 #guard_msgs in
diff --git a/tests/lean/run/premise_selection.lean b/tests/lean/run/premise_selection.lean
deleted file mode 100644
index c1e7c4afd5..0000000000
--- a/tests/lean/run/premise_selection.lean
+++ /dev/null
@@ -1,39 +0,0 @@
-import Lean.PremiseSelection
-
-/--
-error: Type mismatch
-  Nat
-has type
-  Type
-of sort `Type 1` but is expected to have type
-  Lean.PremiseSelection.Selector
-of sort `Type`
----
-error: Failed to elaborate Nat as a `MVarId → Config → MetaM (Array Suggestion)`.
--/
-#guard_msgs in
-set_premise_selector Nat
-
-/--
-error: No premise selector registered. (Note that Lean does not provide a default premise selector, these must be provided by a downstream library, and configured using `set_premise_selector`.)
--/
-#guard_msgs in
-example : True := by
-  suggest_premises
-  trivial
-
-set_premise_selector (fun _ _ => pure #[])
-
-/-- info: Premise suggestions: [] -/
-#guard_msgs in
-example : True := by
-  suggest_premises
-  trivial
-
-set_premise_selector Lean.PremiseSelection.random ⟨1,1⟩
-
--- This would be an extremely fragile test (select 10 random constants!)
--- so we do not use #guard_msgs.
-example : True := by
-  suggest_premises
-  trivial
diff --git a/tests/lean/run/premise_selection_import.lean b/tests/lean/run/premise_selection_import.lean
deleted file mode 100644
index 424df7fe8f..0000000000
--- a/tests/lean/run/premise_selection_import.lean
+++ /dev/null
@@ -1,5 +0,0 @@
-/--
-warning: Add `import Lean.PremiseSelection.Basic` before using the `set_premise_selector` command.
--/
-#guard_msgs (warning, drop error) in
-set_premise_selector (fun _ _ => pure #[])
diff --git a/tests/lean/run/premise_selection_mepo.lean b/tests/lean/run/premise_selection_mepo.lean
deleted file mode 100644
index 4eb8ed0cf7..0000000000
--- a/tests/lean/run/premise_selection_mepo.lean
+++ /dev/null
@@ -1,21 +0,0 @@
-import Lean.PremiseSelection.MePo
-
-set_premise_selector Lean.PremiseSelection.mepoSelector (useRarity := false)
-
-example (a b : Int) : a + b = b + a := by
-  suggest_premises
-  sorry
-
-example (x y z : List Int) : x ++ y ++ z = x ++ (y ++ z) := by
-  suggest_premises
-  sorry
-
-set_premise_selector Lean.PremiseSelection.mepoSelector (useRarity := true)
-
-example (a b : Int) : a + b = b + a := by
-  suggest_premises
-  sorry
-
-example (x y z : List Int) : x ++ y ++ z = x ++ (y ++ z) := by
-  suggest_premises
-  sorry
diff --git a/tests/lean/run/symbolFrequency.lean b/tests/lean/run/symbolFrequency.lean
index cf24567383..17794a77ce 100644
--- a/tests/lean/run/symbolFrequency.lean
+++ b/tests/lean/run/symbolFrequency.lean
@@ -1,7 +1,7 @@
 import Lean.Meta.Basic
-import Lean.PremiseSelection.SymbolFrequency
+import Lean.LibrarySuggestions.SymbolFrequency
 
-open Lean PremiseSelection
+open Lean LibrarySuggestions
 
 /-- info: true -/
 #guard_msgs in
diff --git a/tests/lean/run/symbolFrequency_foldRelevantConsts.lean b/tests/lean/run/symbolFrequency_foldRelevantConsts.lean
index c724b32285..c206a6986d 100644
--- a/tests/lean/run/symbolFrequency_foldRelevantConsts.lean
+++ b/tests/lean/run/symbolFrequency_foldRelevantConsts.lean
@@ -1,9 +1,9 @@
 module
 
-import all Lean.PremiseSelection.SymbolFrequency
+import all Lean.LibrarySuggestions.SymbolFrequency
 import all Init.Data.Array.Basic
 
-open Lean PremiseSelection
+open Lean LibrarySuggestions
 
 /-- info: [List, Eq, HAppend.hAppend] -/
 #guard_msgs in