IO.waitAny but no IO.waitAll ?

Stream: lean4

[Chris Lovett]

Why is there an IO.waitAny that waits for first task in a List of tasks to complete, but no corresponding IO.waitAll that returns the combined results as List α ?

[Chris Lovett]

I can do this, but why should I have to do that?

def processTasks (args: List String) : List String :=
  let tasks := args.map (λ s => Task.spawn fun _ => dbgSleep 1000 fun _ => s)
  let result := tasks.foldl (λ r s =>
    let x := Task.get s
    x :: r) ([]: List String)
  result

#eval processTasks ["apple", "banana", "orange"]

[Mario Carneiro]

I don't see the problem with that. You can write it more succinctly as:

def processTasks (args: List Nat) : List Nat :=
  (args.map fun s => Task.spawn fun _ => dbgSleep 1000 fun _ => s).map Task.get

#eval processTasks (List.range 7)

[Mario Carneiro]

by playing with the number it is amusing to see that the task manager will schedule up to 7 tasks in parallel on my machine (presumably one less than the number of cores on the machine with one being the main thread / scheduler)

[Mario Carneiro]

I find the current interface more flexible in allowing you to stuff the results in your own data structure instead of pulling it out of a list

[Chris Lovett]

I find the current interface more flexible in allowing you to stuff the results in your own data structure instead of pulling it out of a list

Yeah, I can see that now. I guess part of the problem is I'm still hopeless at writing good Lean code, not sure what I was thinking with that foldl call :-) I have 24 cores and I can definitely see the batching take place in this test:

#eval timeit "running " (processTasks (List.range 20)) -- running  1.02s
#eval timeit "running " (processTasks (List.range 40)) -- running  2.03s
#eval timeit "running " (processTasks (List.range 60)) -- running  3.03s
#eval timeit "running " (processTasks (List.range 80)) -- running  4.03s