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>
8 lines
104 B
Text
8 lines
104 B
Text
blocked!
|
|
cancelled!
|
|
blocked!
|
|
cancelled!
|
|
attempt_all_par: leaked!
|
|
blocked!
|
|
cancelled!
|
|
first_par: leaked!
|