New project setup

Stream: general

[Eric Rodriguez]

I'm creating a new project, and I'm just wondering if this error message is to be expected?

mathlib: running post-update hooks
could not execute external process '/Users/ericr/.elan/bin/elan'
error: mathlib: failed to fetch cache

[Mario Carneiro]

no, that looks bad

[Mario Carneiro]

is /Users/ericr/.elan/bin/elan missing or does it have the wrong permissions?

[Eric Rodriguez]

> ls ~/.elan/
settings.toml   tmp     toolchains  update-hashes

[Eric Wieser]

which elan?

[Eric Rodriguez]

/usr/local/bin/elan

[Mario Carneiro]

this is what mine looks like:

$ ls ~/.elan
bin  env  settings.toml  tmp  toolchains  update-hashes

[Eric Wieser]

I think this will be fixed by #8401

[Mario Carneiro]

elan --version?

[Eric Wieser]

I suspect this is a package-manager install rather than an elan shell script install

[Eric Rodriguez]

Mario Carneiro said:

elan --version?

elan 1.4.2 ( ) which is mildly confusing

[Mario Carneiro]

I have elan 3.0.0 (cdb40bff5 2023-09-08)

[Mario Carneiro]

probably you should follow other Eric's suggestion and uninstall this elan and use the shell script instead

[Mario Carneiro]

what is getElan? doing in #8401, is this just a bad function?

[Mario Carneiro]

apparently it is elan from the path, unless ELAN_HOME environment var is set in which case it uses that

[Mario Carneiro]

so I guess #8401 is the right fix in the case when the .elan directory doesn't have the bin in it

[Sebastian Ullrich]

There is already a discussion at #mathlib4 > lake update: invalid toolchain name