Helpers for testing cancellation in interactive tests. Put here because of initialize restrictions and to avoid repeated elaboration overhead per test.

opaque Lean.Server.Test.Cancel.onceRef : IO.Ref (Option (Task Unit))

def Lean.Server.Test.Cancel.tacticWait_for_cancel_once : ParserDescr

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.

opaque Lean.Server.Test.Cancel.unblockedCancelTk : IO.CancelToken

def Lean.Server.Test.Cancel.tacticWait_for_unblock : ParserDescr

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.

def Lean.Server.Test.Cancel.tacticWait_for_unblock_async : ParserDescr

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.

def Lean.Server.Test.Cancel.tacticUnblock : ParserDescr

Unblocks a wait_for_unblock* task.

def Lean.Server.Test.Cancel.tacticWait_for_cancel_once_async : ParserDescr

Like wait_for_cancel_once but does the waiting in a separate task and waits for its cancellation.

def Lean.Server.Test.Cancel.tacticWait_for_main_cancel_once_async : ParserDescr

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.