From 6279ae98c7735e8fb8032cc6f8342cd6e9f51127 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 13 May 2026 15:54:48 +0200 Subject: [PATCH] test: resurrect try cancellation tests (#13707) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- src/Lean/Elab/Tactic/Try.lean | 41 ++++++--- .../cancellation_empty_by.lean | 87 +++++++++++++++++++ .../cancellation_empty_by.lean.out.expected | 5 ++ .../server_interactive/cancellation_par.lean | 81 +++++++++++++++++ .../cancellation_par.lean.out.expected | 3 + 5 files changed, 205 insertions(+), 12 deletions(-) create mode 100644 tests/server_interactive/cancellation_empty_by.lean create mode 100644 tests/server_interactive/cancellation_empty_by.lean.out.expected create mode 100644 tests/server_interactive/cancellation_par.lean create mode 100644 tests/server_interactive/cancellation_par.lean.out.expected diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean index 10cedba3ba..af3d5a2804 100644 --- a/src/Lean/Elab/Tactic/Try.lean +++ b/src/Lean/Elab/Tactic/Try.lean @@ -21,6 +21,15 @@ open Meta A **very** simple `try?` tactic implementation. -/ +register_builtin_option debug.tactic.try.onlyUserSuggestions : Bool := { + defValue := false + descr := "if set, `try?` skips its built-in suggestion branches \ + (simple, simp, grind, simp_all, induction/fun_induction, exact?) and only \ + runs tactics produced by user-registered `@[try_suggestion]` generators. \ + Primarily intended for tests that want to exercise the `try?` machinery \ + without paying for library search and other expensive default branches." +} + declare_config_elab elabTryConfig Try.Config namespace Try @@ -966,18 +975,7 @@ private def mkAllIndStx (info : Try.Info) (cont : TSyntax `tactic) : MetaM (TSyn /-- Returns tactic for `evalAndSuggest` (unsafe version that can evaluate user generators) -/ private unsafe def mkTryEvalSuggestStxUnsafe (goal : MVarId) (info : Try.Info) : MetaM (TSyntax `tactic) := do - let simple ← mkSimpleTacStx - let simp ← mkSimpStx - let grind ← mkGrindStx info - - let atomic ← `(tactic| attempt_all_par | $simple:tactic | $simp:tactic | $grind:tactic | simp_all) - let atomicSuggestions ← mkAtomicWithSuggestionsStx - let atomicOrSuggestions ← `(tactic| first | $atomic:tactic | $atomicSuggestions:tactic) - let funInds ← mkAllFunIndStx info atomicOrSuggestions - let inds ← mkAllIndStx info atomicOrSuggestions - let extra ← `(tactic| (intros; first | $simple:tactic | $simp:tactic | exact?)) - - -- Collect user-defined suggestions (runs after built-in tactics) + -- Collect user-defined suggestions. let userEntries := trySuggestionExtension.getState (← getEnv) let mut userTactics := #[] for entry in userEntries do @@ -991,6 +989,25 @@ private unsafe def mkTryEvalSuggestStxUnsafe (goal : MVarId) (info : Try.Info) : catch e => logWarning m!"try_suggestion generator {entry.name} failed: {e.toMessageData}" + if debug.tactic.try.onlyUserSuggestions.get (← getOptions) then + -- Bypass built-in branches entirely; only run user-registered tactics. + if userTactics.isEmpty then + return ← `(tactic| + fail "debug.tactic.try.onlyUserSuggestions is set but no user suggestions were produced") + else + return ← `(tactic| attempt_all_par $[| $userTactics:tactic]*) + + let simple ← mkSimpleTacStx + let simp ← mkSimpStx + let grind ← mkGrindStx info + + let atomic ← `(tactic| attempt_all_par | $simple:tactic | $simp:tactic | $grind:tactic | simp_all) + let atomicSuggestions ← mkAtomicWithSuggestionsStx + let atomicOrSuggestions ← `(tactic| first | $atomic:tactic | $atomicSuggestions:tactic) + let funInds ← mkAllFunIndStx info atomicOrSuggestions + let inds ← mkAllIndStx info atomicOrSuggestions + let extra ← `(tactic| (intros; first | $simple:tactic | $simp:tactic | exact?)) + -- Build final tactic: built-ins first, then user suggestions as fallback if userTactics.isEmpty then `(tactic| first | $atomic:tactic | $atomicSuggestions:tactic | $funInds:tactic | $inds:tactic | $extra:tactic) diff --git a/tests/server_interactive/cancellation_empty_by.lean b/tests/server_interactive/cancellation_empty_by.lean new file mode 100644 index 0000000000..ac84951b43 --- /dev/null +++ b/tests/server_interactive/cancellation_empty_by.lean @@ -0,0 +1,87 @@ +import Lean.Server.Test.Cancel +import Lean.Elab.Tactic.Try +open Lean Lean.Meta Lean.Elab Lean.Elab.Term Lean.Elab.Tactic +open Lean.Server.Test.Cancel + +-- Diagnostic anchor: synchronous, fires exactly once at command-elab time +-- before any async task is spawned by the rest of the file. If a CI / stress +-- failure shows this line in `.out.produced`, the file worker at least got +-- past imports. +#eval (IO.eprintln "test: imports done" : IO Unit) + +/-! +Test that `cancelRec` reaches the snapshot task spawned by +`elabEmptyByAsTry` on re-elaboration. + +Chronological flow: +1. Empty-`by` example elaborates; `elabEmptyByAsTry` spawns a snapshot + task with its own cancel token and returns. +2. The snapshot task's `try?` calls `tracerSuggestion`, which: + - registers test task `"cancelTokenSet"`, + - registers `cancelTk.onSet` to resolve it, + - resolves sync promise `"tracerSuggestion"`, + - returns `wait_for_test_task "cancelTokenSet"` as the candidate. +3. `try?` evaluates the candidate; it blocks on the test task. +4. `t1` elaborates: `wait_for_sync "tracerSuggestion"` returns + immediately, `trace "blocked"` emits the diagnostic. +5. Runner inserts `; skip`, triggers re-elab; `cancelRec` sets the + cancel token; `onSet` resolves the test task; the candidate's wait + returns; the snapshot task body completes. + +Failure modes: +- `cancelTk? := none` to `Core.logSnapshotTask`: `cancelRec` cannot + reach the cancel token, the wait blocks, runner times out. +- `cancelTk? := none` to `wrapAsyncAsSnapshot`: `tracerSuggestion` + sees no cancel token, doesn't register `onSet`; the promise drops; + `wait_for_test_task` surfaces a `task dropped` diagnostic. + +Ordering note: the empty-`by` example must precede `t1` because `try?` +inside the snapshot task library-searches the environment in a way +that synchronously waits on prior pending async theorem bodies. With +`t1` first, its `wait_for_sync` would block the snapshot's `try?`, +deadlocking. Likely a separate upstream issue. +-/ + +namespace TestEmptyBy + +opaque UnsolvableProp : Prop + +@[try_suggestion] +def tracerSuggestion (_goal : MVarId) (_info : Try.Info) : + MetaM (Array (TSyntax `tactic)) := do + -- Keep dbg_trace output here minimal and gated to the first invocation: + -- this function runs in the snapshot task's stderr buffer, which interleaves + -- non-deterministically with the main elab thread's output. Every additional + -- trace point adds a potential race in `.out.expected`. + if let some prom ← mkTestTask "cancelTokenSet" then + if let some cancelTk := (← readThe Core.Context).cancelTk? then + cancelTk.onSet do + dbg_trace "cancelTokenSet" + prom.resolve () + else + dbg_trace "tracerSuggestion: no cancel token (unexpected -- test setup wrong?)" + dbg_trace "tracerSuggestion ready" + resolveSyncPromise "tracerSuggestion" + return #[← `(tactic| wait_for_test_task "cancelTokenSet")] + +end TestEmptyBy + +set_option tactic.tryOnEmptyBy true +-- Skip the expensive built-in `try?` branches (`simp`/`grind`/`exact?`/…). The +-- test only cares about the user-registered `tracerSuggestion` running inside +-- the snapshot task; the library-search branches are pure overhead here. +set_option debug.tactic.try.onlyUserSuggestions true + +example : True := by + trivial + --^ waitFor: blocked + --^ insert: "; skip" + --^ sync + +example : TestEmptyBy.UnsolvableProp := by + +theorem t1 : True := by + wait_for_sync "tracerSuggestion" + dbg_trace "sync received" + trace "blocked" + trivial diff --git a/tests/server_interactive/cancellation_empty_by.lean.out.expected b/tests/server_interactive/cancellation_empty_by.lean.out.expected new file mode 100644 index 0000000000..926e3e7dfe --- /dev/null +++ b/tests/server_interactive/cancellation_empty_by.lean.out.expected @@ -0,0 +1,5 @@ +test: imports done +cancelTokenSet +tracerSuggestion ready +sync received +sync received diff --git a/tests/server_interactive/cancellation_par.lean b/tests/server_interactive/cancellation_par.lean new file mode 100644 index 0000000000..3bf057628f --- /dev/null +++ b/tests/server_interactive/cancellation_par.lean @@ -0,0 +1,81 @@ +import Lean.Server.Test.Cancel +open Lean.Server.Test.Cancel + +/-! +Test that cancellation propagates into parallel tactic combinators (`attempt_all_par`, +`first_par`). + +Per section, chronological flow: +1. `theorem t` elaborates; its body runs `try? => | block_until_cancelled ""`, + which on the first invocation registers test task `""`, resolves sync promise `""`, + and enters a `Core.checkInterrupted` loop. +2. The gate theorem (`tGate`) elaborates; `wait_for_sync ""` returns immediately (sync was + resolved in step 1), `trace "blocked"` emits the diagnostic the runner is waiting for. +3. Runner inserts `; skip`, triggers re-elab; `cancelRec` walks `t`'s snapshot tree, setting + the cancel token of the `block_until_cancelled` subtask. The loop's `Core.checkInterrupted` + throws, the `finally` resolves the test task, the second invocation's wait returns. + +Section 1 uses sequential `first`; sections 2 and 3 use the parallel combinators +`attempt_all_par` and `first_par`, which spawn the inner tactic on a fresh `asTask` cancel +token. The fix in `CoreM.asTask` (#13428) propagates the parent token to those subtasks; +without it, `cancelRec` cannot reach the subtask's cancel token and the test times out. +-/ + +/-! ## Sequential `first` -/ + +example : True := by + trivial + --^ waitFor: blocked + --^ insert: "; skip" + --^ sync + +theorem t : True := by + try? => first + | block_until_cancelled "first" + +theorem tGate : True := by + wait_for_sync "first" + trace "blocked" + trivial + +-- RESET +import Lean.Server.Test.Cancel +open Lean.Server.Test.Cancel + +/-! ## Parallel `attempt_all_par` -/ + +example : True := by + trivial + --^ waitFor: blocked + --^ insert: "; skip" + --^ sync + +theorem t : True := by + try? => attempt_all_par + | block_until_cancelled "attempt_all_par" + +theorem tGate : True := by + wait_for_sync "attempt_all_par" + trace "blocked" + trivial + +-- RESET +import Lean.Server.Test.Cancel +open Lean.Server.Test.Cancel + +/-! ## Parallel `first_par` -/ + +example : True := by + trivial + --^ waitFor: blocked + --^ insert: "; skip" + --^ sync + +theorem t : True := by + try? => first_par + | block_until_cancelled "first_par" + +theorem tGate : True := by + wait_for_sync "first_par" + trace "blocked" + trivial diff --git a/tests/server_interactive/cancellation_par.lean.out.expected b/tests/server_interactive/cancellation_par.lean.out.expected new file mode 100644 index 0000000000..b49bf2d8f4 --- /dev/null +++ b/tests/server_interactive/cancellation_par.lean.out.expected @@ -0,0 +1,3 @@ +first: blocked +attempt_all_par: blocked +first_par: blocked