hiccup with VS Code after upgrade

Stream: general

[Assaf Kfoury]

VS Code behaved nicely for months until I upgraded my Linux Ubuntu laptop to Linux Ubuntu 22.04. I now get this error message:

info: downloading component 'lean'
error: binary package was not provided for 'linux'

Anyone encountered the same? What's the fix?

[Kalle Kytölä]

I think I had that, too. If I remember correctly, elan self update helped.

[Johan Commelin]

It's indeed an elan issue.

[Patrick Massot]

To be clear: this has nothing to do with VSCode or your Ubuntu upgrade. It has to do with trying to update Lean using an outdated elan.

[Assaf Kfoury]

Many thanks! Indeed, the problem was with "elan". Easy fix: "elan self update".