Zulip Chat Archive

Stream: general

Topic: lean 3.7.2 failed to download


Johan Commelin (Mar 24 2020 at 10:47):

jmc@atarrimbo:~/data/math/mathlib$ cat leanpkg.toml
[package]
name = "mathlib"
version = "0.1"
lean_version = "leanprover-community/lean:3.7.2"
path = "src"

[dependencies]
jmc@atarrimbo:~/data/math/mathlib$ leanpkg build
info: downloading component 'lean'
Error(Download(HttpStatus(401)), State { next_error: None, backtrace: None })
error: could not download nonexistent lean version `leanprover-community-lean-3.7.2`
info: caused by: could not download file from 'https://github.com/leanprover-community/lean/releases/tag/v3.7.2' to '/home/jmc/.elan/tmp/4quei8pkn5hb4ajo_file'
info: caused by: http request returned an unsuccessful status code: 401

Johan Commelin (Mar 24 2020 at 10:50):

I'm confused. Because last week elan worked fine for me. And 3.7.2 seems to be properly released.

Gabriel Ebner (Mar 24 2020 at 10:52):

@Sebastian Ullrich

Sebastian Ullrich (Mar 24 2020 at 10:54):

oh no

Patrick Massot (Mar 24 2020 at 10:55):

Did you try upgrading elan?

Sebastian Ullrich (Mar 24 2020 at 10:55):

Is it reproducible? Can you access that URL in a browser?

Johan Commelin (Mar 24 2020 at 10:56):

This worked

elan toolchain install leanprover-community/lean:3.7.2

Johan Commelin (Mar 24 2020 at 10:56):

It was a fresh elan install

Sebastian Ullrich (Mar 24 2020 at 10:56):

Looks like a Github hiccup

Johan Commelin (Mar 24 2020 at 10:59):

Ok, let's ignore this


Last updated: Dec 20 2023 at 11:08 UTC