`lake update` fails in new project with mathlib dependency (No such file or directory)

[rj00a]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Running lake update on a new project created with the math package template fails. Errors are of the form

error: stderr:
/home/rj/.elan/toolchains/leanprover--lean4---v4.7.0/bin/leanc: line 2: /home/rj/.elan/toolchains/leanprover--lean4---v4.7.tmp/bin/leanc.orig: No such file or directory
error: external command `/home/rj/.elan/toolchains/leanprover--lean4---v4.7.0/bin/leanc` exited with code 127

Context

I'm a new Lean user and followed the instructions for setting up a new project here.

Steps to Reproduce

1. lake +nightly new lean-math math
2. cd lean-math
3. lake update

Expected behavior:

lake update succeeds without errors.

Actual behavior:

lake update fails.

Full Output

rj@pop-os ~/dev/lean-math (main)> lake +nightly update
lean-math: no previous manifest, creating one from scratch
mathlib: cloning https://github.com/leanprover-community/mathlib4.git to '././.lake/packages/mathlib'
std: cloning https://github.com/leanprover/std4 to '././.lake/packages/std'
Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'
importGraph: cloning https://github.com/leanprover-community/import-graph.git to '././.lake/packages/importGraph'
warning: Qq: ignoring missing dependency manifest '././.lake/packages/Qq/lake-manifest.json'
warning: Cli: ignoring missing dependency manifest '././.lake/packages/Cli/lake-manifest.json'
mathlib: running post-update hooks
info: downloading component 'lean'
Total: 168.9 MiB Speed:  30.4 MiB/s
info: installing component 'lean'
info: [0/9] Downloading proofwidgets cloud release
info: [0/9] Unpacking proofwidgets cloud release
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
error: > /home/rj/.elan/toolchains/leanprover--lean4---v4.7.0/bin/leanc -c -o ./.lake/packages/mathlib/.lake/build/ir/Cache/IO.c.o ./.lake/packages/mathlib/.lake/build/ir/Cache/IO.c -O3 -DNDEBUG
error: stderr:
/home/rj/.elan/toolchains/leanprover--lean4---v4.7.0/bin/leanc: line 2: /home/rj/.elan/toolchains/leanprover--lean4---v4.7.tmp/bin/leanc.orig: No such file or directory
error: external command `/home/rj/.elan/toolchains/leanprover--lean4---v4.7.0/bin/leanc` exited with code 127
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
error: > /home/rj/.elan/toolchains/leanprover--lean4---v4.7.0/bin/leanc -c -o ./.lake/packages/mathlib/.lake/build/ir/Cache/Hashing.c.o ./.lake/packages/mathlib/.lake/build/ir/Cache/Hashing.c -O3 -DNDEBUG
error: stderr:
/home/rj/.elan/toolchains/leanprover--lean4---v4.7.0/bin/leanc: line 2: /home/rj/.elan/toolchains/leanprover--lean4---v4.7.tmp/bin/leanc.orig: No such file or directory
error: external command `/home/rj/.elan/toolchains/leanprover--lean4---v4.7.0/bin/leanc` exited with code 127
info: [4/9] Compiling Cache.Requests
info: [4/9] Building Cache.Main
error: > /home/rj/.elan/toolchains/leanprover--lean4---v4.7.0/bin/leanc -c -o ./.lake/packages/mathlib/.lake/build/ir/Cache/Requests.c.o ./.lake/packages/mathlib/.lake/build/ir/Cache/Requests.c -O3 -DNDEBUG
error: stderr:
/home/rj/.elan/toolchains/leanprover--lean4---v4.7.0/bin/leanc: line 2: /home/rj/.elan/toolchains/leanprover--lean4---v4.7.tmp/bin/leanc.orig: No such file or directory
error: external command `/home/rj/.elan/toolchains/leanprover--lean4---v4.7.0/bin/leanc` exited with code 127
info: [5/9] Compiling Cache.Main
error: > /home/rj/.elan/toolchains/leanprover--lean4---v4.7.0/bin/leanc -c -o ./.lake/packages/mathlib/.lake/build/ir/Cache/Main.c.o ./.lake/packages/mathlib/.lake/build/ir/Cache/Main.c -O3 -DNDEBUG
error: stderr:
/home/rj/.elan/toolchains/leanprover--lean4---v4.7.0/bin/leanc: line 2: /home/rj/.elan/toolchains/leanprover--lean4---v4.7.tmp/bin/leanc.orig: No such file or directory
error: external command `/home/rj/.elan/toolchains/leanprover--lean4---v4.7.0/bin/leanc` exited with code 127
error: mathlib: failed to fetch cache

Versions

lean --version is Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release)

OS version is Pop!_OS 22.04 LTS

Additional Information

(No additional information)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[Kha]

I think this is NixOS/nixpkgs#294514?

[rj00a]

I think this is NixOS/nixpkgs#294514?

Thanks, that seems to be the answer. My nixpkgs was a bit outdated.