toolchain problem

Stream: general

[Kevin Buzzard]

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]

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]

What about rm -rf .elan and start again?

[Kevin Buzzard]

good idea!

[Patrick Massot]

a less violent thing to try would be to also get rid of 3.4.2 in update-hashes

[Kevin Buzzard]

Yeah, that did it. Thanks.

[Kevin Buzzard]

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.