Order of running, Tasks in Main

Stream: lean4

[Siddhartha Gadgil]

I was trying to figure out tasks, but find myself with a more basic question about IO and main. I have the following program as Main.lean:

def main (args: List String) : IO Unit := do
    IO.println "Hello, world!"
    IO.println "Computing slow-minimum 2000"
    let res := slowMin 2000
    IO.println (res)
    return ()

With slowMin a silly function just designed to take time. When I compile and run, the program does not output anything before computing the result (takes about 30 seconds) and then outputs everything at once. When I had more code just after the "Hello World!" which had output, the result of slowMin was computed before anything else was run.

Is this expected behaviour? How do I avoid a computation late in a compiled program holding up earlier portions?

Thanks.

[Siddhartha Gadgil]

I was having similar difficulties with parallelization using tasks. In a variation of the above:

def main (args: List String) : IO Unit := do
    IO.println "Hello, world!"
    IO.println "Computing slow-minimum 2000"
    let t1 := Task.spawn <| fun _ => slowMin 2000
    let t2 := Task.spawn <| fun _ => slowMin 2100
    let t3 := Task.spawn <| fun _ => slowMin 2200
    IO.println (t1.get + t2.get + t3.get)
    return ()

I hoped that the tasks would start running as soon as they are spawned (like a Future in scala). However they did not do so, as I could see from both the time taken and using htop.

Can someone tell me what I misunderstand (and how to correct it)? Within IO am I supposed to do something else?