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

[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

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.

[Kha]

Redirecting stdout in a robust manner is not feasible, we've tried. We can have the watchdog look out for response lines that are not valid JSON, assume that streams were crossed, write out the line as an actual diagnostic, and restart the file worker.

[Kha]

This is the likely source of the hang: https://github.com/leanprover/lean4/blob/9686910c72aaf1d39d28792265950b8f9f44880e/src/Lean/Server/Watchdog.lean#L212-L215 The watchdog thinks the file worker is crashing and wants to reap it, but the worker doesn't know that anything went wrong.

[Vtec234]

Yeah, you really shouldn't be writing to the system stdout stream. Lean stdio is redirected and should hopefullly just show up as a diagnostic, but we assume that system stdout is only used for LSP messages. I guess we could create a new pipe and use that, but even then if we cannot catch stdout, it will behave imprecisely (will not show up at the right place as a diagnostic).

[tydeu]

@Vtec234 I think creating a new pipe would be a great idea! Then normal stdout output could just appear in the console (i.e., the VS Code 'Output' panel) like stderr messages do.