Closed nomeata closed 2 months ago
Right now, it tells me that it is downloading lean, but not which toolchain version:
lean
$ lake info: downloading component 'lean' error: binary package was not provided for 'linux'
I think it would give useful ambient information if it would say
$ lake info: downloading component 'lean' from toolchain 'leanprover/lean4:v4.0.0'
(I had a very brief look but it seemed it wouldn’t be a three-line change, so just opening an issue, nor a PR.)
Fixed in https://github.com/leanprover/elan/commit/4e413ea5ec289faede0b3f0b884dbb959dda6295#diff-36708dc8fab8d566c7faf44cd47b23c7870abc48eb10ad16f137b397659736f1R69-R75
Right now, it tells me that it is downloading
lean
, but not which toolchain version:I think it would give useful ambient information if it would say
(I had a very brief look but it seemed it wouldn’t be a three-line change, so just opening an issue, nor a PR.)