Failing to install elan

Stream: lean4

[Frédéric Dupuis]

I have just bought a new laptop (yay!), and I'm trying to set up Lean on it, and the elan installation script doesn't work for some reason. Here's what I'm getting from elan-init.sh (I get the same thing when running it in VSCode like in the instructions):

Welcome to Lean!

This will download and install Elan, a tool for managing different Lean
versions used in packages you create or download. It will also install a
default version of Lean and its package manager, lake, for editing files not
belonging to any package.

It will add the lake, lean, and elan commands to Elan's bin directory, located
at:

  /home/fred/.elan/bin

This path will then be added to your PATH environment variable by modifying the
profile files located at:

  /home/fred/.profile
  /home/fred/.zprofile
  /home/fred/.bash_profile

You can uninstall at any time with elan self uninstall and these changes will
be reverted.

Current installation options:

     default toolchain: stable
  modify PATH variable: yes

1) Proceed with installation (default)
2) Customize installation
3) Cancel installation


error: error during download
info: caused by: [6] Could not resolve hostname (Could not resolve host: release.lean-lang.org)

My internet connection is working, and I can in fact reach release.lean-lang.org in my browser. I have both curl and git installed. Any idea what's going on?

[Julian Berman]

What does curl -v https://release.lean-lang.org show?

[Frédéric Dupuis]

A massive json file with all previous releases.

[Julian Berman]

OK that's .. a good sign clearly.

[Julian Berman]

Ah, that error comes from rust (calling out to libcurl), not curl (the binary) -- so somehow the former isn't working and the latter is. I'm not sure offhand why that'd be -- perhaps a step is to compare the output of ldd $(which curl) and ldd $(which elan) and see which libcurls they're using.

[Frédéric Dupuis]

The elan-init executable that gets run by the script is statically linked according to ldd, so presumably my version of libcurl shouldn't matter...?

[Ben Eltschig]

I'm currently running into a similar issue on my linux laptop: I've used lean on it before and in the repositories I already have installed commands like lake build in lake exe cache get still work fine, but in newly-cloned repositories and repositories where my installed toolchain is outdated any attempts to use lake or install the correct toolchain result in that [6] Could not resolve hostname (Could not resolve host: github.com) error, even though loading github in the browser, pinging it, and running commands like curl https://github.com all work. It does seem like a network issue, but like one that is very specific to whatever elan does / uses under the hood - does anyone have an idea what I can do to fix it? I already tried e.g. temporarily disabling my firewall (it didn't help) and updating elan via curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y (turns out I already had the most recent version 4.1.12).

[Ben Eltschig]

Just to give an update to this in case anyone else encounters a similar issue in the future - in my case the issue resolved itself after just waiting for a few weeks and then installing updates. Maybe a bug in one of the dependencies like libcurl produced this issue and was patched out a bit later, I don't know.