This PR resurrects the tests about cancellation of `try?` tactics.
They were flaky before. By introducing an option
(`debug.tactic.try.onlyUserSuggestions`) to make these tests not run
`exact?` as part of `try?`, and thus be generally faster and use less
memory, the flakiness seems to have disappeared, at least in
non-`master` testing. We’ll see.
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR fixes issues with flaky cancellation_empty_by test.
The original test gated the runner's `waitFor: blocked` on `t1`'s
`wait_for_cancel_once_async`, which had no causal relationship to
`tracerSuggestion` having actually run inside the empty-`by` snapshot
task. On CI under load the runner could trigger the insert before
`tracerSuggestion` registered its `onSet` callback, leading to
intermittent timeouts.
Add a label-keyed `IO.Promise` registry (`syncPromisesRef`) plus
`getSyncPromise` / `resolveSyncPromise` primitives and a
`wait_for_sync <label>` tactic to `Lean.Server.Test.Cancel`. The
empty-`by` test's `tracerSuggestion` now resolves a sync promise
after registering its onSet, and `t1` waits on that promise before
emitting `blocked`. The empty-`by` example must precede `t1` because
`try?` inside the snapshot task synchronously waits on prior pending
async theorem bodies during library search (likely a separate upstream
issue); with that ordering the test is fully deterministic.
`t1` also drops `wait_for_cancel_once_async` in favor of plain
`trace "blocked"`. The test now also `dbg_trace`s at each sync point
(`tracerSuggestion ready`, `sync received`, `cancelTokenSet`) so the
.out.expected captures the deterministic execution sequence.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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>
