Asynchronous printing hangs the server

[tydeu]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Printing text asynchronously (e.g., a IO.println run through IO.asTask) causes the Lean server to hang.

Steps to Reproduce

Run the following code via the Lean server (e.g., in VSCode) to observe the server hanging:

#eval show IO _ from do 
  IO.wait <| ← IO.asTask <| IO.println "test"

Expected behavior:

To print "test" either as a diagnostic or in the output panel.

Actual behavior:

The server hangs.

Reproduces how often:

Always.

Versions

Windows 10 20H2 Lean (version 4.0.0-nightly-2021-10-23, commit a741a3dfd422, Release)

Additional Information

I suspect this is actually due to the same problem as #640. That is, I suspect that the asynchronous print is not being properly redirected (due to being in a separate thread) and is thus printing to normal stdout,. This, as #640 shows, causes the server to hang.

[Kha]

Related to #426, in which case we would lose the output (so simply don't do that).

[Vtec234]

There's another issue. Elaboration is executed in asynchronous tasks, but here the elaborated code runs IO.wait which we know doesn't register a task-task dependency in the task manager, which can result in deadlock.

[tydeu]

@Vtec234 note that the bug still occurs without IO.wait. That is, this also hangs:

#eval show IO _ from do
  discard <| IO.asTask <| IO.println "test"

[Kha]

Oh, I didn't even see the wait. #426 would only lose the output in the latter case of course.