default toolchain

Stream: general

[Patrick Massot]

Shouldn't we update our installation docs and scripts to tell people to run elan-init.sh -y --default-toolchain leanprover-community-lean-3.5.1? The problem is we'll need to maintain that.

[Simon Hudon]

@Sebastian Ullrich Did you end up making the change to the default origin for the toolchains in elan? Does this affect which toolchain is installed when install elan?

[Patrick Massot]

Actually I don't know how to use elan here. If I have

$ elan toolchain list
leanprover-community-lean-3.5.1 (default)

Then leanpkg new test works but then leanpkg add leanprover-community/mathlib says:

info: downloading component 'lean'
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: None })
error: could not download nonexistent lean version `3.5.1`
info: caused by: could not download file from 'https://github.com/leanprover/lean/releases/tag/v3.5.1' to '/home/pmassot/.elan/tmp/rkly9ssuw8ovfl67_file'
info: caused by: http request returned an unsuccessful status code: 404

[Patrick Massot]

Because leanpkg new put 3.5.1 as version in leanpkg.toml.

[Patrick Massot]

instead of the correct leanprover-community/lean-3.5.1

[Sebastian Ullrich]

That is a bug of leanprover-community/lean then, not elan

[Patrick Massot]

You mean a bug in leanpkg from there?

[Patrick Massot]

Oh but I see you just pushed a new elan.

[Sebastian Ullrich]

Yes, but it will not fix this issue. In fact I was about to test whether the leanpkg.toml is created correctly, but you've already done that for me.

[Patrick Massot]

So it's a bug in https://github.com/leanprover-community/lean/tree/master/leanpkg, right?

[Sebastian Ullrich]

Yes, imo

[Patrick Massot]

I opened https://github.com/leanprover-community/lean/issues/126

[Simon Hudon]

Is this completely solved?