search

leanprover / elan

The Lean version manager
Apache License 2.0
310 stars 35 forks source link

elan does not start, complaining about `error: couldn't find value of ELAN_HOME` #109

Open ghost opened 1 year ago

ghost commented 1 year ago

I have built elan 3.0.0 using cargo, according to the AUR's script: https://aur.archlinux.org/packages/elan-lean

I had to update the version.

Now, the command elan , or elan --help produces the following output:

error: couldn't find value of ELAN_HOME
info: caused by: No such file or directory (os error 2)

Would it be possible to make the error more verbose, or, just make it work by default?

kim-em commented 1 year ago

This might be hard to do anything about if we can't reproduce. What exactly do you mean by "I had to update the version"?