Zulip Chat Archive

Stream: general

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


view this post on Zulip Kevin Buzzard (Jul 29 2020 at 19:12):

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?

view this post on Zulip Reid Barton (Jul 29 2020 at 19:26):

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

view this post on Zulip Reid Barton (Jul 29 2020 at 19:26):

then run elan again

view this post on Zulip Kevin Buzzard (Jul 29 2020 at 19:27):

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

view this post on Zulip Kevin Buzzard (Jul 29 2020 at 20:50):

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$

view this post on Zulip Kevin Buzzard (Jul 29 2020 at 20:51):

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

view this post on Zulip Rob Lewis (Jul 29 2020 at 20:52):

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

view this post on Zulip Kevin Buzzard (Jul 29 2020 at 20:52):

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

view this post on Zulip Rob Lewis (Jul 29 2020 at 20:53):

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

view this post on Zulip Rob Lewis (Jul 29 2020 at 20:54):

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

view this post on Zulip Kevin Buzzard (Jul 29 2020 at 20:54):

$ 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

view this post on Zulip Kevin Buzzard (Jul 29 2020 at 20:54):

$ elan toolchain install leanprover-community/lean:3.17.1

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

view this post on Zulip Patrick Massot (Jul 29 2020 at 20:56):

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

view this post on Zulip Kevin Buzzard (Jul 29 2020 at 20:56):

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

view this post on Zulip Kevin Buzzard (Jul 29 2020 at 20:57):

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

view this post on Zulip Markus Himmel (Jul 29 2020 at 20:58):

I know this bug

view this post on Zulip Patrick Massot (Jul 29 2020 at 20:58):

What about doing whatever normal people do during their vacations?

view this post on Zulip Markus Himmel (Jul 29 2020 at 20:59):

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

view this post on Zulip Kevin Buzzard (Jul 29 2020 at 21:07):

Patrick Massot said:

What about doing whatever normal people do during their vacations?

BECAUSE I HAVE TO REFACTOR SUBGROUPS

view this post on Zulip Patrick Massot (Jul 29 2020 at 21:09):

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

view this post on Zulip Kevin Buzzard (Jul 29 2020 at 21:10):

Thanks Markus!


Last updated: May 16 2021 at 05:21 UTC