-
Notifications
You must be signed in to change notification settings - Fork 36
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Could not resolve host in elan toolchain install #112
Comments
@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 On both elan toolchain install leanprover/lean4:v4.2.0-rc1 on ooo I get:
and on toothbrush I get:
which I also found to be weird. I tried a variant: elan toolchain install leanprover/lean4:stable which on toothbrush resulted in:
I'm not sure why stable worked, but v4.2.0-rc1 gave the unchanged message. And on ooo I get:
And with backtrace I get:
with the full stack being:
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: |
When trying to install a fresh elan installation I'm running into the same error.
It did install elan and other lean related programs, but it seems to me that it failed installing a toolchain. I can run
Running the suggested command causes the original error again. elan version: |
@Erotemic probably you have DNS lookup problems like me. you see, i got the same error when i tried to download i'm hoping for the dynamically linked |
@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:
|
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
The text was updated successfully, but these errors were encountered: