Topic: toolchain problem
Kevin Buzzard (Mar 24 2019 at 15:00):
I had to get off a computer quick so I exited VS Code and saved everything. Later on it turned out I'd edited a file in core Lean, more precisely, in
~/.elan/toolchains/3.4.2/. I noticed when I typed
lean --make in a project and it started compiling stuff in the toolchains directory :-/ I figured the safest thing to do would just to be to remove that directory completely and re-install. But I can't persuade elan to re-install 3.4.2.
$ elan toolchain install 3.4.2 3.4.2 unchanged - (toolchain not installed) $ elan toolchain uninstall 3.4.2 info: no toolchain installed for '3.4.2' $ elan toolchain list stable nightly-2018-04-20 nightly-2018-06-21 3.3.0 3.4.1
elan update doesn't download it either.
Kevin Buzzard (Mar 24 2019 at 15:01):
Firing up VS Code with a 3.4.2 project gives me
Server has stopped with error code 1. and debug output
error : toolchain '3.4.2' is not installed
Patrick Massot (Mar 24 2019 at 15:03):
rm -rf .elan and start again?
Kevin Buzzard (Mar 24 2019 at 15:03):
Patrick Massot (Mar 24 2019 at 15:05):
a less violent thing to try would be to also get rid of 3.4.2 in
Kevin Buzzard (Mar 24 2019 at 15:05):
Yeah, that did it. Thanks.
Kevin Buzzard (Mar 24 2019 at 15:06):
That was the thing I was missing. Of cousre I shouldn't have deleted the directory -- I just assumed that deleting the directory and then firing up VS Code would fix it. Now I've had a good look at the elan commands and I realise that actually all the tools I needed were available via elan commands.
Last updated: May 17 2021 at 22:15 UTC