running lean repl commands with thread parralelism

Stream: general

[Frederick Pu]

I'm trying to parrallelize the lean repl using tasks

unsafe def batchVerifyParrallelNaive (initialCmdState : Command.State) (cmds : Array Command) (timeout : Option Nat) : IO (Array (CommandResponse ⊕ Error)) := do
  let commandRunner :=
    match timeout with
    | some t => fun cmd => runCommandGCAuxTimeout initialCmdState cmd t
    | none => runCommandGCAux initialCmdState
  let tasks : Array (Task (Except IO.Error (CommandResponse ⊕ Error))) ← (cmds.mapM <| fun cmd => IO.asTask (commandRunner cmd)
  )
  tasks.mapM fun task => do
    try
      match task.get with
      | .ok cmdres => return cmdres
      | .error e => return .inr ⟨e.toString⟩
    catch e =>
      return .inr ⟨e.toString⟩

Is task.get sufficient or do I need to also do task.wait to make sure that the thread fully closes?

[Sebastian Ullrich]

That should be sufficient