structure

Task.{u} (α : Type u) : Type u

Task α is a primitive for asynchronous computation. It represents a computation that will resolve to a value of type α, possibly being computed on another thread. This is similar to Future in Scala, Promise in Javascript, and JoinHandle in Rust.

The tasks have an overridden representation in the runtime.

Constructor

Task.pure.{u}

Task.pure (a : α) constructs a task that is already resolved with value a.

Fields

get : α

If task : Task α then task.get : α blocks the current thread until the value is available, and then returns the result of the task.

def

Task.spawn.{u} {α : Type u} (fn : Unit → α)
  (prio : Task.Priority :=
    Task.Priority.default) :
  Task α

spawn fn : Task α constructs and immediately launches a new task for evaluating the function fn () : α asynchronously.

prio, if provided, is the priority of the task.

def

Task.Priority : Type

Task priority. Tasks with higher priority will always be scheduled before ones with lower priority.

def

Task.Priority.default : Task.Priority

The default priority for spawned tasks, also the lowest priority: 0.

def

Task.Priority.max : Task.Priority

The highest regular priority for spawned tasks: 8.

Spawning a task with a priority higher than Task.Priority.max is not an error but will spawn a dedicated worker for the task, see Task.Priority.dedicated. Regular priority tasks are placed in a thread pool and worked on according to the priority order.

def

Task.Priority.dedicated : Task.Priority

Any priority higher than Task.Priority.max will result in the task being scheduled immediately on a dedicated thread. This is particularly useful for long-running and/or I/O-bound tasks since Lean will by default allocate no more non-dedicated workers than the number of cores to reduce context switches.

def

Task.get.{u} {α : Type u} (self : Task α) : α

If task : Task α then task.get : α blocks the current thread until the value is available, and then returns the result of the task.

opaque

IO.wait {α : Type} (t : Task α) : BaseIO α

Wait for the task to finish, then return its result.

opaque

IO.waitAny {α : Type} (tasks : List (Task α))
  (h : tasks.length > 0 := by
    exact Nat.zero_lt_succ _) :
  BaseIO α

Wait until any of the tasks in the given list has finished, then return its result.

opaque

BaseIO.mapTask.{u_1} {α : Type u_1} {β : Type}
  (f : α → BaseIO β) (t : Task α)
  (prio : Task.Priority :=
    Task.Priority.default)
  (sync : Bool := false) : BaseIO (Task β)

See BaseIO.asTask.

def

EIO.mapTask.{u_1} {α : Type u_1} {ε β : Type}
  (f : α → EIO ε β) (t : Task α)
  (prio : Task.Priority :=
    Task.Priority.default)
  (sync : Bool := false) :
  BaseIO (Task (Except ε β))

EIO specialization of BaseIO.mapTask.

def

IO.mapTask.{u_1} {α : Type u_1} {β : Type}
  (f : α → IO β) (t : Task α)
  (prio : Task.Priority :=
    Task.Priority.default)
  (sync : Bool := false) :
  BaseIO (Task (Except IO.Error β))

IO specialization of EIO.mapTask.

def

BaseIO.mapTasks.{u_1} {α : Type u_1} {β : Type}
  (f : List α → BaseIO β)
  (tasks : List (Task α))
  (prio : Task.Priority :=
    Task.Priority.default)
  (sync : Bool := false) : BaseIO (Task β)

def

EIO.mapTasks.{u_1} {α : Type u_1} {ε β : Type}
  (f : List α → EIO ε β) (tasks : List (Task α))
  (prio : Task.Priority :=
    Task.Priority.default)
  (sync : Bool := false) :
  BaseIO (Task (Except ε β))

EIO specialization of BaseIO.mapTasks.

def

IO.mapTasks.{u_1} {α : Type u_1} {β : Type}
  (f : List α → IO β) (tasks : List (Task α))
  (prio : Task.Priority :=
    Task.Priority.default)
  (sync : Bool := false) :
  BaseIO (Task (Except IO.Error β))

IO specialization of EIO.mapTasks.

opaque

BaseIO.bindTask.{u_1} {α : Type u_1} {β : Type}
  (t : Task α) (f : α → BaseIO (Task β))
  (prio : Task.Priority :=
    Task.Priority.default)
  (sync : Bool := false) : BaseIO (Task β)

See BaseIO.asTask.

def

EIO.bindTask.{u_1} {α : Type u_1} {ε β : Type}
  (t : Task α)
  (f : α → EIO ε (Task (Except ε β)))
  (prio : Task.Priority :=
    Task.Priority.default)
  (sync : Bool := false) :
  BaseIO (Task (Except ε β))

EIO specialization of BaseIO.bindTask.

def

IO.bindTask.{u_1} {α : Type u_1} {β : Type}
  (t : Task α)
  (f : α → IO (Task (Except IO.Error β)))
  (prio : Task.Priority :=
    Task.Priority.default)
  (sync : Bool := false) :
  BaseIO (Task (Except IO.Error β))

IO specialization of EIO.bindTask.

opaque

BaseIO.asTask {α : Type} (act : BaseIO α)
  (prio : Task.Priority :=
    Task.Priority.default) :
  BaseIO (Task α)

Run act in a separate Task. This is similar to Haskell's unsafeInterleaveIO, except that the Task is started eagerly as usual. Thus pure accesses to the Task do not influence the impure act computation. Unlike with pure tasks created by Task.spawn, tasks created by this function will be run even if the last reference to the task is dropped. The act should manually check for cancellation via IO.checkCanceled if it wants to react to that.

def

EIO.asTask {ε α : Type} (act : EIO ε α)
  (prio : Task.Priority :=
    Task.Priority.default) :
  BaseIO (Task (Except ε α))

EIO specialization of BaseIO.asTask.

def

IO.asTask {α : Type} (act : IO α)
  (prio : Task.Priority :=
    Task.Priority.default) :
  BaseIO (Task (Except IO.Error α))

IO specialization of EIO.asTask.

opaque

IO.cancel.{u_1} {α : Type u_1}
    : Task α → BaseIO Unit

Request cooperative cancellation of the task. The task must explicitly call IO.checkCanceled to react to the cancellation.

opaque

IO.getTaskState.{u_1} {α : Type u_1}
    : Task α → BaseIO IO.TaskState

Returns current state of the Task in the Lean runtime's task manager.

opaque

IO.checkCanceled : BaseIO Bool

Check if the task's cancellation flag has been set by calling IO.cancel or dropping the last reference to the task.

def

IO.hasFinished.{u_1} {α : Type u_1}
    (task : Task α) : BaseIO Bool

Check if the task has finished execution, at which point calling Task.get will return immediately.

8.10. Tasks and Threads

Constructor

Fields