chore: merge master

Author: fgdorais

.github/workflows/pr-title.yml

@@ -15,6 +15,6 @@ jobs:
           script: |
             const msg = context.payload.pull_request? context.payload.pull_request.title : context.payload.merge_group.head_commit.message;
             console.log(`Message: ${msg}`)
-            if (!/^(feat|fix|doc|style|refactor|test|chore|perf): .*[^.]($|\n\n)/.test(msg)) {
+            if (!/^(feat|fix|doc|style|refactor|test|chore|perf): (?![A-Z][a-z]).*[^.]($|\n\n)/.test(msg)) {
               core.setFailed('PR title does not follow the Commit Convention (https://leanprover.github.io/lean4/doc/dev/commit_convention.html).');
             }

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,35 +77,35 @@ 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)
     match attr with
     | .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,6 +200,21 @@ def setGrindParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `ta
 def getGrindParams (stx : TSyntax `tactic) : Array Syntax :=
   stx.raw[grindParamsPos][1].getSepArgs
 
+/-- 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 +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 == `suggestions)
+        | none => true
+      | none => true
+    | none => true
+  ⟨config.raw.setArgs filteredItems⟩
+
 def mkGrindOnly
     (config : TSyntax ``Lean.Parser.Tactic.optConfig)
     (trace : Grind.Trace)
@@ -217,7 +231,8 @@ def mkGrindOnly
       else
         let param ← Grind.globalDeclToGrindParamSyntax declName kind minIndexable
         params := params.push param
-  let result ← `(tactic| grind $config:optConfig only)
+  let filteredConfig := filterSuggestionsFromConfig config
+  let result ← `(tactic| grind $filteredConfig:optConfig only)
   return setGrindParams result params
 
 private def elabGrindConfig' (config : TSyntax ``Lean.Parser.Tactic.optConfig) (interactive : Bool) : TacticM Grind.Config := do

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/PremiseSelection.lean src/Lean/LibrarySuggestions.leansrc/Lean/PremiseSelection.lean renamed to 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/PremiseSelection/Basic.lean src/Lean/LibrarySuggestions/Basic.leansrc/Lean/PremiseSelection/Basic.lean renamed to 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,68 @@ 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) ←
+/-- A library suggestion engine that returns locally defined theorems (those in the current file). -/
+def currentFile : Selector := fun _ cfg => do
+  let env ← getEnv
+  let max := cfg.maxSuggestions
+  -- Use map₂ from the staged map, which contains locally defined constants
+  let mut suggestions := #[]
+  for (name, ci) in env.constants.map₂.toList do
+    if suggestions.size >= max then
+      break
+    if isDeniedPremise env name then
+      continue
+    match ci with
+    | .thmInfo _ => suggestions := suggestions.push { name := name, score := 1.0 }
+    | _ => continue
+  return suggestions
+
+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/PremiseSelection/MePo.lean src/Lean/LibrarySuggestions/MePo.leansrc/Lean/PremiseSelection/MePo.lean renamed to 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