VS Code 0.0.6x - Goofin'

Stream: lean4

[Arthur Paulino]

Seems like it was solved for me, thanks!

[Arthur Paulino]

Hm, now it's crashing a lot and the connection with the server is closing. I'll try to reproduce it consistently

[Arthur Paulino]

I'm not being able to make it crash again, but it's acting a bit weird when opening new files. It looks unresponsive for a few seconds and then starts loading up

[František Silváši]

I've edited the topic name :).

[Notification Bot]

František Silváši has marked this topic as unresolved.

[Gabriel Ebner]

0.0.63 is out. Can you check again please?

[Arthur Paulino]

Gabriel Ebner said:

0.0.63 is out. Can you check again please?

Looks smooth for now! Thanks again!
Will report back if I find anything strange

BTW: did you address anything that could be related to the escape hotkey reset? (I use ; instead of \)

[Gabriel Ebner]

BTW: did you address anything that could be related to the escape hotkey reset? (I use ; instead of \)

I don't think so. But I wouldn't know how that could happen in the first place.

If you tell me how to reproduce, I'll fix it.

[Arthur Paulino]

Yeah, I will need to tweak it some more before I can reproduce it consistently

[Gabriel Ebner]

That is, functions with many references perhaps?

In case anybody was wondering what actually happened:

When vscode opens a hover with a source code snippet, it opens the corresponding file as a text document. From the extension side this kind of document looks exactly like a file the user opened intentionally. But if we told the Lean server that a file was opened, it would start a Lean worker process for that file. It would start a Lean process every time you hover! Clearly this must be avoided.

So we've put in a hack that prevents the vscode LSP library from sending the didOpen notification. Instead, we subscribe to the onDidChangeVisibleTextEditors event and manually send didOpen notification only for these visible text editors.

There's a second complication: to support installing both the Lean 3 and Lean 4 extension at the same time, the Lean 4 extensions needs to change the language id of a file to lean4 after it's opened. This also used to be triggered by the visible editors event. (Changing the language id closes and reopens the text document. IIRC, the hover doesn't like that and opens the file again.)

The recent multi-root workspace PR https://github.com/leanprover/vscode-lean4/pull/104 inadvertently duplicated the setTextDocumentLanguage call and also triggered it when a document was opened. From what I can tell, changing the language id of the hovered file makes the hover open the file again, sending it into an endless loop. Setting the language id twice resulting in one of the calls failing, printing endless error messages on the console (thankfully, this made diagnosing the issue trivial).

cc @Chris Lovett

[František Silváši]

IOW 'just move on to Lean 4 already'! :stuck_out_tongue_closed_eyes:

[Kevin Buzzard]

Do you want to help porting the 700K lines of mathlib3? Once they're all done I'm moving immediately!

[Arthur Paulino]

Just found another issue that's easy to replicate: when doing #check Nat and ctrl+clicking on it, it opens Prelude.lean but I can't ctrl+click anything there

[Henrik Böving]

That is because once you are in the compiler you would need a seperate configuration for that to work out properly (the development guide goes into detail about how to set that up) its not the fault of the plugin

[Sebastian Ullrich]

No, there is no inherent problem with browsing the Lean part of the stdlib taken from a release without further setup, and in fact it just works in Emacs. But that is because lsp-mode will automatically open a workspace (or ask you about it) when you enter a separate project, while in VS Code opening a workspace is always an explicit action afaik.

[Arthur Paulino]

I have (vague) memories of being able to do it a few weeks ago

[Sebastian Ullrich]

Yes, I accidentally opened a VS Code copy with an older extension version and it worked for me as well

[Sebastian Ullrich]

There have been quite a few fundamental changes in the extension in the recent past, some breakage is to be expected

[Sebastian Ullrich]

https://github.com/leanprover/vscode-lean4/issues/115