Iterator-based parallelization for Lean's tactic monads.

This file provides utilities for running computations in parallel using Lean's task system, with support for collecting results in different ways.

Main functions

For each monad (IO, CoreM, MetaM, TermElabM, TacticM), the following functions are provided:

• par / par'

  • Run jobs in parallel, collect results in original order
  • Takes List (MonadM α), returns MonadM (List (Except Error (α × State))) / MonadM (List (Except Error α))
  • All tasks run in parallel, results returned in input order
  • par returns state information, par' discards state
  • Final state is restored to initial state (before tasks ran)
  • Errors wrapped in Except so all results are collected

• parIter / parIterWithCancel

  • Run jobs in parallel, iterate over results in original order
  • Takes List (MonadM α), returns iterator
  • parIterWithCancel also returns cancellation hook

• parIterGreedy / parIterGreedyWithCancel

  • Run jobs in parallel, iterate over results in completion order (greedily)
  • Takes List (MonadM α), returns iterator
  • parIterGreedyWithCancel also returns cancellation hook

• parFirst

  • Run jobs in parallel, return first successful result (by completion order)
  • Cancels remaining tasks after first success (by default)
  • Throws error if all tasks fail

Implementation notes

The greedy iterator-based functions use IO.waitAny' internally to wait for task completion in any order. The ordered iterator-based functions process tasks sequentially in the original order.

State threading in iterators: The iterators (parIter, parIterGreedy, and their WithCancel variants) preserve state from each completed task. When you map over an iterator with a monadic function, the monad state will be that at the conclusion of the monadic action that produced each value. This means:

• For parIter: State is threaded sequentially in the original task order
• For parIterGreedy: State is threaded in task completion order

This allows you to observe state changes (like logged messages, modified metavariable contexts, etc.) as tasks complete, unlike par/par' which restore the initial state after collecting all results.

Iterators do not have Finite instances, as we cannot prove termination from the available information. For consumers that require Finite (like .toList), use .allowNontermination.toList.

structure Std.Iterators.TaskIterator (α : Type w) : Type w

Internal state for an iterator over tasks. Maintains the list of tasks that haven't completed yet.

• tasks : List (Task α)

def Lean.Core.CoreM.parIterWithCancel {α : Type} (jobs : List (CoreM α)) : CoreM (BaseIO PUnit × Std.IterM CoreM (Except Exception α))

Runs a list of CoreM computations in parallel and returns:

• a combined cancellation hook for all tasks, and
• an iterator that yields results in original order.

The iterator runs in CoreM, and as it yields each result, it updates the CoreM state to reflect the state when that particular task completed. This means the state is threaded through the iteration in the order of the original list.

Results are wrapped in Except Exception α so that errors in individual tasks don't stop the iteration - you can observe all results including which tasks failed.

The iterator will terminate after all jobs complete (assuming they all do complete).

Equations

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

def Lean.Core.CoreM.parIter {α : Type} (jobs : List (CoreM α)) : CoreM (Std.IterM CoreM (Except Exception α))

Runs a list of CoreM computations in parallel (without cancellation hook).

Returns an iterator that yields results in original order, wrapped in Except Exception α.

Equations

• Lean.Core.CoreM.parIter jobs = (fun (x : BaseIO PUnit × Std.IterM Lean.CoreM (Except Lean.Exception α)) => x.snd) <$> Lean.Core.CoreM.parIterWithCancel jobs

def Lean.Core.CoreM.parIterGreedyWithCancel {α : Type} (jobs : List (CoreM α)) : CoreM (BaseIO PUnit × Std.IterM CoreM (Except Exception α))

Runs a list of CoreM computations in parallel and returns:

• a combined cancellation hook for all tasks, and
• an iterator that yields results in completion order (greedily).

The iterator runs in CoreM, and as it yields each result, it updates the CoreM state to reflect the state when that particular task completed. This means the state is threaded through the iteration in task completion order.

Results are wrapped in Except Exception α so that errors in individual tasks don't stop the iteration - you can observe all results including which tasks failed.

The iterator will terminate after all jobs complete (assuming they all do complete).

Equations

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

def Lean.Core.CoreM.parIterGreedy {α : Type} (jobs : List (CoreM α)) : CoreM (Std.IterM CoreM (Except Exception α))

