6279ae98c7
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>
87 lines
3.4 KiB
Text
87 lines
3.4 KiB
Text
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
|