VS Code error too big to remove

Stream: general

[Kevin Buzzard]

I was reviewing a PR which added a new file Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean. I was editing the file, maybe I saved my edits, maybe I didn't, it doesn't matter, it's not my PR. I then closed VS Code, and later on switched to master on the command line, stashing my changes in the process, and typed code ., and I was faced with this:

Screenshot-from-2024-06-26-22-23-16.png

I can't click anything, drag anything, close the error box, or use VS Code at all. The only thing I can do is exit and then try code . again where the same thing happens. I'm sure I'll be able to fix it perhaps by switching back to the PR I was reviewing or popping my stash or whatever, but this is certainly a bit weird and it's not the first time I've had such a scary popup recently, but I'd never seen such things before until a couple of days ago.

Edit: indeed switching back to the PR, closing the unsaved Quasicoherent.lean file in VS Code and then switching back to master has got me up and running again. But should this be happening at all?

[Shreyas Srinivas]

That's just nodejs spitting out an entire stack trace to tell you that the file it is trying to open doesn't exist

[Shreyas Srinivas]

Usually vscode knows how to handle this situation smoothly, so this could just be some missing error handling code in the extension. Less likely, it could be a bug introduced in some recent vscode version

[Shreyas Srinivas]

One thing you can try is move your vscode back a couple of versions or so and see if you get it again

[Shreyas Srinivas]

If as I recall, you are on ubuntu, and you installed vscode from the snap store then it is quite easy to do this revert

[Shreyas Srinivas]

But I want to confirm this before going on any further

[Kevin Buzzard]

I'm afraid I have no memory of how I installed VS Code, but I will confess that I'm also unlikely to start fiddling with my system getting earlier versions of software.

[Shreyas Srinivas]

What does snap list code give you (on the terminal)

[Shreyas Srinivas]

Sorry changed the command there a bit

[Shreyas Srinivas]

If you are using a snap store version of vscode, reverting to an old version and then back to a new version can be done with zero trouble. I did that twice this month because of some weird vscode bugs in the latest versions. I am trying to rule out the possibility that the issue lies with a recent update of vscode itself as opposed to the extension which is a distinct possibility.

[Kevin Buzzard]

error: no matching snaps installed

[Shreyas Srinivas]

okay then it isn't that simple

[Marc Huisinga]

The scary popups are deliberate. We now display them when activating the extension would otherwise fail due to internal bugs, which would otherwise leave users confused about why their Lean does not work. So the error is likely old, but the fact that we display it is new.

It's very unfortunate that the VS Code UX is so bad when the error is too large and I'll fix that ASAP. I'll also look into the error you reported. Please keep reporting these kinds of errors so that we can fix these bugs.

[Shreyas Srinivas]

Can't they go into the debug console and be truncated?

[Marc Huisinga]

That's where they went since the Lean 4 VS Code extension started and nobody reported them.

[Marc Huisinga]

The debug console is also not sufficiently visible for users to understand why their Lean 4 extension doesn't work when it fails to launch due to an internal error.

[Shreyas Srinivas]

Then maybe a toast with just the last two lines of the stacktrace will get their attention?

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

(To unfamiliar readers: toast refers to the error box that pops up on the lower right hand corner when something goes wrong)

[Marc Huisinga]

Both the excessively large error popup and the error itself should be resolved by vscode-lean4#488, which is now available in 0.0.170.

The issue was that when you have unsaved changes in a file, close VS Code, delete the file (e.g. by switching branches) and then re-open VS Code, VS Code tells us about this file with unsaved changes as if it actually exists in the file system. One place in the extension was not resilient against this, and so it crashed.
This issue was introduced more than two years ago and started affecting the activation of the VS Code extension a couple of months ago.

[Shreyas Srinivas]

Vscode doesn't tell the user that the file exists. It shows the title of such files with a strikethrough so it clearly knows it is showing a file that isn't in the folder when vscode is reopened. But the extension API might not reflect this fact.

[Marc Huisinga]

Shreyas Srinivas said:

Vscode doesn't tell the user that the file exists.

It does when you have unsaved changes in that file before deleting it. In the case where VS Code shows the file with a strikethrough, it doesn't inform the extension about this file, either.
image.png