Zulip Chat Archive

Stream: mathlib4

Topic: post-update hook failure

Mario Carneiro (Dec 22 2023 at 08:34):

$ lake update
...
mathlib: running post-update hooks
error: toolchain 'leanprover/lean4:v4.5.0-rc1' is not installed
error: mathlib: failed to fetch cache

Running lake update twice in a row fixes the issue.

Mario Carneiro (Dec 22 2023 at 08:35):

I think this is because the post update hook calls elan in a special way (cc: @Mac Malone @Sebastian Ullrich ) which prevents it from attempting to download the toolchain?

Mario Carneiro (Dec 22 2023 at 08:37):

looks like the hook calls elan run leanprover/lean4:v4.5.0-rc1 lake exe cache get, which I did not know was a thing

Mario Carneiro (Dec 22 2023 at 08:38):

does this need some kind of --allow-download flag?

Sebastian Ullrich (Dec 22 2023 at 08:44):

$ elan run --help
elan-run
Run a command with an environment configured for a given toolchain

USAGE:
    elan run [FLAGS] <toolchain> <command>...

FLAGS:
    -h, --help       Prints help information
        --install    Install the requested toolchain if needed

Mario Carneiro (Dec 22 2023 at 08:45):

how does this differ from elan +toolchain command?

Sebastian Ullrich (Dec 22 2023 at 08:45):

lean +t is effectively elan run --install t lean

Mario Carneiro (Dec 22 2023 at 08:46):

hm, that makes me nervous then because I was thinking of just adding --install to the invocation

Mario Carneiro (Dec 22 2023 at 08:47):

the comment says

    /-
    Instead of building and running cache via the Lake API,
    spawn a new `lake` since the toolchain may have changed.
    -/
    let exitCode ← IO.Process.spawn {
      cmd := "elan"
      args := #["run", mathlibToolchain.trim, "lake", "exe", "cache", "get"]
    } >>= (·.wait)

Mario Carneiro (Dec 22 2023 at 08:47):

Oh right, now I remember, this is because using elan normally pins the version because of an env var

Sebastian Ullrich (Dec 22 2023 at 08:48):

Yeah, things like this need to be documented as comments

Mario Carneiro (Dec 22 2023 at 08:48):

does elan +toolchain in a nested invocation also ignore the passed toolchain and use the pin?

Sebastian Ullrich (Dec 22 2023 at 08:49):

I don't think you can use elan itself with +

Mario Carneiro (Dec 22 2023 at 08:50):

er, I meant lake +toolchain

Sebastian Ullrich (Dec 22 2023 at 08:50):

But otherwise I would really hope it would use toolchain

Mario Carneiro (Dec 22 2023 at 08:50):

really? Using +toolchain seems like it should take precedence

Mario Carneiro (Dec 22 2023 at 08:51):

but surely that was the first thing that was tried here

Sebastian Ullrich (Dec 22 2023 at 08:51):

Yes, I edited my comment

Sebastian Ullrich (Dec 22 2023 at 08:53):

Running elan directly could create a more sensible error message in case someone uses Lean without elan

Mario Carneiro (Dec 22 2023 at 08:57):

not really, any error message is > /dev/null :upside_down:

Mario Carneiro (Dec 22 2023 at 08:57):

cc: @Mac Malone then since they wrote this code

Sebastian Ullrich (Dec 22 2023 at 08:58):

I don't see a stderr redirect in the above code?

Mario Carneiro (Dec 22 2023 at 08:58):

oh wait no that's a lie, it inherits stdout and stderr

Sebastian Ullrich (Dec 22 2023 at 08:59):

You started the thread with output from elan in that very call :)

Mario Carneiro (Dec 22 2023 at 09:02):

#9197

Sebastian Ullrich (Dec 22 2023 at 09:04):

I also fixed a related elan docbug that I think was inherited from rustup https://github.com/leanprover/elan/commit/640358e252e6eda100ed4a96a993b2bbb97d0574

Moritz Firsching (Jan 04 2024 at 15:42):

In the Using mathlib as dependency wiki, it still says one should run

curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake update
lake exe cache get

With the post-update hook, running lake exe cache get should be superfluous now, right?

Ruben Van de Velde (Jan 04 2024 at 15:55):

I think so, yes

Moritz Firsching (Jan 04 2024 at 16:28):

Ok, I will edit the wiki accordingly.

Moritz Firsching (Jan 04 2024 at 16:31):

done

Kevin Buzzard (Jan 04 2024 at 16:56):

Heh, I just updated mathlib as a dependency on a project and can confirm that the new instructions worked for me :-)

Last updated: May 02 2025 at 03:31 UTC