From eb675f708b82079b412388dfc2ce03d0aadc4daa Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Thu, 13 Nov 2025 10:49:54 +1100 Subject: [PATCH] feat: user extensibility in `try?` (#11149) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 ` 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. --- > [!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)? ` 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. > > 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). --- src/Init/Try.lean | 13 ++ src/Lean/Elab/Tactic/Try.lean | 148 ++++++++++++++++++- tests/lean/run/try_register_builtin.lean | 14 ++ tests/lean/run/try_user_suggestions.lean | 125 ++++++++++++++++ tests/lean/versoDocMissing.lean.expected.out | 2 +- 5 files changed, 295 insertions(+), 7 deletions(-) create mode 100644 tests/lean/run/try_register_builtin.lean create mode 100644 tests/lean/run/try_user_suggestions.lean diff --git a/src/Init/Try.lean b/src/Init/Try.lean index 3597174f2f..bc05b0d9f8 100644 --- a/src/Init/Try.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean index a17c44dc4c..eeb7736080 100644 --- a/src/Lean/Elab/Tactic/Try.lean +++ b/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 diff --git a/tests/lean/run/try_register_builtin.lean b/tests/lean/run/try_register_builtin.lean new file mode 100644 index 0000000000..5de79c7cab --- /dev/null +++ b/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 diff --git a/tests/lean/run/try_user_suggestions.lean b/tests/lean/run/try_user_suggestions.lean new file mode 100644 index 0000000000..7ed8da6864 --- /dev/null +++ b/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 diff --git a/tests/lean/versoDocMissing.lean.expected.out b/tests/lean/versoDocMissing.lean.expected.out index bf8baa66f4..d391964f10 100644 --- a/tests/lean/versoDocMissing.lean.expected.out +++ b/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'