Server crashes on `extern`

Stream: lean4

[Mac]

Piggy backing off my last question, I am trying to run some external definitions at interpretation time. I have made a plugin with said definitions and I can successfully run a file that uses them at interpretation time if I run it directly with the lean binary. However, the file breaks when run with the server. For example:

@[extern "foo"] constant foo : IO PUnit
#eval foo -- works as expected when run with normal `lean`, causes server to crash

I have verified that the plugin is being loaded (i.e., passing an invalid path causes a server error, but the plugin I give it is accepted without complaint). I suspect this may be related to the fact that such external #evals crash the server when missing (instead of printing an error that the external is missing like normal lean does). That is, I think the evaluation of external (non-builtin) symbols is broken (in the server) regardless of whether or not the symbol is properly provided.

[Mac]

@Sebastian Ullrich is this something work reporting as an issue?

[Sebastian Ullrich]

When you say "to the server", that's probably only to the watchdog and not to the file worker, right?

[Sebastian Ullrich]

And surely there's some stderr output?

[Mac]

@Sebastian Ullrich

For the first question, yes, but my understanding of the watchdog code is that it forwards its plugin arguments to worker when it starts it (at least that is my understand of these two lines in lean.cpp and Watchdog.lean.)

For the second question, no, I don't get any error messages regardless of the existence of the plugin --- the server just hangs and crashes. This is what makes me suspect a bug at work. As running with program with lean directly work s (and reports an error if the symbol is missing). Also providing an invalid plugin to server does cause it to report an error so I know I am not just missing messages from the server.

[Sebastian Ullrich]

Ah, that does sound like a bug

[Mac]

I submitted an issue to the GitHub (#639). However, after some more testing, I discovered I had provided that wrong plugin file (and thus the symbol was still missing). Providing the proper plugin works. The fact that it hangs with no error when the symbol is missing, though, still seems like a bug worth fixing at some point (hence why I did not close the issue).

[Mac]

I believe I discovered the source of the hang (which is a potentially larger bug) and submitted it to GitHub as #640.

[Sebastian Ullrich]

image.png
This might be a Windows-specific issue (I don't think it's non-Nix specific)

[Mac]

@Sebastian Ullrich what are you running there?

[Mac]

Oh! So you are saying the server outputted that (which it never does on my machine)? Ah, then yes it may have something to do with how file handles work on Windows.

[Sebastian Ullrich]

Might simply be that the standard unhandled exception handler uses stdout under MinGW, which would be weird, but we should definitely catch that exception ourselves anyway.

[Mac]

@Sebastian Ullrich It ialmost definitely because it uses stdout -- that is core of the issue I just submitted #640 -- "Writing to C/C++ standard output causes the server file worker to hang" (on Windows, since that is what I am using XD).

[Sebastian Ullrich]

I'm just surprised that it doesn't pop up a dialog box or something instead

[Mac]

I think the problem is that the stream is locked by something (I imagine the Lean Infoview?) and that is what is causing writing to it to hang (as the file worker is waiting on what it wrote to be read).

[Mac]

@Sebastian Ullrich, for that matter how should write to the infoview from C++ code? I would imagine it involves writing to the handle for the stdout IO stream. However, that handle is a FILE* and most C++ libraries (like LLVM) don't support writing to FILE* outputs, because that is not a C++ concept. So I don't know how to figure out what is the real Lean standard output stream to write to in C++.

[Sebastian Ullrich]

I'm not sure what you mean by writing to the info view, its contents are hard-coded until we have widgets. The worker and watchdog communicate via the LSP over regular stdin & stdout, there are no other streams involved.

[Sebastian Ullrich]

Which is the whole reason why it's a bad idea to write non-LSP to stdout in the server process

[Mac]

Ah, what I mean is that #eval IO.println "hello" writes a message that appears in the infoview. How do I, if possible, perform a similar write from C/C++ code?

[Mac]

I initially assumed that jus was a product of writing to stdout that the server worker caught.

[Sebastian Ullrich]

Oh, you mean in a diagnostic. You'd need to return a string to Lean and print it there.

[Mac]

Huh? That's really how? I would think that #eval IO.println "hello" would have to be writing to some stream as that is what the code for IO.println does.

[Sebastian Ullrich]

https://github.com/leanprover/lean4/blob/9686910c72aaf1d39d28792265950b8f9f44880e/src/Init/System/IO.lean#L149-L151

[Mac]

Ah, so instead of the normal primitive stream, in the server, stdout is a fabricated pure stream the produces diagnostics?

[Mac]

Is that what you are saying?

[Sebastian Ullrich]

Essentially, but it's a bit more localized than that. The stream doesn't know anything about diagnostics. https://github.com/leanprover/lean4/blob/9686910c72aaf1d39d28792265950b8f9f44880e/src/Init/System/IO.lean#L541-L542

[Mac]

Ah, is there than a more effective way of printing things in commands? That is, the current chain would be C++ print -> String -> #eval IO.print -> String -> Diagnostic -- is there a way to remove the middle IO link?

[Sebastian Ullrich]

Does it matter? In any case, take a look at how #eval does it: https://github.com/leanprover/lean4/blob/9686910c72aaf1d39d28792265950b8f9f44880e/src/Lean/Elab/BuiltinCommand.lean#L289

[Mac]

Well I am printing entire LLVM IR modules, so outputting a large file multiple times seems rather inefficient. :laughing:

[Mac]

Thanks for the help!

[Sebastian Ullrich]

I wanted to say that outputting into the IO.Buffer should be O(1) if it's the only output, but that's not true even after https://github.com/leanprover/lean4/pull/642 because we convert between String and ByteArray