96f9ee2a41
This PR ensures info tree users such as linters and request handlers have access to info subtrees created by async elab task by introducing API to leave holes filled by such tasks. **Breaking change**: other metaprogramming users of `Command.State.infoState` may need to call `InfoState.substituteLazy` on it manually to fill all holes.
29 lines
773 B
Text
29 lines
773 B
Text
/-
|
||
Copyright (c) 2025 Lean FRO. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Sebastian Ullrich
|
||
|
||
Additional `Task` definitions.
|
||
-/
|
||
prelude
|
||
import Init.Core
|
||
import Init.Data.List.Basic
|
||
|
||
namespace Task
|
||
|
||
/--
|
||
Creates a task that, when all `tasks` have finished, computes the result of `f` applied to their
|
||
results.
|
||
-/
|
||
def mapList (f : List α → β) (tasks : List (Task α)) (prio := Task.Priority.default)
|
||
(sync := false) : Task β :=
|
||
go tasks []
|
||
where
|
||
go
|
||
| [], as =>
|
||
if sync then
|
||
.pure <| f as.reverse
|
||
else
|
||
Task.spawn (prio := prio) fun _ => f as.reverse
|
||
| [t], as => t.map (fun a => f (a :: as).reverse) prio sync
|
||
| t::ts, as => t.bind (fun a => go ts (a :: as)) prio sync
|