Writing to C/C++ standard output causes the server file worker to hang

Prerequisites

• 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

Lean server file workers hang eternally when code writes to the C/C++ standard output (i.e., not to the Lean standard output via IO methods). Restarting them in VS Code requires reloading the window (restarting the server does not restart the work).

Steps to Reproduce

1. Pack the following C++ code:

extern.cpp:

#include <stdio.h>
#include <lean/io.h>

extern "C" uint32_t my_add(uint32_t a, uint32_t b) {
    return a + b;
}

extern "C" lean_obj_res my_hello(lean_obj_arg /* w */) {
  puts("Hello World");
  return lean_io_result_mk_ok(lean_box(0));
}

And the following Lean code:

Extern.lean:

@[extern "my_hello"] constant myHello : IO PUnit
@[extern "my_add"] constant myAdd : UInt32 → UInt32 → UInt32

into a plugin.

2. Run the following code with said plugin passed to the server:

Bug.lean:

import Extern
#eval myAdd 1 2 -- evaluates to 3, as expected
#eval myHello -- hangs eternally

3. Observe the bug. Note that running this file with Lean directly produces the following output:

Hello World
3

Expected behavior:

Ideally, the message would appear in the Infoview. Alternatively, the output could be printed to the 'Output' tab of VS Code (like messages written to standard error) if the former is not possible.

Actual behavior:

The file worker hangs eternally.

Reproduces how often:

Always.

Versions

OS: Windows 20H2
Lean (version 4.0.0-nightly-2021-08-20, commit 1624e42a5d6d, Release)

Additional Information

This is follow-up of #639. I did some more testing and discovered this bug, which explains that issue. Since the error message for missing external symbols is written directly to the C/C++ standard output (see this line), it hangs.

Reproduce the hang with extern.cpp, Extern.lean, and Bug.lean, then inspect src/library/compiler/ir_interpreter.cpp around the linked line 837 where missing external-symbol errors are written to C/C++ standard output. Compare server file-worker behavior with direct Lean execution; done means the worker no longer hangs and the output is handled through the expected Infoview or VS Code output path.