elan panic

Stream: general

[Michael Rothgang]

I just encountered an unexpected elan panic: running lake exe cache get yielded

thread 'main' panicked at src/elan-utils/src/utils.rs:472:32:
called `Result::unwrap()` on an `Err` value: Error { description: "Couldn't resolve host name", code: 6, extra: Some("Could not resolve host: github.com") }
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

CC @Sebastian Ullrich You may be interested.

Detail to reproduce/relevant facts.

• Run on current mathlib master (revision 61161724286)
• I didn't have Lean 4.15 or 4.16.0-rc1 downloaded yet; this is what the cache is downloading right now
• this was when switching wifi connections from one network to another, this might have caused some race condition
• I use Debian/Linux (stable)

[Joachim Breitner]

“Could not resolve hostname” sounds like a simple network issue. Did it work when you tried again once you have switched to another network?

[Michael Rothgang]

Yes, then it worked again.

[Michael Rothgang]

To clarify: elan being unable to download Lean when there's no network is to to be expected :-) elan panicking is not; that is the bug I mean to report.

[Joachim Breitner]

I see, so a UX issue. Feel free to report an issue at https://github.com/leanprover/elan/issues, not sure how pressing it will be, though.

[Marc Huisinga]

Before creating an issue, it would be good to confirm that the issue still occurs with https://github.com/leanprover/elan/releases/tag/eager-resolution-v9.

[Marc Huisinga]

You should be able to run the elan-init.exe from the command line to install the eager toolchain resolution Elan version.