waiting on a List of Tasks

Stream: lean4

[Scott Morrison]

Given a List (Task α), is there any way to find if one is ready?

[Eric Wieser]

On a similar note, do we have a way to go from List (Task X) to Task (List X)?

[Scott Morrison]

Isn't that just

example (L : List (Task X)) : Task (List X) :=
  Task.spawn fun _ => L.map Task.get

[Eric Wieser]

Doesn't that run them sequentially rather than in parallel?

[Alex Keizer]

I think tasks run in the background as soon as they're created. Task.get is not driving the task, it's just checking whether the background computation has finished. At least, that is my interpretation of the following doc:

/--
`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.
-/
@[noinline, extern "lean_task_spawn"]
protected def spawn {α : Type u} (fn : Unit → α) (prio := Priority.default) : Task α :=
  ⟨fn ()⟩

[Eric Wieser]

Ah, sorry for the noise then

[Mac Malone]

Scott Morrison said:

Isn't that just

example (L : List (Task X)) : Task (List X) :=
  Task.spawn fun _ => L.map Task.get

While simple, this is inefficient. It spawns a thread solely to wait on others, which is a waste of resources. Ideally, you would use a bind to merge the tasks into one.

[Wojciech Nawrocki]

Task.spawn with default priority won't spawn a dedicated thread iirc, so that's not so much of an issue. The real problem is that calling Task.get from within another task does not register a dependency with the task manager, so this code can deadlock

[Wojciech Nawrocki]

Unfortunately as far as waiting on a list of Tasks goes, you may have to write the code yourself using docs4#Task.bind or docs4#IO.bindTask . At one point I wrote docs4#IO.AsyncList which can do this for you in cases where your computation is producing a list of tasks, kind of like a coinductive stream. However not all computations can be sensibly phrased this way.

[Wojciech Nawrocki]

Oh, if you just want to find if one is ready, there is docs4#IO.waitAny. The method that's missing would be IO.waitAll.

[Wojciech Nawrocki]

@Scott Morrison ^

[Eric Wieser]

It looks like the API of waitAny is rather lacking; I'd expect it to either return a list of the non-resolved tasks, or the index of the one that was resolved

[Wojciech Nawrocki]

Yeah, it's very low-level. You can easily create the index yourself, though, by returning it from the task.

[Eric Wieser]

Well, the low-level API in C already has the index available as it holds a reference to the task object rather than just its result

[Eric Wieser]

But I see your point

[Sebastian Ullrich]

Wojciech Nawrocki said:

Oh, if you just want to find if one is ready, there is docs4#IO.waitAny. The method that's missing would be IO.waitAll.

In contrast to waitAny, you can build a reasonably efficient version of waitAll using bindTask

[Adam Topaz]

Mac said:

Scott Morrison said:

Isn't that just

example (L : List (Task X)) : Task (List X) :=
  Task.spawn fun _ => L.map Task.get

While simple, this is inefficient. It spawns a thread solely to wait on others, which is a waste of resources. Ideally, you would use a bind to merge the tasks into one.

Would using docs4#List.mapA be the right approach?

[Eric Wieser]

Is that different to docs4#List.traverse ?

[Adam Topaz]

For some reason the docs webpage isn’t letting me look at the source of that function.

[Eric Wieser]

I think source links are broken for all of mathlib

[Eric Wieser]

These lines are failing, cc @Henrik Böving

[Henrik Böving]

Ah, doc-gen is not capable of understanding that a dependnecy that is given as a directory instead of a git thing in lake is an issue, that's annoying, I'll try to fix the action

[Henrik Böving]

Okay I pushed a fix to doc-gen and tested it locally, the source links should work again with the next build so in at max 9 hours

[Henrik Böving]

Ah no! the mathlib4 dooc-gen4 build is failing due to some other weird reason that I dont have influence on from the doc-gen4 repo so you might have to wait a little longer until that is fixed as well.

[Scott Morrison]

Ah, waitAll is essentially already there as BaseIO.mapTasks pure : List (Task α) → BaseIO (Task (List α)).

[Scott Morrison]

!4#3620 has waitAny', which also returns the remaining tasks, and sequenceTasks := BaseIO.mapTasks pure.

[Eric Wieser]

Is "traverse" a better word than "sequence"? nevermind