2229b077d6
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 <noreply@anthropic.com>
80 lines
4 KiB
Text
80 lines
4 KiB
Text
-- This tests the `#info_trees in` command.
|
|
-- If it proves too fragile to test the result using `#guard_msgs`,
|
|
-- it is fine to simply remove the `#guard_msgs` and expected output.
|
|
|
|
/--
|
|
info: • [Command] @ ⟨80, 0⟩-⟨80, 40⟩ @ Lean.Elab.Command.elabDeclaration
|
|
• [Term] Nat : Type @ ⟨80, 15⟩-⟨80, 18⟩ @ Lean.Elab.Term.elabIdent
|
|
• [Completion-Id] Nat : some Sort.{?_uniq.1} @ ⟨80, 15⟩-⟨80, 18⟩
|
|
• [Term] Nat : Type @ ⟨80, 15⟩-⟨80, 18⟩
|
|
• [Term] n (isBinder := true) : Nat @ ⟨80, 11⟩-⟨80, 12⟩
|
|
• [Term] 0 ≤ n : Prop @ ⟨80, 22⟩-⟨80, 27⟩ @ «_aux_Init_Notation___macroRules_term_≤__2»
|
|
• [MacroExpansion]
|
|
0 ≤ n
|
|
===>
|
|
binrel% LE.le✝ 0 n
|
|
• [Term] 0 ≤ n : Prop @ ⟨80, 22⟩†-⟨80, 27⟩† @ Lean.Elab.Term.Op.elabBinRel
|
|
• [Term] 0 ≤ n : Prop @ ⟨80, 22⟩†-⟨80, 27⟩†
|
|
• [Completion-Id] LE.le✝ : none @ ⟨80, 22⟩†-⟨80, 27⟩†
|
|
• [Term] 0 : Nat @ ⟨80, 22⟩-⟨80, 23⟩ @ Lean.Elab.Term.elabNumLit
|
|
• [Term] n : Nat @ ⟨80, 26⟩-⟨80, 27⟩ @ Lean.Elab.Term.elabIdent
|
|
• [Completion-Id] n : none @ ⟨80, 26⟩-⟨80, 27⟩
|
|
• [Term] n : Nat @ ⟨80, 26⟩-⟨80, 27⟩
|
|
• [CustomInfo(Lean.Elab.Term.AsyncBodyInfo)]
|
|
• [Term] n (isBinder := true) : Nat @ ⟨80, 11⟩-⟨80, 12⟩
|
|
• [CustomInfo(Lean.Elab.Term.BodyInfo)]
|
|
• [PartialTerm] @ ⟨80, 31⟩-⟨80, 40⟩ @ Lean.Elab.Tactic.Try.elabEmptyByAsTry
|
|
• [Tactic] @ ⟨80, 31⟩-⟨80, 40⟩
|
|
(Term.byTactic
|
|
"by"
|
|
(Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" (Tactic.optConfig []) [])])))
|
|
before ⏎
|
|
n : Nat
|
|
⊢ 0 ≤ n
|
|
after no goals
|
|
• [Tactic] @ ⟨80, 31⟩-⟨80, 33⟩
|
|
"by"
|
|
before ⏎
|
|
n : Nat
|
|
⊢ 0 ≤ n
|
|
after no goals
|
|
• [Tactic] @ ⟨80, 34⟩-⟨80, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq
|
|
(Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" (Tactic.optConfig []) [])]))
|
|
before ⏎
|
|
n : Nat
|
|
⊢ 0 ≤ n
|
|
after no goals
|
|
• [Tactic] @ ⟨80, 34⟩-⟨80, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented
|
|
(Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" (Tactic.optConfig []) [])])
|
|
before ⏎
|
|
n : Nat
|
|
⊢ 0 ≤ n
|
|
after no goals
|
|
• [Tactic] @ ⟨80, 34⟩-⟨80, 40⟩ @ Lean.Elab.LibrarySearch.evalExact
|
|
(Tactic.exact? "exact?" (Tactic.optConfig []) [])
|
|
before ⏎
|
|
n : Nat
|
|
⊢ 0 ≤ n
|
|
after no goals
|
|
• [Tactic] @ ⟨80, 34⟩†-⟨80, 40⟩† @ Lean.Elab.Tactic.evalExact
|
|
(Tactic.exact "exact" (Term.app `Nat.zero_le [`n]))
|
|
before ⏎
|
|
n : Nat
|
|
⊢ 0 ≤ n
|
|
after no goals
|
|
• [Term] Nat.zero_le n : 0 ≤ n @ ⟨1, 1⟩†-⟨1, 1⟩† @ Lean.Elab.Term.elabApp
|
|
• [Completion-Id] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.47.3 @ ⟨1, 0⟩†-⟨1, 0⟩†
|
|
• [Term] Nat.zero_le : ∀ (n : Nat), 0 ≤ n @ ⟨1, 0⟩†-⟨1, 0⟩†
|
|
• [Term] n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† @ Lean.Elab.Term.elabIdent
|
|
• [Completion-Id] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩†
|
|
• [Term] n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩†
|
|
• [CustomInfo(Lean.Meta.Tactic.TryThis.TryThisInfo)]
|
|
• [Term] t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨80, 8⟩-⟨80, 9⟩
|
|
• [Term] t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨80, 8⟩-⟨80, 9⟩
|
|
---
|
|
info: Try this:
|
|
[apply] exact Nat.zero_le n
|
|
-/
|
|
#guard_msgs in
|
|
#info_trees in
|
|
theorem t (n : Nat) : 0 ≤ n := by exact?
|