search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.04k stars 348 forks source link

bug: server/vscode-lean4 not responding for certain files #1642

Open EdAyers opened 1 year ago

EdAyers commented 1 year ago

I haven't quite figured out the MWE yet. Possibly a vscode-lean4 bug.

There seem to be certain files for me where vscode and Lean will stop talking to each other. I have observed this a few times but today I found an example on the main branch of mathlib.

Please let me know, firstly, whether you can reproduce this because I am not sure whether my setup has entered a bad state.

Reproduction

The one that doesn't work for me is the file showTerm.lean from leanprover-community/mathlib4 (commit 492d30e023d3275404876f2c2ac8b68744a98b1f) with vscode extension version v0.0.95. Lean version is Lean (version 4.0.0-nightly-2022-09-22, commit 708a777d7472, Release). I double checked that vscode was using the right lean version.

Opening this file will cause the server to not respond. image

If instead I switch to this page from a file that is working normally I get an error in the infoview

image

I tracked down this error being due to the rpc call 'Lean.Widget.getInteractiveDiagnostics' resolving to undefined, however this line assumes that it is an array, causing the error.

However I can't determine why the connection is entering a weird state for this file, no other server calls are functioning at all. If I open the file with "lean4.trace.server": "verbose",, there is no traffic to or from the server other than keepAlives.

lovettchris commented 1 year ago

Thanks for the bug report, that file with that commit seems to work fine for me, do you see anything in the "Lean: Editor" Output page?

image

If you turn on the Lean Server logging via this setting you could attach the wdIn.txt, wdOut.txt and fwIn.txt and fwOut.txt log files. I like to also put these logs in a separate "log" folder using the second setting here:

image

EdAyers commented 1 year ago

I tried to reproduce again on this file and I can't, it all seems to be working now. I'll keep developing and see if I can catch it failing again.

At the time, Lean Editor: Output was only emitting keepAlive messages. I think the server was dead or in a weird state.