Task creation utilities for Lean's tactic monads.

This file provides asTask and asTask' functions for various monads (CoreM, MetaM, TermElabM, TacticM), which convert monadic computations into tasks that run in parallel while preserving state.

Each asTask function returns:

• a cancellation hook and
• a Task containing a monadic value with the cached result and updated state

The asTask' variants omit the cancellation hook for convenience.

Note: Calling IO.cancel on t.map f does not cancel t, so these functions are careful to construct cancellation hooks connected to the underlying task rather than various maps of it.

def Lean.Core.CoreM.asTask {α : Type} (t : CoreM α) : CoreM (BaseIO Unit × Task (CoreM α))

Given a monadic value in CoreM, creates a task that runs it in the current state, returning

• a cancellation hook and
• a monadic value with the cached result (and subsequent state as it was after running).

The task is run with a fresh CancelToken in its context, so it can detect cancellation via Core.checkInterrupted. The cancellation hook sets this token.

Uses Core.wrapAsync internally to properly handle name generators and heartbeats.

Note: We only set the cancel token and don't call IO.cancel task. We're uncertain whether IO.cancel is also necessary - it may be required for tasks that use IO.checkCanceled instead of Core.checkInterrupted.

def Lean.Core.CoreM.asTask' {α : Type} (t : CoreM α) : CoreM (Task (CoreM α))

Given a monadic value in CoreM, creates a task that runs it in the current state, returning a monadic value with the cached result (and subsequent state as it was after running).

def Lean.Meta.MetaM.asTask {α : Type} (t : MetaM α) : MetaM (BaseIO Unit × Task (MetaM α))

Given a monadic value in MetaM, creates a task that runs it in the current state, returning

• a cancellation hook and
• a monadic value with the cached result (and subsequent state as it was after running).

def Lean.Meta.MetaM.asTask' {α : Type} (t : MetaM α) : MetaM (Task (MetaM α))

Given a monadic value in MetaM, creates a task that runs it in the current state, returning a monadic value with the cached result (and subsequent state as it was after running).

def Lean.Elab.Term.TermElabM.asTask {α : Type} (t : TermElabM α) : TermElabM (BaseIO Unit × Task (TermElabM α))

Given a monadic value in TermElabM, creates a task that runs it in the current state, returning

• a cancellation hook and
• a monadic value with the cached result (and subsequent state as it was after running).

def Lean.Elab.Term.TermElabM.asTask' {α : Type} (t : TermElabM α) : TermElabM (Task (TermElabM α))

Given a monadic value in TermElabM, creates a task that runs it in the current state, returning a monadic value with the cached result (and subsequent state as it was after running).

def Lean.Elab.Tactic.TacticM.asTask {α : Type} (t : TacticM α) : TacticM (BaseIO Unit × Task (TacticM α))

Given a monadic value in TacticM, creates a task that runs it in the current state, returning

• a cancellation hook and
• a monadic value with the cached result (and subsequent state as it was after running).

def Lean.Elab.Tactic.TacticM.asTask' {α : Type} (t : TacticM α) : TacticM (Task (TacticM α))

Given a monadic value in TacticM, creates a task that runs it in the current state, returning a monadic value with the cached result (and subsequent state as it was after running).