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.

Equations

• One or more equations did not get rendered due to their size.

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

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.

Equations

• One or more equations did not get rendered due to their size.

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

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)