Assaf Kfoury (Oct 31 2022 at 20:52):
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ä (Oct 31 2022 at 20:56):
I think I had that, too. If I remember correctly,
elan self update helped.
Johan Commelin (Oct 31 2022 at 20:57):
It's indeed an
Patrick Massot (Oct 31 2022 at 21:02):
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 (Oct 31 2022 at 21:44):
Many thanks! Indeed, the problem was with "elan". Easy fix: "elan self update".
Last updated: Aug 03 2023 at 10:10 UTC