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 replaces the `check_cancel` two-way coordination protocol used
by
`tests/server_interactive/cancellation_par.lean` with a single tactic
`block_until_cancelled "<label>"`. The first invocation for a label
registers
a promise, prints `<label>: blocked`, and loops on
`Core.checkInterrupted`
until the cancel token fires (then `finally` resolves the promise). Any
later
invocation for the same label waits on that promise — so the test only
terminates if the first invocation actually exited the loop. If
cancellation
fails to propagate, the second invocation's `IO.wait` blocks forever and
the
test hangs (timeout = failure), with no false-success path.
The test was disabled in `tests/CMakeLists.txt` due to flakiness in the
old
two-way protocol; this PR re-enables it. Verified that reverting #13428
makes the test deadlock as expected.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
This PR fixes parallel tactic combinators (`attempt_all_par`,
`first_par`) leaking their subtasks when the server cancels elaboration
on re-elaboration. Subtasks spawned via `CoreM.asTask` (and its
`MetaM`/`TermElabM`/`TacticM` variants) get a fresh `IO.CancelToken`,
which previously had no link to the parent token; `cancelRec` would set
the command-level token but the children kept running.
The fix is one line in `CoreM.asTask`: when a parent token is in scope,
register `cancelToken.set` as an `onSet` callback on the parent.
Server-level cancellation now flows down to every parallel subtask, and
`Core.checkInterrupted` inside the child sees the token set as expected.
Fixes#13300.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `try? => tac` syntax that runs `evalSuggest` directly on
a given tactic, useful for testing the `try?` machinery in isolation. It
also adds a server_interactive test (`cancellation_par.lean`) that
demonstrates a cancellation bug with parallel tactic combinators.
The test contrasts three combinators:
- **`first`** (sequential): cancellation works correctly — the tactic
runs on the main elaboration thread and shares its cancel token.
- **`attempt_all_par`** (parallel): cancellation is broken — the subtask
spawned via `asTask` gets a fresh cancel token that is never set on
re-elaboration.
- **`first_par`** (parallel): same bug as `attempt_all_par`.
The test uses a `check_cancel <label>` helper tactic that detects leaked
cancel tokens without any timing dependency: the second invocation (from
re-elaboration) signals the first, which then checks whether its cancel
token was set.
Related issue: #13300
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