Runs a list of CoreM computations in parallel (without cancellation hook).

Returns an iterator that yields results in completion order, wrapped in Except Exception α.

Equations

• Lean.Core.CoreM.parIterGreedy jobs = (fun (x : BaseIO PUnit × Std.IterM Lean.CoreM (Except Lean.Exception α)) => x.snd) <$> Lean.Core.CoreM.parIterGreedyWithCancel jobs

def Lean.Core.CoreM.par {α : Type} (jobs : List (CoreM α)) : CoreM (List (Except Exception (α × SavedState)))

Runs a list of CoreM computations in parallel and collects results in the original order, including the saved state after each task completes.

Unlike parIter, this waits for all tasks to complete and returns results in the same order as the input list, not in completion order.

Results are wrapped in Except Exception (α × Core.SavedState) so that errors in individual tasks don't stop the collection - you can observe all results including which tasks failed.

The final CoreM state is restored to the initial state (before tasks ran).

Equations

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

def Lean.Core.CoreM.par' {α : Type} (jobs : List (CoreM α)) : CoreM (List (Except Exception α))

Runs a list of CoreM computations in parallel and collects results in the original order, discarding state information.

Unlike par, this doesn't return state information from tasks.

The final CoreM state is restored to the initial state (before tasks ran).

Equations

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

def Lean.Core.CoreM.parFirst {α : Type} (jobs : List (CoreM α)) (cancel : Bool := true) : CoreM α

Runs a list of CoreM computations in parallel and returns the first successful result (by completion order, not list order).

If cancel := true (the default), cancels all remaining tasks after the first success.

Equations

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

def Lean.Meta.MetaM.par {α : Type} (jobs : List (MetaM α)) : MetaM (List (Except Exception (α × SavedState)))

Runs a list of MetaM computations in parallel and collects results in the original order, including the saved state after each task completes.

Unlike parIter, this waits for all tasks to complete and returns results in the same order as the input list, not in completion order.

Results are wrapped in Except Exception (α × Meta.SavedState) so that errors in individual tasks don't stop the collection - you can observe all results including which tasks failed.

The final MetaM state is restored to the initial state (before tasks ran).

Equations

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

def Lean.Meta.MetaM.par' {α : Type} (jobs : List (MetaM α)) : MetaM (List (Except Exception α))

Runs a list of MetaM computations in parallel and collects results in the original order, discarding state information.

Unlike par, this doesn't return state information from tasks.

The final MetaM state is restored to the initial state (before tasks ran).

Equations

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

def Lean.Meta.MetaM.parIterWithCancel {α : Type} (jobs : List (MetaM α)) : MetaM (BaseIO PUnit × Std.IterM MetaM (Except Exception α))

Runs a list of MetaM computations in parallel and returns:

• a combined cancellation hook for all tasks, and
• an iterator that yields results in original order.

The iterator runs in MetaM, and as it yields each result, it updates the MetaM state to reflect the state when that particular task completed. This means the state is threaded through the iteration in the order of the original list.

Results are wrapped in Except Exception α so that errors in individual tasks don't stop the iteration - you can observe all results including which tasks failed.

The iterator will terminate after all jobs complete (assuming they all do complete).

Equations

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

def Lean.Meta.MetaM.parIter {α : Type} (jobs : List (MetaM α)) : MetaM (Std.IterM MetaM (Except Exception α))

Runs a list of MetaM computations in parallel (without cancellation hook).

Returns an iterator that yields results in original order, wrapped in Except Exception α.

Equations

• Lean.Meta.MetaM.parIter jobs = (fun (x : BaseIO PUnit × Std.IterM Lean.MetaM (Except Lean.Exception α)) => x.snd) <$> Lean.Meta.MetaM.parIterWithCancel jobs

def Lean.Meta.MetaM.parIterGreedyWithCancel {α : Type} (jobs : List (MetaM α)) : MetaM (BaseIO PUnit × Std.IterM MetaM (Except Exception α))

Runs a list of MetaM computations in parallel and returns:

• a combined cancellation hook for all tasks, and
• an iterator that yields results in completion order (greedily).

