Zulip Chat Archive

Stream: lean4 dev

Topic: Top-level task


James Gallicchio (Nov 29 2022 at 18:25):

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 (Nov 29 2022 at 18:27):

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

Gabriel Ebner (Nov 29 2022 at 18:29):

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

James Gallicchio (Nov 29 2022 at 18:49):

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 (Nov 29 2022 at 19:28):

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


Last updated: Dec 20 2023 at 11:08 UTC