From 2229b077d6ebd2ff42d665fe1c32501df8915dff Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 11 May 2026 08:31:42 +0200 Subject: [PATCH] feat: empty `by` runs `try?` to suggest a proof (#13430) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR makes an empty `by` block run `try?` in the background and surface its suggestions, while still producing the usual unsolved-goals diagnostic. The implicit `try?` is informational only — it does not change elaboration behavior beyond emitting messages. Behaviour is controlled by a new option `tactic.tryOnEmptyBy`, disabled by default for now; set it to `true` to opt in. The default may flip in a future release. Behaviour summary, when the option is enabled: * The empty `by` reports unsolved goals immediately, before the (possibly slow) `try?` has finished. * The `try?` work is spawned as an asynchronous snapshot task (`Term.wrapAsyncAsSnapshot` + `Core.logSnapshotTask`), so subsequent elaboration is not blocked and the suggestions arrive when ready. * `try?` is gated on its parser infrastructure being available, so working on the prelude (before `Init.Try` is imported) keeps the regular empty-`by` behaviour. * No effect when the empty `by` appears inside a backtracking combinator (e.g. `first | exact (by) | …`) or when `try?` finds no applicable suggestion. Implementation notes: * `elabEmptyByAsTry` (in `Lean.Elab.Tactic.Try`) is registered as a second `@[builtin_term_elab byTactic]`, alongside the existing `elabByTactic` in `Lean.Elab.BuiltinTerm`. The gate `shouldElabEmptyByAsTry` is checked in both elaborators so the empty-`by` path takes the `try?` route while non-empty `by` follows the regular path. The body shared between them is factored as `elabByTacticCore`. The two-elaborator setup avoids a circular module dependency between `BuiltinTerm.lean` and `Tactic/Try.lean`; an inline comment in `Try.lean` explains this. * A latent bug from #13229 is fixed along the way: `evalSepTactics` returned at the very top for an empty tactic sequence without resolving the `tacSnap` promise that `MutualDef.mkTacTask` sets up for `:= by …` bodies. The dangling promise was harmless in typical use because the cmd's cancellation token would fire shortly after elaboration and drop it, but with a slow async snapshot task in the same command (as the implicit `try?` here) the language-server info-tree walk would block on it and the editor's Messages view would only update once the task finished. Resolved at the early-return in `evalSepTactics`. * The test infrastructure in `Lean.Server.Test.Cancel` gains a label-keyed `testTasksRef` registry plus `mkTestTask` / `wait_for_test_task`. The pre-existing `block_until_cancelled` is reimplemented on top of `mkTestTask` and the redundant `blockUntilCancelledOnce` ref is removed. Tests: * `tests/elab/tryOnEmptyBy.lean`, `tests/elab/try_prelude.lean` — feature behaviour and prelude gating. * `tests/server_interactive/cancellation_empty_by.lean` — verifies that on document re-elaboration `cancelRec` reaches the empty-`by` snapshot's cancel token registered with `Core.logSnapshotTask`. A `[try_suggestion]` generator wires the outer cancel token's `onSet` to resolve a `mkTestTask "T_outer"` promise, and the candidate `wait_for_test_task "T_outer"` waits on it. If `cancelTk? := none` is passed to `Core.logSnapshotTask`, `cancelRec` cannot reach the token, the wait blocks, and the runner times out. If `cancelTk? := none` is also passed to `wrapAsyncAsSnapshot`, no `onSet` resolver is registered, the promise drops without resolution, and `wait_for_test_task` surfaces a `"task dropped"` diagnostic on stderr. * `tests/server_interactive/cancellation_try_plain.lean` — verifies cancellation of plain `try?` (no `=>`) when its `[try_suggestion]` candidate runs synchronously inside `expandUserTactic`, by chaining through `wait_for_cancel_once_async`'s shared promise. Breaking `SnapshotTask.cancelRec` to skip walking children causes a runner timeout. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.6 --- src/Lean/Elab/BuiltinTerm.lean | 39 +++++++- src/Lean/Elab/Tactic/BuiltinTactic.lean | 6 ++ src/Lean/Elab/Tactic/Try.lean | 58 ++++++++++-- src/Lean/Meta/Tactic/TryThis.lean | 10 +- src/Lean/Server/Test/Cancel.lean | 91 ++++++++++++------- tests/elab/info_trees.lean | 45 ++++----- tests/elab/tryOnEmptyBy.lean | 68 ++++++++++++++ tests/elab/try_prelude.lean | 15 +++ .../cancellation_empty_by.lean | 68 ++++++++++++++ .../cancellation_empty_by.lean.out.expected | 2 + .../cancellation_try_plain.lean | 46 ++++++++++ .../cancellation_try_plain.lean.out.expected | 2 + 12 files changed, 382 insertions(+), 68 deletions(-) create mode 100644 tests/elab/tryOnEmptyBy.lean create mode 100644 tests/elab/try_prelude.lean create mode 100644 tests/server_interactive/cancellation_empty_by.lean create mode 100644 tests/server_interactive/cancellation_empty_by.lean.out.expected create mode 100644 tests/server_interactive/cancellation_try_plain.lean create mode 100644 tests/server_interactive/cancellation_try_plain.lean.out.expected diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean index b094c3fc19..fe4da771f6 100644 --- a/src/Lean/Elab/BuiltinTerm.lean +++ b/src/Lean/Elab/BuiltinTerm.lean @@ -157,7 +157,37 @@ private def getMVarFromUserName (ident : Syntax) : MetaM Expr := do elabTerm b expectedType? | _ => throwUnsupportedSyntax -@[builtin_term_elab byTactic] def elabByTactic : TermElab := fun stx expectedType? => do +register_builtin_option tactic.tryOnEmptyBy : Bool := { + defValue := false + descr := "when an empty `by` block is encountered interactively, run `try?` to suggest \ + a proof (currently disabled by default; may become the default in a future release)" +} + +/-- Returns `true` if `stx` is a `by` expression with an empty tactic body +(not a parse error producing `.missing`). +The structure is: `node byTactic [atom "by", node tacticSeq [node tacticSeq1Indented [node null []]]]` -/ +def isEmptyByBlock (stx : Syntax) : Bool := + stx.getNumArgs == 2 && + stx[1].getNumArgs >= 1 && + stx[1][0].isOfKind ``Lean.Parser.Tactic.tacticSeq1Indented && + stx[1][0].getNumArgs >= 1 && + stx[1][0][0].getNumArgs == 0 && + !stx[1][0][0].isMissing + +/-- Returns `true` if all conditions are met for empty `by` to be elaborated as `try?`: +the body is empty, the option is enabled, we are in an interactive (non-combinator) context, +and the `try?` infrastructure (parser `Lean.Parser.Tactic.tryTrace`) is available — the latter +matters when working on the prelude, before `Init.Try` is imported. -/ +def shouldElabEmptyByAsTry (stx : Syntax) : TermElabM Bool := do + return isEmptyByBlock stx + && tactic.tryOnEmptyBy.get (← getOptions) + && (← read).errToSorry + && (← getEnv).contains `Lean.Parser.Tactic.tryTrace + +/-- Body of the `byTactic` term elaborator: registers a tactic mvar for the body, or +errors when there's no expected type. Shared between `elabByTactic` and +`Lean.Elab.Tactic.Try`'s `elabEmptyByAsTry` so the two paths can't drift. -/ +def elabByTacticCore : TermElab := fun stx expectedType? => do match expectedType? with | some expectedType => -- `by` switches from an exported to a private context, so we must disallow unassigned @@ -168,6 +198,13 @@ private def getMVarFromUserName (ident : Syntax) : MetaM Expr := do tryPostpone throwError ("invalid 'by' tactic, expected type has not been provided") +@[builtin_term_elab byTactic] def elabByTactic : TermElab := fun stx expectedType? => do + -- When the conditions for `try?` on empty `by` are met, skip this elaborator so a later one + -- (in Lean.Elab.Tactic.Try) can handle it with try?. + if (← shouldElabEmptyByAsTry stx) then + throwUnsupportedSyntax + elabByTacticCore stx expectedType? + @[builtin_term_elab noImplicitLambda] def elabNoImplicitLambda : TermElab := fun stx expectedType? => elabTerm stx[1] (mkNoImplicitLambdaAnnotation <$> expectedType?) diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index 76f6656345..0132303d32 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -38,6 +38,12 @@ where -- `stx[0]` is the next tactic step, if any goEven stx := do if stx.getNumArgs == 0 then + -- No more tactic steps, but if the parent still passed us a tactic snapshot + -- bundle (e.g. for an empty `by` body) we must resolve its promise so that + -- consumers walking the snapshot tree (like the language-server info-tree + -- lookup) don't block waiting on a promise nothing else will resolve. + if let some snap := (← readThe Term.Context).tacSnap? then + snap.new.resolve default return let tac := stx[0] /- diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean index 0681e04893..10cedba3ba 100644 --- a/src/Lean/Elab/Tactic/Try.lean +++ b/src/Lean/Elab/Tactic/Try.lean @@ -12,6 +12,7 @@ public import Lean.Elab.Tactic.LibrarySearch public import Lean.Elab.Tactic.Grind.Main public import Lean.Elab.Parallel public meta import Lean.Elab.Command +import Lean.Elab.BuiltinTerm import Init.Omega public section namespace Lean.Elab.Tactic @@ -1009,7 +1010,8 @@ private def wrapSuggestionWithBy (sugg : Tactic.TryThis.Suggestion) : TacticM Ta | _ => return sugg /-- Version of `evalAndSuggest` that wraps tactic suggestions with `by` for term mode. -/ -private def evalAndSuggestWithBy (tk : Syntax) (tac : TSyntax `tactic) (originalMaxHeartbeats : Nat) (config : Try.Config) : TacticM Unit := do +private def evalAndSuggestWithBy (tk : Syntax) (tac : TSyntax `tactic) (originalMaxHeartbeats : Nat) + (config : Try.Config) (footer : MessageData := MessageData.nil) : TacticM Unit := do -- Suppress "Try this" messages from intermediate tactic executions let tac' ← withSuppressedMessages do try @@ -1023,23 +1025,30 @@ private def evalAndSuggestWithBy (tk : Syntax) (tac : TSyntax `tactic) (original -- Wrap each suggestion with `by ` let termSuggestions ← suggestions.mapM wrapSuggestionWithBy if termSuggestions.size == 1 then - Tactic.TryThis.addSuggestion tk termSuggestions[0]! (origSpan? := (← getRef)) + Tactic.TryThis.addSuggestion tk termSuggestions[0]! (origSpan? := (← getRef)) (footer := footer) else - Tactic.TryThis.addSuggestions tk termSuggestions (origSpan? := (← getRef)) + Tactic.TryThis.addSuggestions tk termSuggestions (origSpan? := (← getRef)) (footer := footer) -@[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 +/-- Core implementation of `try?`: focus, collect info, build tactic, evaluate and suggest. +`tk` is the syntax token where "Try this:" appears. The optional `footer` is appended to the +suggestions message (only when `wrapWithBy := true`). -/ +private def elabTryCore (tk : Syntax) (config : Try.Config) (footer : MessageData := MessageData.nil) : + TacticM Unit := + Tactic.focus do withMainContext do let originalMaxHeartbeats ← getMaxHeartbeats withUnlimitedHeartbeats do let goal ← getMainGoal let info ← Try.collect goal config let stx ← mkTryEvalSuggestStx goal info if config.wrapWithBy then - evalAndSuggestWithBy tk stx originalMaxHeartbeats config + evalAndSuggestWithBy tk stx originalMaxHeartbeats config (footer := footer) else evalAndSuggest tk stx originalMaxHeartbeats config + +@[builtin_tactic Lean.Parser.Tactic.tryTrace] def evalTryTrace : Tactic := fun stx => do + match stx with + | `(tactic| try?%$tk $config:optConfig) => + elabTryCore tk (← elabTryConfig config) | _ => throwUnsupportedSyntax @[builtin_tactic Lean.Parser.Tactic.tryTraceWith] def evalTryTraceWith : Tactic := fun stx => do @@ -1055,4 +1064,37 @@ private def evalAndSuggestWithBy (tk : Syntax) (tac : TSyntax `tactic) (original evalAndSuggest tk tac originalMaxHeartbeats config | _ => throwUnsupportedSyntax +open Term in +/-- When the `by` body is empty and `tactic.tryOnEmptyBy` is set, run `try?` for its +informational side effect (the "Try this" suggestions) and then delegate to the normal +`by` elaborator so the empty body still produces an unsolved-goals error. The implicit +mode must not change elaboration behavior beyond emitting messages. +Disabled when `errToSorry` is false (nested in a combinator like `first`), +or when `try?` infrastructure is not yet available (e.g. while building the prelude). + +We register a *second* `builtin_term_elab` for `byTactic` (rather than folding the +gate-and-dispatch into `elabByTactic` directly) because `Lean.Elab.Tactic.Try` already +imports `Lean.Elab.BuiltinTerm`, so the `try?` infrastructure can't be referenced +from `BuiltinTerm.lean` without breaking the dependency direction. The gate in +`elabByTactic` skips this elaborator (via `throwUnsupportedSyntax`) when the `try?` +path doesn't apply. This could be cleaned up later, e.g. via a registered handler ref +in `BuiltinTerm.lean` populated by `Try.lean`. -/ +@[builtin_term_elab byTactic] def elabEmptyByAsTry : TermElab := fun stx expectedType? => do + unless (← shouldElabEmptyByAsTry stx) do + throwUnsupportedSyntax + let some expectedType := expectedType? | do tryPostpone; throwUnsupportedSyntax + -- Run the same body the normal `by` elaborator would. + let mvar ← elabByTacticCore stx expectedType? + let cancelTk ← IO.CancelToken.new + let footer := m!"\n\n(Disable this with `set_option tactic.tryOnEmptyBy false`.)" + let act ← Term.wrapAsyncAsSnapshot (cancelTk? := cancelTk) fun (_ : Unit) => do + let scratch ← mkFreshExprMVar expectedType MetavarKind.syntheticOpaque + try + discard <| Tactic.run scratch.mvarId! <| + withRef stx do elabTryCore stx[0] { wrapWithBy := true } (footer := footer) + catch _ => pure () + let t ← BaseIO.asTask (act ()) + Core.logSnapshotTask { stx? := none, reportingRange := .skip, task := t, cancelTk? := cancelTk } + return mvar + end Lean.Elab.Tactic.Try diff --git a/src/Lean/Meta/Tactic/TryThis.lean b/src/Lean/Meta/Tactic/TryThis.lean index e05435a849..047f4a7969 100644 --- a/src/Lean/Meta/Tactic/TryThis.lean +++ b/src/Lean/Meta/Tactic/TryThis.lean @@ -91,14 +91,15 @@ The parameters are: -/ def addSuggestion (ref : Syntax) (s : Suggestion) (origSpan? : Option Syntax := none) (header : String := "Try this:") (codeActionPrefix? : Option String := none) - (diffGranularity : Hint.DiffGranularity := .none) : CoreM Unit := do + (diffGranularity : Hint.DiffGranularity := .none) + (footer : MessageData := MessageData.nil) : CoreM Unit := do let hintSuggestion := { span? := origSpan? diffGranularity toTryThisSuggestion := s } let suggs ← Hint.mkSuggestionsMessage #[hintSuggestion] ref codeActionPrefix? (forceList := false) - logInfoAt ref m!"{header}{suggs}" + logInfoAt ref m!"{header}{suggs}{footer}" set_option linter.unusedVariables false in /-- Add a list of "try this" suggestions as a single "try these" suggestion. This has two effects: @@ -134,7 +135,8 @@ def addSuggestions (ref : Syntax) (suggestions : Array Suggestion) (origSpan? : Option Syntax := none) (header : String := "Try these:") (style? : Option SuggestionStyle := none) (codeActionPrefix? : Option String := none) - (diffGranularity : Hint.DiffGranularity := .none) : CoreM Unit := do + (diffGranularity : Hint.DiffGranularity := .none) + (footer : MessageData := MessageData.nil) : CoreM Unit := do if suggestions.isEmpty then throwErrorAt ref "No suggestions available" let hintSuggestions := suggestions.map fun s => { span? := origSpan? @@ -142,7 +144,7 @@ def addSuggestions (ref : Syntax) (suggestions : Array Suggestion) toTryThisSuggestion := s } let suggs ← Hint.mkSuggestionsMessage hintSuggestions ref codeActionPrefix? (forceList := true) - logInfoAt ref m!"{header}{suggs}" + logInfoAt ref m!"{header}{suggs}{footer}" /-! # Tactic-specific widget hooks -/ /-- diff --git a/src/Lean/Server/Test/Cancel.lean b/src/Lean/Server/Test/Cancel.lean index e6fb243383..03358640ac 100644 --- a/src/Lean/Server/Test/Cancel.lean +++ b/src/Lean/Server/Test/Cancel.lean @@ -192,39 +192,6 @@ elab_rules : tactic dbg_trace "blocked!" log "blocked" -/-! ## Helpers for end-to-end testing of cancellation propagation -/ - -meta initialize blockUntilCancelledOnce : IO.Ref (Std.HashMap String (Task Unit)) ← IO.mkRef {} - -/-- -Tactic for testing cancellation propagation. On the first invocation for a given `