Helpers for testing cancellation in interactive tests. Put here because of initialize
restrictions
and to avoid repeated elaboration overhead per test.
On first invocation, sends a diagnostics "blocked", blocks until cancelled, and then eprints "cancelled!"; further invocations complete when this wait is done but do not wait for their own cancellation. Thus all document versions should complete strictly after the printing has completed and we avoid terminating the server too early to see the message.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Waits for unblock
to be called, which is expected to happen in a subsequent document version that
does not invalidate this tactic. Complains if cancellation token was set before unblocking, i.e. if
the tactic was invalidated after all.
Equations
- Lean.Server.Test.Cancel.tacticWait_for_unblock = Lean.ParserDescr.node `Lean.Server.Test.Cancel.tacticWait_for_unblock 1024 (Lean.ParserDescr.nonReservedSymbol "wait_for_unblock" false)
Instances For
Spawns a logSnapshotTask
that waits for unblock
to be called, which is expected to happen in a
subsequent document version that does not invalidate this tactic. Complains if cancellation token
was set before unblocking, i.e. if the tactic was invalidated after all.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Unblocks a wait_for_unblock*
task.
Equations
- Lean.Server.Test.Cancel.tacticUnblock = Lean.ParserDescr.node `Lean.Server.Test.Cancel.tacticUnblock 1024 (Lean.ParserDescr.nonReservedSymbol "unblock" false)
Instances For
Like wait_for_cancel_once
but does the waiting in a separate task and waits for its
cancellation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Like wait_for_cancel_once_async
but waits for the main thread's cancellation token. This is useful
to test main thread cancellation in non-incremental contexts because we otherwise wouldn't be able
to send out the "blocked" message from there.
Equations
- One or more equations did not get rendered due to their size.