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

@@ -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. -/

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
 

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

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

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
 

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

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

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

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
 

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

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,

tests/lean/run/grind_question_mark_premises.lean

@@ -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

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

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

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

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 #[])

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

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

tests/lean/run/premise_selection.lean

@@ -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

tests/lean/run/premise_selection_import.lean

@@ -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 #[])

tests/lean/run/premise_selection_mepo.lean

@@ -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

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

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