feat: user extensibility in try? (#11149)

This PR adds a user-extension mechanism for the `try?` tactic. You can
either use the `@[try_suggestion]` attribute on a declaration with
signature ``MVarId -> Try.Info -> MetaM (Array (TSyntax `tactic))`` to
produce suggestions, or the `register_try?_tactic <stx>` command with a
fixed piece of syntax. User-extensions are only tried *after* the
built-in try strategies have been tried and failed.

I wanted to ensure that if the user provides a tactic that produces a
"Try this:" suggestion, we both emit the original tactic and the
suggested replacement (this is what we already do with `grind` and
`simp`). I have this working, but it is quite hacky: we grab the message
log and parse it. I fear this will break when the "Try this:" format is
inevitably changed in the future.


<!-- CURSOR_SUMMARY -->
---

> [!NOTE]
> Adds user-defined suggestion generators for `try?` via
`@[try_suggestion]` and `register_try?_tactic`, executed after built-ins
with priority and double-suggestion handling.
> 
> - **Parser/Command**:
> - Add command syntax `register_try?_tactic (priority := n)?
<tacticSeq>` in `Lean.Parser.Command`.
> - **Suggestion registry**:
> - Introduce `@[try_suggestion (prio)]` attribute with a scoped env
extension to register generators (`MVarId → Try.Info → MetaM (Array
(TSyntax `tactic))`).
>   - Priority ordering (higher first); supports local/global scope.
> - **Tactic engine (`try?`)**:
> - New unsafe pipeline to collect and run user generators after
built-in tactics; expands nested "Try this" outputs from user tactics.
> - `mkTryEvalSuggestStx` now takes `(goal, info)`; integrates user
tactics as fallback via `attempt_all`.
> - Suppress intermediate "Try this" messages during `evalAndSuggest` by
restoring the message log.
> - **Imports**:
>   - Add `meta import Lean.Elab.Command` for command elaboration.
> - **Tests**:
> - `try_register_builtin.lean`: command availability and warning
without import.
> - `try_user_suggestions.lean`: basic, priority, built-in fallback,
double-suggestion, and command registration cases.
> - Update `versoDocMissing.lean.expected.out` to include
`register_try?_tactic` in expected commands.
> 
> <sup>Written by [Cursor
Bugbot](https://cursor.com/dashboard?tab=bugbot) for commit
302dc9454450eb29ad4ea9b01d87ac60365299ad. This will update automatically
on new commits. Configure
[here](https://cursor.com/dashboard?tab=bugbot).</sup>
<!-- /CURSOR_SUMMARY -->

src/Init/Try.lean

@@ -57,3 +57,16 @@ syntax (name := attemptAll) "attempt_all " withPosition((ppDedent(ppLine) colGe
 syntax (name := tryResult) "try_suggestions " tactic* : tactic
 
 end Lean.Parser.Tactic
+
+namespace Lean.Parser.Command
+
+/--
+`register_try?_tactic tac` registers a tactic `tac` as a suggestion generator for the `try?` tactic.
+
+An optional priority can be specified with `register_try?_tactic (priority := 500) tac`.
+Higher priority generators are tried first. The default priority is 1000.
+-/
+syntax (name := registerTryTactic) (docComment)?
+  "register_try?_tactic" ("(" &"priority" ":=" num ")")? tacticSeq : command
+
+end Lean.Parser.Command

src/Lean/Elab/Tactic/Try.lean

@@ -11,6 +11,7 @@ public import Lean.Meta.Tactic.Try
 public import Lean.Elab.Tactic.SimpTrace
 public import Lean.Elab.Tactic.LibrarySearch
 public import Lean.Elab.Tactic.Grind
+meta import Lean.Elab.Command
 
 public section
 
@@ -244,6 +245,115 @@ builtin_initialize tryTacticElabAttribute : KeyedDeclsAttribute TryTactic ← do
 private def getEvalFns (kind : SyntaxNodeKind) : CoreM (List (KeyedDeclsAttribute.AttributeEntry TryTactic)) := do
   return tryTacticElabAttribute.getEntries (← getEnv) kind
 
+/-! User-extensible try suggestion generators -/
+
+/-- A user-defined generator that proposes tactics for `try?` to attempt.
+Takes the goal MVarId and collected info, returns array of tactics to try. -/
+abbrev TrySuggestionGenerator := MVarId → Try.Info → MetaM (Array (TSyntax `tactic))
+
+/-- Entry in the try suggestion registry -/
+structure TrySuggestionEntry where
+  name : Name
+  prio : Nat
+  deriving Inhabited
+
+/-- Environment extension for user try suggestion generators (supports local scoping) -/
+builtin_initialize trySuggestionExtension : SimpleScopedEnvExtension TrySuggestionEntry (Array TrySuggestionEntry) ←
+  registerSimpleScopedEnvExtension {
+    addEntry := fun entries entry =>
+      -- Insert new entry and maintain sorted order by priority (higher = runs first)
+      (entries.push entry).qsort (·.prio > ·.prio)
+    initial := #[]
+  }
+
+/-- Register the @[try_suggestion prio] attribute -/
+builtin_initialize registerBuiltinAttribute {
+  name := `try_suggestion
+  descr := "Register a tactic suggestion generator for try? (runs after built-in tactics)"
+  add := fun declName stx kind => do
+    let prio ← match stx with
+      | `(attr| try_suggestion $n:num) => pure n.getNat
+      | `(attr| try_suggestion) => pure 1000  -- Default priority
+      | _ => throwError "invalid 'try_suggestion' attribute syntax"
+    let attrKind := if kind == AttributeKind.local then AttributeKind.local else AttributeKind.global
+    trySuggestionExtension.add {
+      name := declName,
+      prio := prio
+    } attrKind
+}
+
+/-- Elaborate `register_try?_tactic` command -/
+@[builtin_command_elab registerTryTactic]
+meta def elabRegisterTryTactic : Command.CommandElab := fun stx => do
+  if `Lean.Elab.Tactic.Try ∉ (← getEnv).header.moduleNames then
+    logWarning "Add `import Lean.Elab.Tactic.Try` before using the `register_try?_tactic` command."
+    return
+  -- stx[0]: optional docComment, stx[1]: "register_try?_tactic",
+  -- stx[2]: optional priority clause, stx[3]: tacticSeq
+  let doc? := stx[0]
+  let prio := if stx[2].isNone then 1000 else stx[2][0][3].isNatLit?.getD 1000
+  let tacStx := stx[3]
+
+  -- Generate a unique name based on a hash of the tactic syntax
+  let tacHash := hash tacStx.prettyPrint.pretty
+  let name := Name.mkSimple s!"auxTryTactic{tacHash}"
+
+  -- Generate code that parses the tactic at runtime
+  let prioStx := Syntax.mkNumLit (toString prio)
+  let nameId := mkIdent name
+  let tacText := Syntax.mkStrLit tacStx.prettyPrint.pretty
+
+  let cmd ← `(command|
+    open Lean Meta Elab Tactic Try in
+    @[try_suggestion $prioStx] meta def $nameId
+      (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
+      let env ← getEnv
+      match Parser.runParserCategory env `tactic $tacText with
+      | Except.ok stx => return #[⟨stx⟩]
+      | Except.error _ => return #[])
+
+  let finalCmd := if doc?.isNone then cmd else ⟨doc?.setArg 1 cmd.raw⟩
+  Command.elabCommand finalCmd
+
+/--
+Evaluates a user-generated tactic and captures any "Try this" suggestions it produces
+by examining the message log.
+
+Returns an array of tactics: the original tactic followed by any extracted suggestions.
+-/
+private def expandUserTactic (tac : TSyntax `tactic) (goal : MVarId) : MetaM (Array (TSyntax `tactic)) := do
+  Term.TermElabM.run' <| do
+    let initialState ← saveState
+    let initialLog ← Core.getMessageLog
+    let initialMsgCount := initialLog.toList.length
+
+    let result ← try
+      -- Run the tactic to capture its "Try this" messages
+      discard <| Tactic.run goal do
+        evalTactic tac
+
+      -- Extract tactic suggestions from new messages
+      -- This parses the format produced by TryThis.addSuggestions: "Try this:\n  [apply] tactic"
+      let newMsgs := (← Core.getMessageLog).toList.drop initialMsgCount
+      let mut suggestions : Array (TSyntax `tactic) := #[]
+      for msg in newMsgs do
+        if msg.severity == MessageSeverity.information then
+          let msgText ← msg.data.toString
+          for line in msgText.splitOn "\n" do
+            if line.startsWith "  [apply] " then
+              let tacticText := line.drop "  [apply] ".length
+              let env ← getEnv
+              if let .ok stx := Parser.runParserCategory env `tactic tacticText then
+                suggestions := suggestions.push ⟨stx⟩
+
+      pure (some suggestions)
+    catch _ =>
+      pure none
+
+    initialState.restore
+    Core.setMessageLog initialLog
+    return #[tac] ++ (result.getD #[])
+
 -- TODO: polymorphic `Tactic.focus`
 abbrev focus (x : TryTacticM α) : TryTacticM α := fun ctx => Tactic.focus (x ctx)
 
@@ -653,10 +763,13 @@ private def addSuggestions (tk : Syntax) (s : Array Tactic.TryThis.Suggestion) :
     Tactic.TryThis.addSuggestions tk (s.map fun stx => stx) (origSpan? := (← getRef))
 
 def evalAndSuggest (tk : Syntax) (tac : TSyntax `tactic) (config : Try.Config := {}) : TacticM Unit := do
+  let initialLog ← Core.getMessageLog
   let tac' ← try
     evalSuggest tac |>.run { terminal := true, root := tac, config }
   catch _ =>
     throwEvalAndSuggestFailed config
+  -- Restore message log to suppress "Try this" messages from intermediate tactic executions
+  Core.setMessageLog initialLog
   let s := (getSuggestions tac')[*...config.max].toArray
   if s.isEmpty then
     throwEvalAndSuggestFailed config
@@ -763,26 +876,49 @@ private def mkAllIndStx (info : Try.Info) (cont : TSyntax `tactic) : MetaM (TSyn
 
 /-! Main code -/
 
-/-- Returns tactic for `evalAndSuggest` -/
-private def mkTryEvalSuggestStx (info : Try.Info) : MetaM (TSyntax `tactic) := do
+/-- Returns tactic for `evalAndSuggest` (unsafe version that can evaluate user generators) -/
+private unsafe def mkTryEvalSuggestStxUnsafe (goal : MVarId) (info : Try.Info) : MetaM (TSyntax `tactic) := do
   let simple ← mkSimpleTacStx
   let simp ← mkSimpStx
   let grind ← mkGrindStx info
+
   let atomic ← `(tactic| attempt_all | $simple:tactic | $simp:tactic | $grind:tactic | simp_all)
   let atomicSuggestions ← mkAtomicWithSuggestionsStx
   let funInds ← mkAllFunIndStx info atomic
   let inds ← mkAllIndStx info atomic
   let extra ← `(tactic| (intros; first | $simple:tactic | $simp:tactic | exact?))
-  `(tactic| first | $atomic:tactic | $atomicSuggestions:tactic | $funInds:tactic | $inds:tactic | $extra:tactic)
 
--- TODO: make it extensible.
+  -- Collect user-defined suggestions (runs after built-in tactics)
+  let userEntries := trySuggestionExtension.getState (← getEnv)
+  let mut userTactics := #[]
+  for entry in userEntries do
+    try
+      let generator ← evalConst TrySuggestionGenerator entry.name
+      let suggestions ← generator goal info
+      -- Expand each tactic to capture nested "Try this" suggestions
+      for userTac in suggestions do
+        let expandedTacs ← expandUserTactic userTac goal
+        userTactics := userTactics ++ expandedTacs
+    catch e =>
+      logWarning m!"try_suggestion generator {entry.name} failed: {e.toMessageData}"
+
+  -- Build final tactic: built-ins first, then user suggestions as fallback
+  if userTactics.isEmpty then
+    `(tactic| first | $atomic:tactic | $atomicSuggestions:tactic | $funInds:tactic | $inds:tactic | $extra:tactic)
+  else
+    let userAttemptAll ← `(tactic| attempt_all $[| $userTactics:tactic]*)
+    `(tactic| first | $atomic:tactic | $atomicSuggestions:tactic | $funInds:tactic | $inds:tactic | $extra:tactic | $userAttemptAll:tactic)
+
+@[implemented_by mkTryEvalSuggestStxUnsafe]
+private opaque mkTryEvalSuggestStx (goal : MVarId) (info : Try.Info) : MetaM (TSyntax `tactic)
 
 @[builtin_tactic Lean.Parser.Tactic.tryTrace] def evalTryTrace : Tactic := fun stx => do
   match stx with
   | `(tactic| try?%$tk $config:optConfig) => Tactic.focus do withMainContext do
     let config ← elabTryConfig config
-    let info ← Try.collect (← getMainGoal) config
-    let stx ← mkTryEvalSuggestStx info
+    let goal ← getMainGoal
+    let info ← Try.collect goal config
+    let stx ← mkTryEvalSuggestStx goal info
     evalAndSuggest tk stx config
   | _ => throwUnsupportedSyntax
 

tests/lean/run/try_register_builtin.lean

@@ -0,0 +1,14 @@
+/-
+Test that register_try?_tactic works as a builtin command
+The syntax is available without any imports, but it warns when Lean.Elab.Tactic.Try is not imported
+-/
+
+-- Custom predicate for testing
+inductive MyProp : Prop where
+  | intro : MyProp
+
+/--
+warning: Add `import Lean.Elab.Tactic.Try` before using the `register_try?_tactic` command.
+-/
+#guard_msgs in
+register_try?_tactic exact MyProp.intro

tests/lean/run/try_user_suggestions.lean

@@ -0,0 +1,125 @@
+/-
+Test that try? supports user-defined suggestion generators via @[try_suggestion]
+-/
+module
+public import Lean
+public meta import Lean.Elab.Tactic.Try
+
+open Lean Meta Elab Tactic Try
+
+-- Define a custom inductive predicate that built-in tactics won't solve automatically
+inductive CustomProp : Prop where
+  | mk : CustomProp
+
+-- Lemma about CustomProp
+theorem customPropHolds : CustomProp := CustomProp.mk
+
+section BasicTest
+-- Define a generator that suggests the custom lemma
+@[local try_suggestion]
+meta def customPropSolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
+  return #[← `(tactic| exact CustomProp.mk)]
+
+-- Test that try? picks up the user-defined suggestion
+-- Built-in tactics won't solve this, so only user suggestion appears
+/--
+info: Try this:
+  [apply] exact CustomProp.mk✝
+-/
+#guard_msgs in
+example : CustomProp := by
+  try?
+end BasicTest
+
+section PriorityTest
+-- Test priority ordering with multiple generators
+@[local try_suggestion 2000]
+meta def highPrioritySolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
+  return #[← `(tactic| apply CustomProp.mk)]
+
+@[local try_suggestion 1000]
+meta def midPrioritySolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
+  return #[← `(tactic| exact CustomProp.mk)]
+
+@[local try_suggestion 500]
+meta def lowPrioritySolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
+  return #[← `(tactic| constructor)]
+
+-- All generators return successful tactics, ordered by priority (highest first)
+/--
+info: Try these:
+  [apply] apply CustomProp.mk✝
+  [apply] exact CustomProp.mk✝
+  [apply] constructor
+-/
+#guard_msgs in
+example : CustomProp := by
+  try?
+end PriorityTest
+
+section BuiltInFallback
+-- Test that user generators only run if built-ins fail
+-- For True, built-ins succeed so user generators shouldn't run
+@[local try_suggestion]
+meta def shouldNotRunForTrue (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
+  return #[← `(tactic| exact True.intro)]
+
+-- Built-ins succeed, so user suggestion doesn't appear
+/--
+info: Try these:
+  [apply] simp
+  [apply] simp only
+  [apply] grind
+  [apply] grind only
+  [apply] simp_all
+-/
+#guard_msgs in
+example : True := by
+  try?
+end BuiltInFallback
+
+section DoubleSuggestion
+-- Test double-suggestion: when a user tactic produces "Try this" messages,
+-- both the original tactic and the suggestions should appear
+-- Use CustomProp which built-ins can't solve
+@[local try_suggestion]
+meta def doubleSuggestionSolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
+  return #[← `(tactic| show_term apply CustomProp.mk)]
+
+-- Double-suggestion: when show_term produces a "Try this" message,
+-- both the original tactic and the extracted suggestion should appear
+-- The message from show_term during extraction is suppressed
+/--
+info: Try these:
+  [apply] show_term apply CustomProp.mk✝
+  [apply] exact CustomProp.mk
+-/
+#guard_msgs in
+example : CustomProp := by
+  try?
+end DoubleSuggestion
+
+section RegisterCommand
+-- Test the register_try?_tactic convenience command
+register_try?_tactic (priority := 500) constructor
+
+/--
+info: Try this:
+  [apply] constructor
+-/
+#guard_msgs in
+example : CustomProp := by
+  try?
+
+-- Test without explicit priority (should default to 1000, so appear before constructor at 500)
+register_try?_tactic apply CustomProp.mk
+
+/--
+info: Try these:
+  [apply] apply CustomProp.mk
+  [apply] constructor
+-/
+#guard_msgs in
+example : CustomProp := by
+  try?
+end RegisterCommand

tests/lean/versoDocMissing.lean.expected.out

@@ -1 +1 @@
-versoDocMissing.lean:10:0: error: unexpected end of input; expected '#guard_msgs', 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_dsimproc', 'builtin_dsimproc_decl', 'builtin_grind_propagator', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'coinductive', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'dsimproc', 'dsimproc_decl', 'elab', 'elab_rules', 'example', 'grind_propagator', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'recommended_spelling', 'register_error_explanation', 'register_tactic_tag', 'simproc', 'simproc_decl', 'structure', 'syntax', 'tactic_extension', 'theorem' or 'unif_hint'
+versoDocMissing.lean:10:0: error: unexpected end of input; expected '#guard_msgs', 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_dsimproc', 'builtin_dsimproc_decl', 'builtin_grind_propagator', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'coinductive', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'dsimproc', 'dsimproc_decl', 'elab', 'elab_rules', 'example', 'grind_propagator', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'recommended_spelling', 'register_error_explanation', 'register_tactic_tag', 'register_try?_tactic', 'simproc', 'simproc_decl', 'structure', 'syntax', 'tactic_extension', 'theorem' or 'unif_hint'