vscode-lean4 Doesn't Work When I Switch Files

Stream: lean4

[Arjun Viswanathan]

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.

[Chris B]

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)

[Chris B]

@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.

[Gabriel Ebner]

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