The iterator runs in MetaM, and as it yields each result, it updates the MetaM state to reflect the state when that particular task completed. This means the state is threaded through the iteration in task completion order.

Results are wrapped in Except Exception α so that errors in individual tasks don't stop the iteration - you can observe all results including which tasks failed.

The iterator will terminate after all jobs complete (assuming they all do complete).

Equations

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

def Lean.Meta.MetaM.parIterGreedy {α : Type} (jobs : List (MetaM α)) : MetaM (Std.IterM MetaM (Except Exception α))

Runs a list of MetaM computations in parallel (without cancellation hook).

Returns an iterator that yields results in completion order, wrapped in Except Exception α.

Equations

• Lean.Meta.MetaM.parIterGreedy jobs = (fun (x : BaseIO PUnit × Std.IterM Lean.MetaM (Except Lean.Exception α)) => x.snd) <$> Lean.Meta.MetaM.parIterGreedyWithCancel jobs

def Lean.Meta.MetaM.parFirst {α : Type} (jobs : List (MetaM α)) (cancel : Bool := true) : MetaM α

Runs a list of MetaM computations in parallel and returns the first successful result (by completion order, not list order).

If cancel := true (the default), cancels all remaining tasks after the first success.

Equations

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

def Lean.Elab.Term.TermElabM.parIterWithCancel {α : Type} (jobs : List (TermElabM α)) : TermElabM (BaseIO PUnit × Std.IterM TermElabM (Except Exception α))

Runs a list of TermElabM computations in parallel and returns:

• a combined cancellation hook for all tasks, and
• an iterator that yields results in original order.

The iterator runs in TermElabM, and as it yields each result, it updates the TermElabM state to reflect the state when that particular task completed. This means the state is threaded through the iteration in the order of the original list.

Results are wrapped in Except Exception α so that errors in individual tasks don't stop the iteration - you can observe all results including which tasks failed.

The iterator will terminate after all jobs complete (assuming they all do complete).

Equations

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

def Lean.Elab.Term.TermElabM.parIter {α : Type} (jobs : List (TermElabM α)) : TermElabM (Std.IterM TermElabM (Except Exception α))

Runs a list of TermElabM computations in parallel (without cancellation hook).

Returns an iterator that yields results in original order, wrapped in Except Exception α.

Equations

• Lean.Elab.Term.TermElabM.parIter jobs = (fun (x : BaseIO PUnit × Std.IterM Lean.Elab.TermElabM (Except Lean.Exception α)) => x.snd) <$> Lean.Elab.Term.TermElabM.parIterWithCancel jobs

def Lean.Elab.Term.TermElabM.parIterGreedyWithCancel {α : Type} (jobs : List (TermElabM α)) : TermElabM (BaseIO PUnit × Std.IterM TermElabM (Except Exception α))

Runs a list of TermElabM computations in parallel and returns:

• a combined cancellation hook for all tasks, and
• an iterator that yields results in completion order (greedily).

The iterator runs in TermElabM, and as it yields each result, it updates the TermElabM state to reflect the state when that particular task completed. This means the state is threaded through the iteration in task completion order.

Results are wrapped in Except Exception α so that errors in individual tasks don't stop the iteration - you can observe all results including which tasks failed.

The iterator will terminate after all jobs complete (assuming they all do complete).

Equations

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

def Lean.Elab.Term.TermElabM.parIterGreedy {α : Type} (jobs : List (TermElabM α)) : TermElabM (Std.IterM TermElabM (Except Exception α))

Runs a list of TermElabM computations in parallel (without cancellation hook).

Returns an iterator that yields results in completion order, wrapped in Except Exception α.

Equations

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

def Lean.Elab.Term.TermElabM.par {α : Type} (jobs : List (TermElabM α)) : TermElabM (List (Except Exception (α × SavedState)))

Runs a list of TermElabM computations in parallel and collects results in the original order, including the saved state after each task completes.

Unlike parIter, this waits for all tasks to complete and returns results in the same order as the input list, not in completion order.

Results are wrapped in Except Exception (α × Term.SavedState) so that errors in individual tasks don't stop the collection - you can observe all results including which tasks failed.

The final TermElabM state is restored to the initial state (before tasks ran).

Equations

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

def Lean.Elab.Term.TermElabM.par' {α : Type} (jobs : List (TermElabM α)) : TermElabM (List (Except Exception α))

