432d11541b
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>
67 lines
1.8 KiB
Text
67 lines
1.8 KiB
Text
import Lean.Server.Test.Cancel
|
|
open Lean.Server.Test.Cancel
|
|
|
|
/-!
|
|
Test contrasting cancellation behavior between sequential and parallel combinators.
|
|
|
|
Each section uses `check_cancel <label>`: on first invocation it loops checking
|
|
`Core.checkInterrupted`, waiting for the second invocation (triggered by re-elaboration) to
|
|
signal it. If the cancel token was properly set, `checkInterrupted` fires first and the tactic
|
|
is interrupted. Otherwise the signal arrives, the tactic finds `cancelTk` unset, and prints
|
|
`"{label}: leaked!"`.
|
|
|
|
**Sequential `first`** (section 1): runs on the main elaboration thread, sharing the command's
|
|
cancel token. On re-elaboration, `checkInterrupted` fires — no leak.
|
|
|
|
**Parallel `attempt_all_par`** (section 2): runs in a subtask via `asTask` with its own fresh
|
|
cancel token. Nobody sets that token on re-elaboration — **leak**.
|
|
|
|
**Parallel `first_par`** (section 3): same bug as `attempt_all_par`.
|
|
-/
|
|
|
|
/-! ## Sequential `first`: cancellation works -/
|
|
|
|
example : True := by
|
|
trivial
|
|
--^ waitFor: blocked
|
|
--^ insert: "; skip"
|
|
--^ sync
|
|
|
|
theorem t : True := by
|
|
wait_for_cancel_once_async
|
|
try? => first
|
|
| check_cancel first
|
|
|
|
-- RESET
|
|
import Lean.Server.Test.Cancel
|
|
open Lean.Server.Test.Cancel
|
|
|
|
/-! ## Parallel `attempt_all_par`: cancellation is broken -/
|
|
|
|
example : True := by
|
|
trivial
|
|
--^ waitFor: blocked
|
|
--^ insert: "; skip"
|
|
--^ sync
|
|
|
|
theorem t : True := by
|
|
wait_for_cancel_once_async
|
|
try? => attempt_all_par
|
|
| check_cancel attempt_all_par
|
|
|
|
-- RESET
|
|
import Lean.Server.Test.Cancel
|
|
open Lean.Server.Test.Cancel
|
|
|
|
/-! ## Parallel `first_par`: cancellation is broken -/
|
|
|
|
example : True := by
|
|
trivial
|
|
--^ waitFor: blocked
|
|
--^ insert: "; skip"
|
|
--^ sync
|
|
|
|
theorem t : True := by
|
|
wait_for_cancel_once_async
|
|
try? => first_par
|
|
| check_cancel first_par
|