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.unblockedCancelTkRef : IO.Ref (Option 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.

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)

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)

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.

Equations

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

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.

Equations

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

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

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

Like wait_for_main_cancel_once_async but for commands. Takes a num parameter so that its syntax can be changed (via change:) to trigger re-elaboration. Sends "blocked" as a diagnostic and spawns an async task that waits for the command's cancellation token to be set.

Equations

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

opaque Lean.Server.Test.Cancel.testTasksRef : IO.Ref (Std.HashMap String (Task (Option Unit)))

Registry of label-keyed Task (Option Unit) values for use by mkTestTask and wait_for_test_task. The stored task is prom.result? of the promise returned by mkTestTask; the registry itself does not keep that promise alive, so if no other reference exists, the promise drops and the task fires none.

def Lean.Server.Test.Cancel.mkTestTask (label : String) : BaseIO (Option (IO.Promise Unit))

Register a fresh test task under label, returning the underlying IO.Promise. Returns none if a task is already registered under label. The caller is responsible for keeping the returned promise alive and arranging its resolution -- typically by capturing it in a cancelTk.onSet closure that calls prom.resolve.

Equations

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

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

Block until the test task named label fires. Prints a diagnostic to stderr if the underlying promise was dropped without resolution, or if no task is registered for label. The diagnostic uses stderr rather than throwError so that the failure is visible even when this tactic is evaluated inside try? (or any other combinator that swallows tactic errors).

Equations

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

opaque Lean.Server.Test.Cancel.syncPromisesRef : IO.Ref (Std.HashMap String (IO.Promise Unit))

Registry of label-keyed IO.Promise Unit for synchronization between cooperating tactics/elaborators in tests. The promise is kept alive by the ref itself, so prom.result? only fires on explicit resolveSyncPromise -- there is no drop signal. Distinct from testTasksRef, which stores only the Task side and relies on caller liveness to detect dropped-without-resolved.

def Lean.Server.Test.Cancel.getSyncPromise (label : String) : BaseIO (IO.Promise Unit)

Return the sync promise for label, creating it if no entry exists. All callers receive the same promise.

Equations

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

def Lean.Server.Test.Cancel.resolveSyncPromise (label : String) : BaseIO Unit

Resolve the sync promise for label. Idempotent (subsequent resolves are no-ops).

Equations

• Lean.Server.Test.Cancel.resolveSyncPromise label = do let __do_lift ← Lean.Server.Test.Cancel.getSyncPromise label IO.Promise.resolve () __do_lift

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

Block until resolveSyncPromise label has been called. Direct IO.wait, no polling.

Equations

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

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

Tactic for testing cancellation propagation. On the first invocation for a given <label>, prints <label>: blocked to stderr, resolves the sync promise <label> (so a separate theorem can gate the runner's waitFor on this invocation having actually started), and loops on Core.checkInterrupted until the tactic's cancel token fires (at which point the loop throws and finally resolves the shared task). Subsequent invocations (e.g. on re-elaboration) wait on that task: they return as soon as the first invocation has actually exited the loop, and hang otherwise. So if cancellation propagates correctly, the test completes; if propagation is broken, the second invocation's wait blocks forever and the test hangs (timeout = failure).

Equations

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