Zulip Chat Archive

Stream: general

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

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):

What about rm -rf .elan and start again?

Kevin Buzzard (Mar 24 2019 at 15:03):

good idea!

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 update-hashes

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: Aug 03 2023 at 10:10 UTC