feat: automatic try? suggestions for empty by, unsolved goals, and sorry#13830
Draft
nomeata wants to merge 38 commits into
Draft
feat: automatic try? suggestions for empty by, unsolved goals, and sorry#13830nomeata wants to merge 38 commits into
try? suggestions for empty by, unsolved goals, and sorry#13830nomeata wants to merge 38 commits into
Conversation
…vedGoal,onSorry}` options This PR replaces the in-elaborator `tactic.tryOnEmptyBy` mechanism with a post-elaboration hook that walks each command's info trees and runs `try?` at positions of interest, offering three independently-gated triggers: * `autoTry.onEmptyBy` -- on empty `by` blocks (replaces the old `tactic.tryOnEmptyBy`) * `autoTry.onUnsolvedGoal` -- on every tactic that left goals unsolved (in practice the suggestion at the terminal tactic of a `by` block is the relevant one) * `autoTry.onSorry` -- on each `sorry` (term or tactic), de-duplicated by source position so `by sorry` reports once The walk lives in the new `Lean.Elab.Tactic.AutoTry` module. It hooks into `addLinter` because that is a convenient post-command-elab entry point with infotree access, but the feature is not a linter in the user-facing sense: it does not bail on `messages.hasErrors`, the triggers are not bundled with `linter.all`, and the options are *not* under the `linter.` namespace -- using the hook borrows infrastructure rather than identity. The `by` term elaborator returns to its pre-`tryOnEmptyBy` form: no second registered `@[builtin_term_elab byTactic]`, no `errToSorry` gate, no `elabByTacticCore` split. `elabTryCore` in `Lean.Elab.Tactic.Try` becomes public so `AutoTry` can drive it. A new `trace.autoTry` trace class is available for diagnostics. Behavior changes from the old `tactic.tryOnEmptyBy`: * the option is renamed (`tactic.tryOnEmptyBy` -> `autoTry.onEmptyBy`) * nested-in-backtracking empty `by` (e.g. `first | exact (by) | trivial`) also triggers a suggestion now; the linter does not have access to the `errToSorry` flag the elaborator used. The outer proof still succeeds. * the disable-footer is dropped (the option name is in the option's description, which suffices for `set_option ... false` discoverability) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…nd tests This PR refines the auto-`try?` hook in two ways: * Drop the `sorry` *term* trigger path. Only `sorry` *tactic* fires now. The term-level case was redundant -- `by sorry` already gets covered via the tactic trigger -- and a bare term `:= sorry` is a different ergonomic case that arguably shouldn't be a `try?` site. * Skip triggers nested inside multi-elaboration combinators. Tactics like `first | a | b`, `<;>` (which expands to `focus / all_goals`), `try ...`, `attempt_all`/`attempt_all_par`, `first_par`, `repeat`/`repeat'`, `iterate`, `any_goals` all elaborate their arguments multiple times or in a backtracking context. Running `try?` on each speculative branch produces noisy suggestions for code that did not in fact fail. The infotree walk now tracks a combinator depth (`isMultiElabCombinator`) and only emits triggers at depth zero. In practice this restores the pre-linter behavior for `by first | exact (by) | trivial` (no suggestion for the failed inner branch) and `_ <;> _` (no per-goal suggestion spam), while still firing on the outer terminal tactic if the proof as a whole left goals unsolved. Renames `tests/elab/tryOnEmptyBy.lean` to `tests/elab/autoTry.lean` and expands it to cover all three triggers, including the nested-in-combinator suppression and the explicit "no term-`sorry`" case. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… heuristics This PR drops the hand-maintained `isMultiElabCombinator` list in favor of two data-driven heuristics, both motivated by the observation that a single "Try this" suggestion cannot replay against multiple proof states: 1. *Per-syntax multi-elaboration*: count `TacticInfo` nodes grouped by `(kind, sourcePos)`. Tactics whose count exceeds one were elaborated against multiple goals (rhs of `<;>` -> `all_goals`, body of `repeat`, `repeat'`, `iterate`, etc.) and we skip them. Keying by `(kind, pos)` rather than just `pos` distinguishes the user-typed tactic from its macro-expanded form (e.g. `sorry` -> `exact sorry`), which would otherwise spuriously inflate the count. 2. *Same-goal dedup*: when collecting triggers, group by the `MVarId` of the relevant goal so that `by first | skip | trivial` (where both `skip` and the outer `first` carry the same unsolved-goal mvar) only produces one suggestion -- at the first (outer) site visited by the depth-first traversal. A new `hasNonUnsolvedGoalError` check additionally suppresses the entire hook on commands that logged any error besides "unsolved goals". The intuition: if the user is in the middle of fixing a broken proof, a suggestion at the unsolved-goal site is noise. Behavioral consequence: `by first | exact (by) | trivial` and similar do trigger a suggestion now (one branch is elaborated against one goal, so the uniqueness heuristic doesn't catch it). The `<;>`, `repeat`, etc. cases that motivated the suppression originally are still handled. Tests updated and expanded to cover all three triggers, the `<;>` suppression case, and the error-gate case. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ductive; drop redundant `private`s `TriggerKind` was a `Nat` abbreviation with hand-maintained doc comments mapping `0`/`1`/`2` to the three triggers. Replace with a proper inductive (`emptyBy`/`sorryTactic`/`unsolvedGoal`), now that the `meta` section allows declaring one once `Init.Prelude` is imported as a non-`meta` public import. All trigger-kind sites at the construction and dispatch points get their named constructors back. Also drop the `private` markers on declarations inside the module body -- the new module system makes everything private to the module by default, so the `private` keyword was redundant noise. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…imports The file is internal (consumed only by `Lean.Elab.Tactic`'s umbrella module to trigger `builtin_initialize addLinter`), so the imports don't need to be re-exported -- plain `import` suffices. And the linter machinery runs at ordinary `CommandElabM` time, not at elaborator-construction time, so the `meta` qualifier was unnecessary too. Matches the import style of other core linters like `Lean.Linter.Extra.UnreachableTactic`. Also drops `public section`, which had the same overreach. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Address a code review of the auto-`try?` feature with a batch of small, independent improvements: * Drop the synthetic-stx case at candidate-collection time so the code action always has a real document range to apply. * Fix the option-merge direction in `runMetaMWithMessages` so the saved infotree options win over surrounding `CommandElabM` options. * Re-raise interrupt / max-recursion exceptions from `try?` instead of swallowing them. * Use `Lean.Syntax.Range.contains` against the raw position from `stx.getRange?` in `hasNonUnsolvedGoalError`, replacing the lossy line-only comparison. * Replace the hand-rolled `InfoTree` recursion with `InfoTree.foldInfo` and `InfoTree.foldInfoM`. * Replace the two-pass `(kind, pos)` multiplicity scheme with a single collection pass plus a `pos`-only drop-on-duplicates filter. * Key `seenGoal` on `MVarId` directly instead of `MVarId.name`. * Add a comment explaining `setExporting false` in `runMetaMWithMessages`. * Restrict the unsolved-goal trigger to exactly one remaining goal, so e.g. \`constructor\` (two open goals) stays silent. * Add a \`#guard_msgs (positions := true)\` regression test verifying the unsolved-goal suggestion anchors at the failing tactic, distinct from the error's wider range. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Expose `evalAndCollectSuggestions` and `collectTryCoreSuggestions` returning the raw suggestion array, so callers outside `try?`'s normal syntax-driven flow can format and emit the suggestions themselves. Used by the upcoming append-mode rendering in the `autoTry` linter. No behavioural change in `try?` itself. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Reshape `autoTry.onUnsolvedGoal` to suggest *appending* a tactic to the existing `by` block rather than replacing the failing tactic. Concretely: * Drop `autoTry.onEmptyBy` -- the empty-`by` case is subsumed by the reshaped `onUnsolvedGoal` (an empty `by` has exactly one unsolved goal by definition). * Trigger on the `byTactic` node, not on inner tactics; fires when the byTactic left exactly one unsolved goal. * For `by skip`, the suggestion now reads as `by skip; <found>` (with a `"; "` separator). For empty `by`, it reads as `by <found>`. For multi-line `by`, it reads as a newline + indent-aligned append. * The [apply] widget continues to display the bare tactic; the actual edit text (separator + tactic) is computed once and stored in `Suggestion.suggestion`, with `messageData?` overriding the rendering. To make the edit verifiable in tests, add `autoTry.debug.showEdits` which logs an info message per suggestion describing the replacement text and the (zero-width) insertion position. Positions are emitted relative to the enclosing command's first line, matching the format of `#guard_msgs (positions := true)` so tests can be moved around the file without breakage. Internals: * `Lean.Elab.Tactic.Try` gains a public `collectTryCoreSuggestions` returning the raw suggestion array; the existing `evalAndSuggest` flow is unchanged. * The autoTry hook wraps its full body in a final `try ... catch` that re-raises only control-flow exceptions; everything else (including `try?` failing in restricted contexts like a prelude file) is logged at trace level and swallowed so the linter never produces a user-visible error. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…e unexpected errors * Restore the `autoTry.onEmptyBy` option as a strict subset of `autoTry.onUnsolvedGoal`. It fires only when the `by` block has no tactics yet -- useful when the user wants suggestions only for "start-of-proof" sites and not on every in-progress proof. * Drop the broad `try ... catch` that previously swallowed any exception escaping `try?`'s internals. Such errors now propagate as linter failures so they remain visible. * Update `tests/elab/try_prelude.lean` to expect the surfaced linter error in restricted (prelude) environments; the comment notes this as a documented limitation for now. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Apply the simplifications identified by the post-review pass: * Drop `dropMultiElabCandidates` helper. Its position-multiplicity check was followed by another `seenPos` dedupe in the hook body; after the multiplicity filter, no two surviving candidates share a position, so the second pass was redundant. The hook now builds the counts map inline and skips both passes' work in one loop. * Drop the `seenGoal` MVarId dedupe. Distinct trigger positions have distinct mvars by construction (nested by-blocks operate on fresh goals), so the filter never actually rejected anything. * Collapse the double `match k` in the hook body (one to compute `goal?`, one to dispatch the action) into a single match per kind. * Inline the `push` closure in `collectTriggerPoints`: its `anchor` argument was always `tacInfo.stx`, and the `getPos?` guard is a one-line pre-check at the top of the case. * Factor `evalAndSuggestWithBy` in `Try.lean` through `evalAndCollectSuggestions` (the missing call-site from the earlier factoring commit). Net effect: 62 lines of `AutoTry.lean` reduced to 36; identical behaviour, identical test output. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
# Conflicts: # tests/elab/tryOnEmptyBy.lean
The "after a command is elaborated" wording was implementation context (when the hook runs), not user-facing behaviour. The short descrs now read as plain "what this option does" statements. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…dits Debug options conventionally live under the `debug.` prefix; the previous name was inconsistent with `debug.tactic.try.*` and similar. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`ctx.options` is the options snapshot at the saved infotree point and already inherits file-/command-scope settings, so the previous merge against the surrounding `CommandElabM` options was redundant. Drop the merge and pass `ctx.options` straight through. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`collectSuggestionsForGoal` used an `IO.Ref` only because `Tactic.run` returns the post-run goals, not the action's value. Make `runCore'` non-private and use it to thread the suggestion array out of TacticM through TermElabM into MetaM and finally CommandElabM as a normal return value. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The body of emitAppendSuggestions only uses operations that are available in `CoreM` (pretty-printing tactic syntax, reading options, logging info messages, calling `Tactic.TryThis.addSuggestion`), so there is no reason to enter `MetaM`. Factor out `runCoreMWithMessages` from the existing `runMetaMWithMessages`; the MetaM variant now just wraps the CoreM one. The unused `mctx` parameter on `emitAppendSuggestions` is also dropped. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Reword the docstring on `runReplaceTryOnGoal` to drop the misleading "legacy syntax-driven path" framing. * Note in `computeAppendSep` that this is a heuristic to be replaced by a proper formatter when available. * Reformat multiline docstrings so that `/--` and `-/` are on their own lines with the content unindented, matching the convention in the rest of `src/Lean`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`autoTry.onUnsolvedGoal` previously fired only on `by` blocks. It now fires on any tactic-sequence container -- `by`, `· …`, `case h => …`, `focus …`, and `(…)` -- whose body left exactly one unsolved goal. The suggestion is rendered as an append at the appropriate position for the host. `autoTry.onEmptyBy` remains a strictly narrower variant that fires only on empty `by` blocks. * New tests cover `case h => skip` and `· skip` inside a `by` block; both produce per-scope suggestions in addition to the outer-`by` suggestion for the sibling goal. * `computeAppendSep` now looks up the body via a generic `findBodySeq` helper that searches for the first `tacticSeq` child, replacing the byTactic-specific `byStx[1]` access. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Drop the hardcoded `isTacticSeqContainer` kind list; instead trigger `onUnsolvedGoal` on any `TacticInfo` whose syntax has a `tacticSeq` child, found via the existing `findBodySeq` helper. This naturally covers `by`, `· …`, `case … => …`, `focus …`, `(…)`, `try …`, and any future tactic of the same shape without needing to extend the list. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`emitAppendSuggestions` was routing through `runCoreMWithMessages` to get a CoreM context, but every operation it performs (`getOptions`, `getFileMap`, `PrettyPrinter.ppTactic`, `logInfoAt`, `Tactic.TryThis.addSuggestion`) is available in CommandElabM either natively or via `liftCoreM`. Drop the wrapping; the function no longer needs the saved `ContextInfo`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…cases The new `case` and `·` tests produce two "Try these" messages, one per scope. Enabling positions in `#guard_msgs` makes them distinguishable at a glance: each suggestion's anchor span tells you which scope it belongs to. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…thMessages The `runCoreMWithMessages` split was introduced when `emitAppendSuggestions` still wrapped its body in one of them. That wrapping is gone, so the only remaining caller (both `collectSuggestionsForGoal` and `runReplaceTryOnGoal`) needs the MetaM variant. Drop the CoreM helper and inline its body in `runMetaMWithMessages`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
Reverts the change that made `TacticM.runCore'` non-private. Inline the same effect in `collectSuggestionsForGoal` using `ReaderT.run` and `StateRefT.run'`, both of which are already public. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ptyProof Switch the trigger criterion for `autoTry.onUnsolvedGoal` from "`goalsAfter.length == 1`" to "there's an unsolved-goals error in the scope's range". This: * Picks up scopes that admitted with sorry but emitted an error first (`·` with a body that doesn't close, `case h => …` likewise). * Skips combinators that silently admit without erroring -- notably `case'`, which docs explicitly as "does not ensure the goal has been solved nor admits the goal if `tac` failed". Rename `autoTry.onEmptyBy` to `autoTry.onEmptyProof`. The option now fires on *any* tactic-sequence container whose body has no tactics yet -- empty `by`, empty `·`, empty `case h => `, etc. -- as long as the scope emitted an unsolved-goals error. Internals: * `hasUnsolvedGoalErrorInRange` walks `reportedPlusUnreported` (not just `unreported`), so the linter sees errors that the surrounding framework has already marked reported by the time it runs. * `hasNonUnsolvedGoalError` switched to the same accessor. * The candidate tuple now carries `(mctx, goal)` directly so the hook doesn't have to re-derive them from the `TacticInfo`; in particular scopes that admitted with sorry fall back to `goalsBefore.head`. Tests cover empty `· `, empty `case` (fires), and `case' … => skip` (doesn't fire); the latter is the regression test for the error-gated behaviour. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ings Drop the "tactic-sequence scope/container" jargon in favour of "empty proofs and empty subproofs"; reframe `onUnsolvedGoal` as the broader form of `onEmptyProof` rather than the other way around. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… scope
Two related fixes:
1. **Nested-scope error isolation.** Previously a scope fired whenever
an unsolved-goals error existed *anywhere* in its range. That
misfired on patterns like
```lean
example : True := by
have h : False := by skip
trivial
```
where the outer `by` is closed by `trivial`, but the nested `have`
left a goal unsolved. Replace the "any error in range" check with
an "owns error" check: a candidate owns an error iff its range
contains the error position and no strictly deeper candidate's
range also contains it.
2. **Focused-goal selection.** Previously the goal for `try?` was
read off the container's `goalsBefore`/`goalsAfter`, taking
`.head`. That's wrong for scopes like `case right => …`, where
`right` need not be the head of the parent's goal list. Read the
focused goal off the body's `tacticSeq` info-tree node instead:
that node's `goalsAfter` (or `goalsBefore` as a fallback for
admitted bodies like `by { }` / `·`) reflects the actual focused
goal the user sees as unsolved.
Both fixes use information that's already in the info tree -- in
particular, switching `collectTriggerPoints` from `foldInfoM` to
`foldInfoTree` (so it can see each container's children) is the only
structural change.
New tests cover both: nested `have := by skip` inside a closed `by`,
and `case left => skip` in a `False ∧ True` proof.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
github-actions
Bot
added
the
mathlib4-nightly-available
…ee-node count When `findFirstBodyGoal` walks a container's children, it now collects *all* immediate-descendant `tacticSeq` info-tree nodes. If more than one is found, the body was elaborated against multiple proof states (typical of the rhs of `<;>` via `all_goals`); a single suggestion can't be replayed against all of them, so we return `none` and the candidate stays quiet. Previously the "first match" heuristic silently picked one of the multi-elab invocations and emitted a misleading suggestion. Also: make `autoTry.onUnsolvedGoal`'s docstring self-contained rather than referencing `onEmptyProof`, and considered the user's idea of matching by `MVarId` between unsolved-goals error and candidate body -- rejected for now because scopes that share a focused goal (e.g. `case'` that silently leaves the goal open and the enclosing `by` that errors about the same goal) cannot be distinguished by `MVarId` alone. The position-based deepest-owner check remains the right signal. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Reaffirm the `goalsAfter.isEmpty` case in `findFirstBodyGoal`: for
admitted-empty-body forms (`by { }` and `· `, both of which close the
focused goal with sorry at the wrapper), the body's `tacticSeq`
info-tree node has `goalsAfter = []` and there's no deeper tacticSeq
node to fall through to (the parser produces no separate body node
when the body is empty). The goal the user sees as unsolved is still
the one we entered the body with -- read it off `goalsBefore`.
Documenting why this fallback is still needed after switching to the
inner-tacticSeq-based goal lookup, so we don't try to drop it again.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add a regression test pinning the current (suboptimal) behaviour on
`by have h := True.intro; { }`: the outer `by` block fires via the
`goalsBefore` fallback in `findFirstBodyGoal` (because the inner
empty `{ }` admitted the focused goal and has no body tacticSeq to
read off), the suggestion is anchored *after* the `{ }` -- so pasting
any of the suggested tactics would run against "no goals to be
solved" because the admit already closed the goal -- and the local
context the suggestion is computed in coincidentally still includes
`h` only because the error message captures the live `lctx`.
The proper fix is for admit-emitting elaborators to push an explicit
autoTry info-tree marker carrying the precise `(mctx, goal,
insertPos)` triple. Until then, this test documents the gap; once
the fix is in, the test should be updated to expect a suggestion
that uses `h` and is anchored *inside* the admit wrapper.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
mathlib-lean-pr-testing
Bot
added
the
builds-mathlib
…ooks
This PR makes the `autoTry` linter consume an explicit `AutoTryHook.HookInfo`
info-tree marker that admit-emitting elaborators (`by`, `tacticSeqBracketed`,
`cdot`, `case`) push at the exact admit point, carrying the focused goal,
mctx, and tactic sequence to extend. Previously the linter had to infer all
of this from scope spans and `unsolved goals` error positions, which read
hypotheses off the wrong state for admit-wrapped bodies (e.g. `by have h := …; { }`)
and inserted suggestions at the wrong append point.
`closeUsingOrAdmit` now takes an optional `onAdmit : MVarId → MetavarContext → TacticM Unit`
that fires before the goal is admitted with `sorry`. The pre-tactic mctx
snapshot is passed in because `focusAndDone` → `done` admits the goal via
`reportUnsolvedGoals` before the exception is caught, so `getMCtx` at the
catch point already sees the goal as assigned.
Drops the position-based error-ownership filter and the `findBodySeq` /
`findFirstBodyGoal` fallbacks from `AutoTry.lean`. The separator heuristic
for append suggestions also simplifies to "always `; ` unless the existing
tactic sequence already has more than one entry on separate lines".
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR makes `closeUsingOrAdmit`'s `onAdmit` hook fire with the focused goal
and `MetavarContext` as they stand *after* the tactic ran (but before the goal
is admitted to `sorry`). Previously the hook saw the entry state, so for bodies
that add hypotheses before failing (e.g. `· have h : True := True.intro`) the
suggestion was computed against the wrong local context.
`onAdmit` now only fires when exactly one goal remains -- a single suggestion
can't replay against multiple subgoals from e.g. `apply f` decomposing the
focused goal.
Tests cover state-changing bodies in `{ }`, `· `, and `case h => …`: each
introduces an `h : True` hypothesis whose presence is detectable by `try?`
suggesting `assumption` as its first candidate.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Collaborator
Author
|
Not quite satified with the interaction between elaborators, the messages and info tree, and the autoTry linter. Tried a few things, but nothing quite convincing. May have to sit and simmer for a bit for better ideas. |
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 25, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
May 25, 2026
…olvedGoals`
This PR moves the autoTry info-tree marker into `Term.reportUnsolvedGoals` itself,
which now pushes one `AdmittedGoalInfo { mctx, goal }` leaf per unsolved goal at
the current `ref` before admitting any of them to `sorry`. The dedicated
`AutoTryHook` module, `closeUsingOrAdmit`'s `onAdmit` callback, and the SyntheticMVars
push site all go away; `closeUsingOrAdmit` goes back to plain `focusAndDone`.
The linter recovers the body to extend from the leaf's `stx` by walking the
surrounding command syntax for the smallest enclosing admit-emitting scope
(`byTactic` / `tacticSeqBracketed` / `cdot` / `case` / `case'`). The "single
remaining goal" filter -- which is autoTry-specific, not a property of
`reportUnsolvedGoals` -- moves into the linter's duplicate-position counting.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR drops the `AdmittedGoalInfo` info-tree push from `Term.reportUnsolvedGoals` and recovers the same `(mctx, mvarId)` data by walking the command's message log: each `Tactic.unsolvedGoals` error already carries the goals structurally (`MessageData.ofGoal mvarId`) under a `MessageData.withContext`, so a small walk over the `MessageData` recovers the same pairs the producer used to push. The trigger logic now: 1. Walks `MessageData` for `(mctx, mvarId)` pairs on every `Tactic.unsolvedGoals` error. 2. Finds the deepest `TacticInfo` whose `goalsAfter` still contains the mvar -- the last tactic that didn't close it. 3. Walks the command syntax for the surrounding admit-emitting scope (`by` / `tacticSeqBracketed` / `cdot` / `case` / `case'`) to recover the body to extend and the diagnostic ref. `Term.reportUnsolvedGoals` reverts to its original `MetaM Unit` shape, no info-tree push. The memory cost of carrying a `MetavarContext` per unsolved goal in the info tree is no longer paid on deep-elaboration paths (mutual defs, WF/Fix). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR simplifies the trigger lookup: `findEnclosingAdmitScope` now takes the range of the `Tactic.unsolvedGoals` error directly and walks the command syntax for the smallest admit-emitting scope containing that range. The previous detour through `findLastTacticForGoal` (find deepest `TacticInfo` with the mvar in `goalsAfter`, then walk syntax up from there) was redundant -- the message range already pinpoints the scope. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 25, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
May 25, 2026
…lookup
This PR simplifies the trigger by:
* Using the *unsolved-goals error's source range* as the "Try this:" diagnostic
anchor (a synthetic Syntax with that range), so the suggestion always shows up
at the same location as the error -- if the user sees the error, they see the
suggestion.
* Narrowing the syntax-kind dispatch in `findTacticSeqBody` from five wrapper
kinds (`byTactic`, `tacticSeqBracketed`, `cdot`, `case`, `case'`) to two body
kinds (`tacticSeq1Indented`, `tacticSeqBracketed`). The dispatch is now only to
read the tactics-container at the right child index (0 vs 1) and to know that
the empty-body insertion point sits before `}` for bracketed bodies.
* Walking the path of `range`-containing nodes and taking the outermost
seq-variant in the smallest containing subtree, so we correctly find the body
whether the error is logged inside it (`case h => skip`, `{ skip }`, `· skip`)
or at an adjacent token (`by` keyword for `by skip`, the synthetic case-body
marker, etc.).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR rewrites the `autoTry` tests around two opaque propositions `P` / `Q` and a single `@[try_suggestion]` generator that returns one tactic per recognised goal type, combined with `debug.tactic.try.onlyUserSuggestions` to disable the expensive built-in branches of `try?` (`simp` / `grind` / `exact?` / …). The tests are now smaller (501 vs 628 lines), faster (one tactic per suggestion to elaborate, no library search), and stable against try?-ordering churn (no more `impossible by simp` vs `impossible by decide` vs `impossible by grind` flakiness). The suggester also exercises focused-goal correctness: it returns `exact Pintro` for `P` goals, `exact Qintro` for `Q` goals, and prefers a local `h` when one is in scope, so the suggestion text itself proves which goal and which context the generator saw. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 25, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
May 25, 2026
This PR adds a test for `induction n with | zero => skip | succ n ih => skip`, exercising a composite tactic whose syntax embeds one `tacticSeq` per branch. Each unsolved branch fires its own suggestion anchored at the branch's body. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 25, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
May 25, 2026
`runLintersAsync` accumulates diagnostics both in the command state's message log and in the snapshot tree it then merges back, so the same `Tactic.unsolvedGoals` error commonly appears twice in `(← get).messages`. The downstream `counts > 1` filter -- which is meant to suppress scopes elaborated against multiple proof states (the rhs of `<;>`, etc.) -- collapsed both copies into a single bogus duplicate and silently skipped legitimate triggers, including the empty-`by` ones that drive the `cancellation_empty_by` server test. This PR scopes the message walk to the current command's range and dedups the remaining unsolved-goal errors by source range before emitting candidates. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 26, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
May 26, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds automatic
try?suggestions at common proof sites, gated by three optionsthat default to off:
autoTry.onEmptyProof— suggests on empty proofs and empty subproofs: emptyby,empty
·, emptycase h =>, and so on.autoTry.onUnsolvedGoal— likeautoTry.onEmptyProof, but also fires on proofs andsubproofs that already contain some tactics and left a goal unsolved. The suggestion
is appended to the existing sequence (e.g.
by skip→by skip; <found>).autoTry.onSorry— suggests onsorrytactics; the suggestion replaces thesorry.Suggestions are silenced on commands that logged any error other than "unsolved goals",
and on tactic positions elaborated against multiple proof states (rhs of
<;>, body ofrepeat/iterate, …) where a single replacement can't be replayed.This iterates on #13430, with a different implementation, and removes the
tactic.tryOnEmptyByoption added there.