`NumberTheory.Multiplicity` and `NumberTheory.Transcendental.Liouville.Residual` build fail

[tcosmo]

Hello, I've had to build mathlib for the formal conjecture project, however it fails building Mathlib.NumberTheory.Multiplicity and Mathlib.NumberTheory.Transcendental.Liouville.Residual:

✖ [5867/6489] Building Mathlib.NumberTheory.Multiplicity
trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/packages/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH= /Users/cosmo/.elan/toolchains/leanprover--lean4---v4.17.0/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -DmaxSynthPendingDepth=3 -Dweak.linter.docPrime=false -Dweak.linter.hashCommand=true -Dweak.linter.oldObtain=true -Dweak.linter.refine=true -Dweak.linter.style.cdot=true -Dweak.linter.style.dollarSyntax=true -Dweak.linter.style.header=true -Dweak.linter.style.lambdaSyntax=true -Dweak.linter.style.longLine=true -Dweak.linter.style.longFile=1500 -Dweak.linter.style.missingEnd=true -Dweak.linter.style.multiGoal=true -Dweak.linter.style.setOption=true ././.lake/packages/mathlib/././Mathlib/NumberTheory/Multiplicity.lean -R ././.lake/packages/mathlib/./. -o ././.lake/packages/mathlib/.lake/build/lib/Mathlib/NumberTheory/Multiplicity.olean -i ././.lake/packages/mathlib/.lake/build/lib/Mathlib/NumberTheory/Multiplicity.ilean -c ././.lake/packages/mathlib/.lake/build/ir/Mathlib/NumberTheory/Multiplicity.c --json
info: stderr:
failed to write '././.lake/packages/mathlib/.lake/build/lib/Mathlib/NumberTheory/Multiplicity.olean': 2 No such file or directory
error: Lean exited with code 1
✖ [5913/6489] Building Mathlib.NumberTheory.Transcendental.Liouville.Residual
trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/packages/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH= /Users/cosmo/.elan/toolchains/leanprover--lean4---v4.17.0/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -DmaxSynthPendingDepth=3 -Dweak.linter.docPrime=false -Dweak.linter.hashCommand=true -Dweak.linter.oldObtain=true -Dweak.linter.refine=true -Dweak.linter.style.cdot=true -Dweak.linter.style.dollarSyntax=true -Dweak.linter.style.header=true -Dweak.linter.style.lambdaSyntax=true -Dweak.linter.style.longLine=true -Dweak.linter.style.longFile=1500 -Dweak.linter.style.missingEnd=true -Dweak.linter.style.multiGoal=true -Dweak.linter.style.setOption=true ././.lake/packages/mathlib/././Mathlib/NumberTheory/Transcendental/Liouville/Residual.lean -R ././.lake/packages/mathlib/./. -o ././.lake/packages/mathlib/.lake/build/lib/Mathlib/NumberTheory/Transcendental/Liouville/Residual.olean -i ././.lake/packages/mathlib/.lake/build/lib/Mathlib/NumberTheory/Transcendental/Liouville/Residual.ilean -c ././.lake/packages/mathlib/.lake/build/ir/Mathlib/NumberTheory/Transcendental/Liouville/Residual.c --json
info: stderr:
failed to write '././.lake/packages/mathlib/.lake/build/lib/Mathlib/NumberTheory/Transcendental/Liouville/Residual.olean': 2 No such file or directory
error: Lean exited with code 1
Some required builds logged failures:
- Mathlib.NumberTheory.Multiplicity
- Mathlib.NumberTheory.Transcendental.Liouville.Residual
error: build failed

My configuration is:

macos 14.2.1
vscode 1.101.0
Lake version 5.0.0-306f361 (Lean version 4.17.0)

And I just ran:

lake exe cache get
lake build

At the root of a fresh clone of https://github.com/google-deepmind/formal-conjectures (I have an issue opened there)

[tcosmo]

It eventually worked by re-running lake build, I don't know why the first build failed.