Runs a list of TermElabM computations in parallel and collects results in the original order, discarding state information.

Unlike par, this doesn't return state information from tasks.

The final TermElabM state is restored to the initial state (before tasks ran).

Equations

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

def Lean.Elab.Term.TermElabM.parFirst {α : Type} (jobs : List (TermElabM α)) (cancel : Bool := true) : TermElabM α

Runs a list of TermElabM computations in parallel and returns the first successful result (by completion order, not list order).

If cancel := true (the default), cancels all remaining tasks after the first success.

Equations

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

def Lean.Elab.Tactic.TacticM.parIterWithCancel {α : Type} (jobs : List (TacticM α)) : TacticM (BaseIO PUnit × Std.IterM TacticM (Except Exception α))

Runs a list of TacticM computations in parallel and returns:

• a combined cancellation hook for all tasks, and
• an iterator that yields results in original order.

The iterator runs in TacticM, and as it yields each result, it updates the TacticM state to reflect the state when that particular task completed. This means the state is threaded through the iteration in the order of the original list.

Results are wrapped in Except Exception α so that errors in individual tasks don't stop the iteration - you can observe all results including which tasks failed.

The iterator will terminate after all jobs complete (assuming they all do complete).

Equations

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

def Lean.Elab.Tactic.TacticM.parIter {α : Type} (jobs : List (TacticM α)) : TacticM (Std.IterM TacticM (Except Exception α))

Runs a list of TacticM computations in parallel (without cancellation hook).

Returns an iterator that yields results in original order, wrapped in Except Exception α.

Equations

• Lean.Elab.Tactic.TacticM.parIter jobs = (fun (x : BaseIO PUnit × Std.IterM Lean.Elab.Tactic.TacticM (Except Lean.Exception α)) => x.snd) <$> Lean.Elab.Tactic.TacticM.parIterWithCancel jobs

def Lean.Elab.Tactic.TacticM.parIterGreedyWithCancel {α : Type} (jobs : List (TacticM α)) : TacticM (BaseIO PUnit × Std.IterM TacticM (Except Exception α))

Runs a list of TacticM computations in parallel and returns:

• a combined cancellation hook for all tasks, and
• an iterator that yields results in completion order (greedily).

The iterator runs in TacticM, and as it yields each result, it updates the TacticM state to reflect the state when that particular task completed. This means the state is threaded through the iteration in task completion order.

Results are wrapped in Except Exception α so that errors in individual tasks don't stop the iteration - you can observe all results including which tasks failed.

The iterator will terminate after all jobs complete (assuming they all do complete).

Equations

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

def Lean.Elab.Tactic.TacticM.parIterGreedy {α : Type} (jobs : List (TacticM α)) : TacticM (Std.IterM TacticM (Except Exception α))

Runs a list of TacticM computations in parallel (without cancellation hook).

Returns an iterator that yields results in completion order, wrapped in Except Exception α.

Equations

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

def Lean.Elab.Tactic.TacticM.par {α : Type} (jobs : List (TacticM α)) : TacticM (List (Except Exception (α × SavedState)))

Runs a list of TacticM computations in parallel and collects results in the original order, including the saved state after each task completes.

Unlike parIter, this waits for all tasks to complete and returns results in the same order as the input list, not in completion order.

Results are wrapped in Except Exception (α × Tactic.SavedState) so that errors in individual tasks don't stop the collection - you can observe all results including which tasks failed.

The final TacticM state is restored to the initial state (before tasks ran).

Equations

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

def Lean.Elab.Tactic.TacticM.par' {α : Type} (jobs : List (TacticM α)) : TacticM (List (Except Exception α))

Runs a list of TacticM computations in parallel and collects results in the original order, discarding state information.

Unlike par, this doesn't return state information from tasks.

The final TacticM state is restored to the initial state (before tasks ran).

Equations

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

def Lean.Elab.Tactic.TacticM.parFirst {α : Type} (jobs : List (TacticM α)) (cancel : Bool := true) : TacticM α

Runs a list of TacticM computations in parallel and returns the first successful result (by completion order, not list order).

If cancel := true (the default), cancels all remaining tasks after the first success.

Equations

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