Documentation

Lean.Server.Test.Cancel

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
    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
        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.
            Instances For