Lean 4.7.0rc2 error: 4.7.tmp; NixOS

Stream: general

[Yury G. Kudryashov]

I just git pulled Mathlib4 and I get the following error:

/home/urkud/.elan/toolchains/leanprover--lean4---v4.7.0-rc2/bin/leanc: line 2:
/home/urkud/.elan/toolchains/leanprover--lean4---v4.7.tmp/bin/leanc.orig: No such file or directory

I'm on NixOS, so leanc looks like

#! /nix/store/087167dfxal194pm54cmcbbxsfy3cjgn-bash-5.2p26/bin/bash
LEAN_CC="${LEAN_CC:-/nix/store/ln6zld1ia7rxddmxgbpfhrmb42rbxdw8-gcc-wrapper-13.2.0/bin/cc}" exec -a "$0" /home/urkud/.elan/toolchains/leanprover--lean4---v4.7.tmp/bin/leanc.orig "$@" -L /home/urkud/.elan/toolchains/leanprover--lean4---v4.7.tmp/lib  # use bundled libraries, but not bundled compiler that doesn't know about NIX_LDFLAGS

[Yury G. Kudryashov]

If I change both tmp in leanc to 0-rc2, then it works.

[Sebastian Ullrich]

This is #lean4 > elan 3.1.0/3.1.1 on Nixpkgs

[Yury G. Kudryashov]

Thank you!