Building Mathlib.NumberTheory.Multiplicity failed

Stream: mathlib4

[Tristan Stérin]

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)

I have an issue about this on the formal conjecture project

[Tristan Stérin]

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

[Yaël Dillies]

Tristan Stérin said:

I've had to build mathlib for the formal conjecture project

:scream: You should never have to build mathlib. Do you know about lake exe cache get?

[Tristan Stérin]

I think I ran the command, as instructed in the formal conjecture project:

lake exe cache get
lake build

But I may have ran it in another terminal session, would that matter?

[Yaël Dillies]

Doesn't matter what terminal session you ran it in so long as you ran it in the correct folder. If you did run it in the correct folder, then I would advise you give us more precise indications of what exactly you did, so as to debug

[Tristan Stérin]

OK, I think I did ran it in the correct folder, but I'm not 100% sure now, and the only thing I had done was lake build as well as opening vscode and clicking "Restart File" which launched a long, seemingly looping for ever, yellow spinning wheel.

[Yaël Dillies]

Did you run lake build and/or clicked "Restart File" after lake exe cache get was done running, or while it was running?

[Tristan Stérin]

Unfortunately, I don't remember :( sorry!