error: toolchain 'leanprover-community-lean-3.17.1' is not i

Stream: general

[Kevin Buzzard]

woo I got my laptop charged so now I have a couple of hours of Lean. Except I broke my installation :-(

error: toolchain 'leanprover-community-lean-3.17.1' is not installed

Indeed I have removed ~/.elan/toolchains/leanprover-community-lean-3.17.1. How do I get it back?

[Reid Barton]

maybe elan toolchain uninstall leanprover-community-lean-3.17.1?

[Reid Barton]

then run elan again

[Kevin Buzzard]

PS yesterday I learnt that starting to think about unifying monoid.pow and nat.pow in a field with no internet might not be a good idea, because editing core might mean a lot of recompiling

[Kevin Buzzard]

I still have error: toolchain 'leanprover-community-lean-3.17.1' is not installed if I open mathlib in VS Code.

$ elan toolchain install leanprover-community-lean-3.17.1
info: downloading component 'lean'
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: None })
error: could not download nonexistent lean version `leanprover-community-lean-3.17.1`
info: caused by: could not download file from 'https://github.com/leanprover/lean/releases/tag/leanprover-community-lean-3.17.1' to '/home/buzzard/.elan/tmp/80vik336h7fpqcyi_file'
info: caused by: http request returned an unsuccessful status code: 404
buzzard@ebony:~/.elan/toolchains$

[Kevin Buzzard]

buzzard@ebony:~$ elan toolchain install leanprover-community:lean-3.17.1
error: invalid toolchain name: 'leanprover-community:lean-3.17.1'
buzzard@ebony:~$ elan toolchain install leanprover-community/lean-3.17.1
error: invalid toolchain name: 'leanprover-community/lean-3.17.1'
buzzard@ebony:~$ elan toolchain install git@github.com/leanprover-community/leanprover-community-lean-3.17.1
error: invalid toolchain name: 'git@github.com/leanprover-community/leanprover-community-lean-3.17.1'
buzzard@ebony:~$

waaah

[Rob Lewis]

Did you change a / to a - in your leanpkg.toml?

[Kevin Buzzard]

I didn't change anything in the toml. I just deleted the subdirectory of .elan because I edited it and it made everything recompile

[Rob Lewis]

elan toolchain install leanprover-community-lean-3.17.1 should be elan toolchain install leanprover-community/lean-3.17.1 I think

[Rob Lewis]

I'm not 100% sure there but https://github.com/leanprover/lean/releases/tag/leanprover-community-lean-3.17.1 is clearly wrong...

[Kevin Buzzard]

$ elan toolchain install leanprover-community/lean-3.17.1
error: invalid toolchain name: 'leanprover-community/lean-3.17.1'

oh what have I done. I don't understand why leanproject up might change the toml to a new thing and then a new lean automatically gets downloaded, but I can't emulate this here

[Kevin Buzzard]

$ elan toolchain install leanprover-community/lean:3.17.1

  leanprover-community-lean-3.17.1 unchanged - (toolchain not installed)

[Patrick Massot]

It's part of leanproject's job to make sure you don't have a clue about using elan directly.

[Kevin Buzzard]

$ elan show
installed toolchains
--------------------

stable
nightly-2018-04-20
nightly-2018-06-21
nightly-2019-01-13
leanprover-community-lean-3.10.0
leanprover-community-lean-3.11.0
leanprover-community-lean-3.13.2
leanprover-community-lean-3.14.0
leanprover-community-lean-3.15.0
leanprover-community-lean-3.16.2
leanprover-community-lean-3.16.3
leanprover-community-lean-3.16.4
leanprover-community-lean-3.16.5
leanprover-community-lean-3.17.0 (default)
leanprover-community-lean-3.5.0
leanprover-community-lean-3.5.1
leanprover-community-lean-3.6.1
leanprover-community-lean-3.7.0
leanprover-community-lean-3.7.1
leanprover-community-lean-3.7.2
leanprover-community-lean-3.8.0
leanprover-community-lean-3.9.0
3.4.1
3.4.2

active toolchain
----------------

leanprover-community-lean-3.17.0 (default)
Lean (version 3.17.0, commit 5d8f59fd1d49, Release)

[Kevin Buzzard]

OK I'll try leanproject get mathlib even though it's going to take a loong time and cost me a lot of data :-/

[Markus Himmel]

I know this bug

[Patrick Massot]

What about doing whatever normal people do during their vacations?

[Markus Himmel]

You need to remove .elan/update-hashes/leanprover-community-lean-3.17.1 and then the elan toolchain install leanprover-community-lean-3.17.1 will work

[Kevin Buzzard]

Patrick Massot said:

What about doing whatever normal people do during their vacations?

BECAUSE I HAVE TO REFACTOR SUBGROUPS

[Patrick Massot]

Yeah, Lean is no so healthy in the long run.

[Kevin Buzzard]

Thanks Markus!