Open Erotemic opened 1 year ago
@Erotemic, I'm going to guess this was a transient problem at github. If you can still reproduce a day later, could you ping here and we can look at it?
It is still failing. This might be some setting on my machine, but I can't think of what it would be. I have two machines with nearly the same setup, the main difference is one is running 2010 hardware (ooo) and another is running 2020 hardware (toothbrush). On both my machines, I moved the toolchain
folder in ~/.elan
to toolchain-old
and reran:
On both elan toolchain list
reports no installed toolchains, but when running:
elan toolchain install leanprover/lean4:v4.2.0-rc1
on ooo I get:
info: downloading component 'lean'
Error(Download(Msg("error during download")), State { next_error: Some(Error { description: "Couldn't resolve host name", code: 6, extra: Some("Could not resolve host: github.com") }), backtrace: InternalBacktrace { backtrace: None } })
error: could not download file from 'https://github.com/leanprover/lean4/releases/expanded_assets/v4.2.0-rc1' to '/home/joncrall/.elan/tmp/5e3yjgdnzdija3mx_file'
info: caused by: error during download
info: caused by: [6] Couldn't resolve host name (Could not resolve host: github.com)
and on toothbrush I get:
leanprover/lean4:v4.2.0-rc1 unchanged - (toolchain not installed)
which I also found to be weird. I tried a variant:
elan toolchain install leanprover/lean4:stable
which on toothbrush resulted in:
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.1.0
info: downloading component 'lean'
179.2 MiB / 179.2 MiB (100 %) 7.8 MiB/s ETA: 0 s
info: installing component 'lean'
I'm not sure why stable worked, but v4.2.0-rc1 gave the unchanged message.
And on ooo I get:
info: syncing channel updates for 'stable'
thread 'main' panicked at 'called `Result::unwrap()` on an `Err` value: Error { description: "Couldn't resolve host name", code: 6, extra: Some("Could not resolve host: github.com") }', src/elan-utils/src/utils.rs:514:32
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
And with backtrace I get:
info: syncing channel updates for 'stable'
thread 'main' panicked at 'called `Result::unwrap()` on an `Err` value: Error { description: "Couldn't resolve host name", code: 6, extra: Some("Could not resolve host: github.com") }', src/elan-utils/src/utils.rs:514:32
stack backtrace:
0: rust_begin_unwind
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/panicking.rs:593:5
1: core::panicking::panic_fmt
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/core/src/panicking.rs:67:14
2: core::result::unwrap_failed
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/core/src/result.rs:1651:5
3: elan_utils::utils::fetch_url
4: elan_utils::utils::fetch_latest_release_tag
5: elan_dist::dist::update_from_dist_
6: elan_dist::dist::update_from_dist
7: elan::install::InstallMethod::run
8: elan::toolchain::Toolchain::install
9: elan::toolchain::Toolchain::install_from_dist
10: elan_init::elan_mode::update
11: elan_init::elan_mode::main
12: elan_init::main
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
with the full stack being:
info: syncing channel updates for 'stable'
thread 'main' panicked at 'called `Result::unwrap()` on an `Err` value: Error { description: "Couldn't resolve host name", code: 6, extra: Some("Could not resolve host: github.com") }', src/elan-utils/src/utils.rs:514:32
stack backtrace:
0: 0x7f805bbefb11 - std::backtrace_rs::backtrace::libunwind::trace::h752edb5e763c622a
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
1: 0x7f805bbefb11 - std::backtrace_rs::backtrace::trace_unsynchronized::h186570be9d64c708
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
2: 0x7f805bbefb11 - std::sys_common::backtrace::_print_fmt::h3c97392bc43f6100
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/sys_common/backtrace.rs:65:5
3: 0x7f805bbefb11 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h0a500936d7ce1aa3
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/sys_common/backtrace.rs:44:22
4: 0x7f805bc3c36f - core::fmt::rt::Argument::fmt::h49d8384db0e23147
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/core/src/fmt/rt.rs:138:9
5: 0x7f805bc3c36f - core::fmt::write::hceee497f41d5c978
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/core/src/fmt/mod.rs:1094:21
6: 0x7f805bbebcb7 - std::io::Write::write_fmt::h95250bef2fd518bf
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/io/mod.rs:1714:15
7: 0x7f805bbef925 - std::sys_common::backtrace::_print::ha8144dbed1846c2c
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/sys_common/backtrace.rs:47:5
8: 0x7f805bbef925 - std::sys_common::backtrace::print::hf483708776650079
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/sys_common/backtrace.rs:34:9
9: 0x7f805bbf0ee3 - std::panicking::default_hook::{{closure}}::hf31b00cbd6179696
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/panicking.rs:269:22
10: 0x7f805bbf0c74 - std::panicking::default_hook::hb91091ef23c52620
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/panicking.rs:288:9
11: 0x7f805bbf1469 - std::panicking::rust_panic_with_hook::h1637607b7d82e47f
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/panicking.rs:705:13
12: 0x7f805bbf1367 - std::panicking::begin_panic_handler::{{closure}}::hefcd5d25990c0376
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/panicking.rs:597:13
13: 0x7f805bbeff76 - std::sys_common::backtrace::__rust_end_short_backtrace::h74318f6f4a659750
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/sys_common/backtrace.rs:151:18
14: 0x7f805bbf10b2 - rust_begin_unwind
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/panicking.rs:593:5
15: 0x7f805b787903 - core::panicking::panic_fmt::h1cdc5ad0767cefdc
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/core/src/panicking.rs:67:14
16: 0x7f805b787da3 - core::result::unwrap_failed::h0fba1ec415bdc4a5
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/core/src/result.rs:1651:5
17: 0x7f805b8fdd00 - elan_utils::utils::fetch_url::h61908eec202ff432
18: 0x7f805b8fdeaf - elan_utils::utils::fetch_latest_release_tag::h26b3b2f8d26eaf0e
19: 0x7f805b866090 - elan_dist::dist::update_from_dist_::h658d6cd873d7e2e5
20: 0x7f805b865823 - elan_dist::dist::update_from_dist::hf8f15589da492bb3
21: 0x7f805b7f6fe4 - elan::install::InstallMethod::run::hcb83ed7990548610
22: 0x7f805b7e55ef - elan::toolchain::Toolchain::install::h7489e05e37daa148
23: 0x7f805b7e57b3 - elan::toolchain::Toolchain::install_from_dist::h9c3bd1d92802adb2
24: 0x7f805b7a0316 - elan_init::elan_mode::update::he5a495aa7f13c835
25: 0x7f805b79cfd5 - elan_init::elan_mode::main::h26b7f887853f8ae8
26: 0x7f805b7c16cf - elan_init::main::hf84f4544d6e5cbd5
27: 0x7f805b7b1663 - std::sys_common::backtrace::__rust_begin_short_backtrace::h3147485e1feaa76b
28: 0x7f805b7b2399 - std::rt::lang_start::{{closure}}::h658c53cb01f309ea
29: 0x7f805bbe50f2 - core::ops::function::impls::<impl core::ops::function::FnOnce<A> for &F>::call_once::h53f7fdef9fa97f44
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/core/src/ops/function.rs:284:13
30: 0x7f805bbe50f2 - std::panicking::try::do_call::h241dc6f55f440bfa
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/panicking.rs:500:40
31: 0x7f805bbe50f2 - std::panicking::try::h6fa7a7ecf68ec302
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/panicking.rs:464:19
32: 0x7f805bbe50f2 - std::panic::catch_unwind::h3adf6baef0afdbb9
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/panic.rs:142:14
33: 0x7f805bbe50f2 - std::rt::lang_start_internal::{{closure}}::hf1cf4178cf5b8437
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/rt.rs:148:48
34: 0x7f805bbe50f2 - std::panicking::try::do_call::h7dbeb5f468ea2e7a
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/panicking.rs:500:40
35: 0x7f805bbe50f2 - std::panicking::try::h34a81bcdebb1642f
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/panicking.rs:464:19
36: 0x7f805bbe50f2 - std::panic::catch_unwind::hdd88670df2ed76f9
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/panic.rs:142:14
37: 0x7f805bbe50f2 - std::rt::lang_start_internal::h312f4ba9c2a0dedf
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/rt.rs:148:20
38: 0x7f805b7c19e5 - main
I don't know why the machines have different results. They are on the same network, and I tend to keep them in sync with each other. Both run ubuntu 22.04 and they ahve teh same elan version: elan 3.0.0 (cdb40bff5 2023-09-08)
. This also seems like a slightly different error than I originally reported. Any help debugging would be appreciated.
When trying to install a fresh elan installation I'm running into the same error.
$ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
...
Current installation options:
default toolchain: stable
modify PATH variable: yes
1) Proceed with installation (default)
2) Customize installation
3) Cancel installation
1
info: syncing channel updates for 'stable'
thread 'main' panicked at 'called `Result::unwrap()` on an `Err` value: Error { description: "Couldn't resolve host name", code: 6, extra: Some("Could not resolve host: github.com") }', src/elan-utils/src/utils.rs:514:32
stack backtrace:
0: rust_begin_unwind
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/std/src/panicking.rs:593:5
1: core::panicking::panic_fmt
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/core/src/panicking.rs:67:14
2: core::result::unwrap_failed
at /rustc/5680fa18feaa87f3ff04063800aec256c3d4b4be/library/core/src/result.rs:1651:5
3: elan_utils::utils::fetch_url
4: elan_utils::utils::fetch_latest_release_tag
5: elan_dist::dist::update_from_dist_
6: elan_dist::dist::update_from_dist
7: elan::install::InstallMethod::run
8: elan::toolchain::Toolchain::install
9: elan::toolchain::Toolchain::install_from_dist
10: elan_init::self_update::install
11: elan_init::setup_mode::main
12: elan_init::main
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
It did install elan and other lean related programs, but it seems to me that it failed installing a toolchain. I can run lean
now, but it just reports the following error:
error: no default toolchain configured. run `elan default stable` to install & configure the latest Lean 4 stable release.
Running the suggested command causes the original error again.
elan version: elan 3.0.0 (cdb40bff5 2023-09-08)
i'm having the same problem in Termux
. but my problem is known. since elan
is a statically linked binary that does networking stuff and Termux
is not FHS
compliant it can't resolve DNS names
because /etc/resolv.conf
doesn't exist in Termux. so every time i'm downloading something with elan
i have to launch Termux's proot script for resolv.conf
to be accessible. it would be nice if there were a dynamically linked glibc based elan
binary for Linux/aarch64
like rustup
. so we don't have to install slow Termux
proot distros
to use these tools.
rustup
working without entering proot
sorry for my English.
@Erotemic probably you have DNS lookup problems like me. you see, i got the same error when i tried to download lean
but when elan
is pointed to the right resolv.conf
using proot -b
command it's working fine.
i'm hoping for the dynamically linked elan
binary for Linux Arm64. glibc would deal with the DNS lookups
. i guess.
@dhuux Did you manage to get lake to run? I was able to install the toolchain but whenever I try running lake I just get:
error: command failed 'lake'
info: caused by: No such file or directory (os error 2)
I'm encountering an error while trying to install a specific lean toolchain with elan. I'm not sure what could be happening, if this is a problem with elan, or if this is a user-error (and perhaps in need of documentation?).
Running:
Results in
However, I can
ping github.com
just fine.Adding
export RUST_BACKTRACE=1
results inI installed elan with the following commands:
Environment
Elan version:
OS: Ubuntu 22.04