Anyone have notes/docs/comments about IO.Promise?

Stream: lean4

[nrs]

I'm trying to figure out how task delegation works in TermElabM, and am currently working on understanding how elabHeaders in src/Lean/Elab/MutualDef.lean works. (specifically, I need to understand how it consumes bodyPromises : Array (IO.Promise (Option BodyProcessedSnapshot)) and tacPromises : Array (IO.Promise Tactic.TacticParsedSnapshot).

Anyone got additional documentation or notes about how IO.Promise works? (or a high-level overview of Lean's task/threading/async model?)