Top-level task

Stream: lean4 dev

[James Gallicchio]

Hey, we were talking about this a bit in the Std meeting -- is it possible to have the top-level main thread block on a task non-busily?

It seems like IO.wait is a busy loop, which is not ideal. Would it be possible for a main function to be allowed to be IO (Task Unit) instead of IO Unit so that it can asynchronously wait for other tasks?

[Gabriel Ebner]

Why do you think IO.wait is a busy loop?

[Gabriel Ebner]

It's certainly not ideal; it will wake up every time a task finishes. But it's not a busy loop.

[James Gallicchio]

Ohhhh, that is not what I thought, very cool. I'm not sure where I got the idea that it blocks. Maybe we should include that in the docstring for IO.wait.

It still might be nice to allow Task toplevel -- from what we talked about it seems IO.wait is not deadlock-safe in general, whereas task binds are since the task manager tracks those dependencies. So a top-level task makes it the compiler's job to call the IO.wait and I can have it not appear as the last line of my main functions :)

[Sebastian Ullrich]

It blocks, but it doesn't busy loop. Those are separate things.