Zulip Chat Archive

Stream: general

Topic: default toolchain


view this post on Zulip Patrick Massot (Feb 22 2020 at 18:06):

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.

view this post on Zulip Simon Hudon (Feb 22 2020 at 18:56):

@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?

view this post on Zulip Patrick Massot (Feb 22 2020 at 21:33):

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

view this post on Zulip Patrick Massot (Feb 22 2020 at 21:33):

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

view this post on Zulip Patrick Massot (Feb 22 2020 at 21:34):

instead of the correct leanprover-community/lean-3.5.1

view this post on Zulip Sebastian Ullrich (Feb 22 2020 at 21:34):

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

view this post on Zulip Patrick Massot (Feb 22 2020 at 21:36):

You mean a bug in leanpkg from there?

view this post on Zulip Patrick Massot (Feb 22 2020 at 21:36):

Oh but I see you just pushed a new elan.

view this post on Zulip Sebastian Ullrich (Feb 22 2020 at 21:38):

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.

view this post on Zulip Patrick Massot (Feb 22 2020 at 21:39):

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

view this post on Zulip Sebastian Ullrich (Feb 22 2020 at 21:44):

Yes, imo

view this post on Zulip Patrick Massot (Feb 23 2020 at 13:45):

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

view this post on Zulip Simon Hudon (Mar 15 2020 at 15:17):

Is this completely solved?


Last updated: May 12 2021 at 23:13 UTC