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} {α : Type u} (get : α) : Task α

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.

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.

Task.Priority : Type

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

Task.Priority.default : Task.Priority

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

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.

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.

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.

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

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

EIO specialization of BaseIO.asTask.

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

IO specialization of EIO.asTask.

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.

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

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

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.

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.