Zulip Chat Archive

Stream: general

Topic: Error "downloading component"


Wrenna Robson (Aug 22 2022 at 09:03):

When I start up VS Code and open mathlib, I'm getting the following error:

info: downloading component 'lean'
cannot parse: Error(Download(Msg("error during download")), State { next_error: Some(Error { description: "Timeout was reached", code: 28, extra: Some("SSL connection timeout") }), backtrace: InternalBacktrace { backtrace: None } })
error: could not download file from 'https://github.com/leanprover-community/lean/releases/tag/v3.46.0' to '/home/wrobson/.elan/tmp/bx0vsjdbb0pcppwu_file'
info: caused by: error during download
info: caused by: [28] Timeout was reached (SSL connection timeout)

To be clear, my internet is working as far as I can tell! And this was fine before my vacation. But I just upgraded mathlib and now I'm getting this. Do I need to upgrade something else? Anyone know what's up?

Wrenna Robson (Aug 22 2022 at 09:06):

Fixed my own problem. Needed to run elan update.


Last updated: Dec 20 2023 at 11:08 UTC