Zulip Chat Archive

Stream: lean4

Topic: vscode-lean4 Doesn't Work When I Switch Files


view this post on Zulip Arjun Viswanathan (Mar 26 2021 at 18:37):

The VSCode extension for Lean4 works properly on my project when I open it as long as I stay within the file that I opened to. When I switch tabs to a different Lean file, I immediately get this output:

Watchdog error: Got unknown document URI (file:///filename)
[Info  - 1:28:01 PM] Connection to server got closed. Server will restart.
[Error - 1:28:01 PM] Request textDocument/documentSymbol failed.
Error: Connection got disposed.
    at Object.dispose (/home/arjun/.vscode/extensions/leanprover.lean4-0.0.20/out/extension.js:2:145468)

and then the extension doesn't work anymore until I restart VSCode.

Has anybody else had this experience? Any help will be appreciated.

view this post on Zulip Chris B (Mar 26 2021 at 19:27):

I'm getting this inconsistently on 4.0.0-m2 with 0.0.2 for the extension. Mine is slightly more verbose:

Watchdog error: Got unknown document URI (file:///Users/zzz/test_dir/testfile2.lean)
[Info  - 2:19:18 PM] Connection to server got closed. Server will restart.
[Error - 2:19:18 PM] Request textDocument/documentSymbol failed.
Error: Connection got disposed.
    at Object.dispose (/Users/zzz/.vscode/extensions/leanprover.lean4-0.0.20/out/extension.js:2:145468)
    at Object.dispose (/Users/zzz/.vscode/extensions/leanprover.lean4-0.0.20/out/extension.js:2:225640)
    at C.handleConnectionClosed (/Users/zzz/.vscode/extensions/leanprover.lean4-0.0.20/out/extension.js:2:225853)
    at C.handleConnectionClosed (/Users/zzz/.vscode/extensions/leanprover.lean4-0.0.20/out/extension.js:2:286241)
    at t (/Users/zzz/.vscode/extensions/leanprover.lean4-0.0.20/out/extension.js:2:223942)
    at invoke (/Users/zzz/.vscode/extensions/leanprover.lean4-0.0.20/out/extension.js:2:147081)
    at o.fire (/Users/zzz/.vscode/extensions/leanprover.lean4-0.0.20/out/extension.js:2:147842)
    at Y (/Users/zzz/.vscode/extensions/leanprover.lean4-0.0.20/out/extension.js:2:134726)
    at invoke (/Users/zzz/.vscode/extensions/leanprover.lean4-0.0.20/out/extension.js:2:147081)
    at o.fire (/Users/zzz/.vscode/extensions/leanprover.lean4-0.0.20/out/extension.js:2:147842)
    at m.fireClose (/Users/zzz/.vscode/extensions/leanprover.lean4-0.0.20/out/extension.js:2:159295)
    at Socket.<anonymous> (/Users/zzz/.vscode/extensions/leanprover.lean4-0.0.20/out/extension.js:2:160080)
    at Socket.emit (events.js:315:20)
    at Pipe.<anonymous> (net.js:674:12)

view this post on Zulip Chris B (Mar 26 2021 at 19:33):

@Arjun Viswanathan This might just be an issue with stable. The instructions for the vscode extension say to use the nightly build of lean4, and that does seem to prevent this.

view this post on Zulip Gabriel Ebner (Mar 26 2021 at 20:07):

Yup, this has been fixed a few days ago: https://github.com/leanprover/lean4/pull/344/commits/a266f584d551185703d44e2d3142eeb5c026ce82


Last updated: May 07 2021 at 11:09 UTC