compilation error on master?

Stream: mathlib4

[Kevin Buzzard]

Right now on master, this commit

commit 258b485d4252a0cb5049ee25e87107830f13b7d1 (HEAD -> master, upstream/update-dependencies-bot-use-only, upstream/master, upstream/HEAD)
Author: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date:   Tue Oct 21 18:15:21 2025 +1100

    chore: merge bump/v4.25.0 (#30740)

I tried rm -rf .lake and then lake exe cache get and then lake build and I'm getting

buzzard@IC-HWDXTW69VR Mathlib % lake build
✖ [28/478] Replaying ImportGraph.RequiredModules
error: no such file or directory (error code: 2)
  file: /Users/buzzard/Lean/Projects/Mathlib/.lake/packages/importGraph/.lake/build/lib/lean/ImportGraph/RequiredModules.ir
✖ [56/478] Replaying Qq.Macro
error: no such file or directory (error code: 2)
  file: /Users/buzzard/Lean/Projects/Mathlib/.lake/packages/Qq/.lake/build/lib/lean/Qq/Macro.ir
✖ [426/1574] Replaying Plausible.Arbitrary
error: no such file or directory (error code: 2)
  file: /Users/buzzard/Lean/Projects/Mathlib/.lake/packages/plausible/.lake/build/lib/lean/Plausible/Arbitrary.ir
✖ [435/1574] Replaying LeanSearchClient.Basic
error: no such file or directory (error code: 2)
  file: /Users/buzzard/Lean/Projects/Mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean/LeanSearchClient/Basic.ir
Some required targets logged failures:
- ImportGraph.RequiredModules
- Qq.Macro
- Plausible.Arbitrary
- LeanSearchClient.Basic
error: build failed
buzzard@IC-HWDXTW69VR Mathlib %

Can anyone else reproduce?

[Markus Himmel]

This also seems to be the reason for all of the failures in #rss > mathlib bors notifications so mathlib is standing still right now. We might have to revert the bump to 4.25.0 until we understand what's going wrong here. cc @Kim Morrison

[Christian Krause]

Hi there,
I just pushed a small commit to #30130 but CI failed (after an hour). But strangely, there were no build errors. It just said that it wasn't able to "verify that everything is available in the cache".
image.png
To me, this seems like somethings that could be fixed by just rerunning CI, but I can't find the button that does this... (Does a normal user even have the permission to do this?).

[Robin Carlier]

Note that if you skip the lake exe cache get step it seems to build just fine.

[Markus Himmel]

Yes, there were some significant changes to the cache as part of the 4.25.0 bump

[Robin Carlier]

Probably related to #mathlib4 > compilation error on master?

[Christian Krause]

Ohh, yes, probably, I did not see the topic before writing this

[Bryan Gin-ge Chen]

I've put #30747 (reverting the bump) on the queue with high priority. If it fails to go through we may have to merge manually.

[Kim Morrison]

Thanks all, just back at my computer now and taking a look.

[Kim Morrison]

I'm pretty sure I see what has happened.

Current (broken) master is 258b485d4252, while the (successful) commit on nightly-testing that was the culmination of getting everything ready for v4.25.0-rc1 was 1b84b44509b73ac56eccb48879e3956a6d0b4b03.

The diff between these is

diff --git a/Cache/IO.lean b/Cache/IO.lean
index 82c2d7e1682..1438cc079f3 100644
--- a/Cache/IO.lean
+++ b/Cache/IO.lean
@@ -90,7 +90,7 @@ def getLeanTar : IO String := do
 /-- Bump this number to invalidate the cache, in case the existing hashing inputs are insufficient.
 It is not a global counter, and can be reset to 0 as long as the lean githash or lake manifest has
 changed since the last time this counter was touched. -/
-def rootHashGeneration : UInt64 := 3
+def rootHashGeneration : UInt64 := 1

 /--
 `CacheM` stores the following information:
@@ -321,10 +321,10 @@ def mkBuildPaths (mod : Name) : CacheM <| List (FilePath × Bool) := do
     (packageDir / LIBDIR / path.withExtension "olean.private.hash", false),
     (packageDir / LIBDIR / path.withExtension "ilean", true),
     (packageDir / LIBDIR / path.withExtension "ilean.hash", true),
-    (packageDir / LIBDIR / path.withExtension "ir", false),
-    (packageDir / LIBDIR / path.withExtension "ir.hash", false),
     (packageDir / IRDIR  / path.withExtension "c", true),
     (packageDir / IRDIR  / path.withExtension "c.hash", true),
+    -- (packageDir / LIBDIR / path.withExtension "ir", true),
+    -- (packageDir / LIBDIR / path.withExtension "ir.hash", true),
     (packageDir / LIBDIR / path.withExtension "extra", false)]

 /-- Check that all required build files exist. -/

[Kim Morrison]

I'm not quite sure how I managed to get that into the PR I squash merged into master... :-(

[Kim Morrison]

But it would explain neatly the observed failure.

[Kim Morrison]

So I propose pulling #30747 off, and just applying that diff to master.

[Kim Morrison]

#30748

[Kim Morrison]

Sad, that is failing. :-(

[Kim Morrison]

Not my day.

[Kim Morrison]

Putting #30747 back on the queue ...

[Markus Himmel]

Try bumping rootHashGeneration as part of #30748 to get rid of the bad cache?

[Kim Morrison]

#30748 was already doing that!

[Kim Morrison]

AH.

[Kim Morrison]

The problem is that we are using the old cache in CI.

[Kim Morrison]

So I think we actually just have to be brave and trust that #30748 is actually right, and merge it without CI.

[Kim Morrison]

Lovely.

[Kim Morrison]

(This is a consequence of our new security procedures not allowing changes to cache in the same PR!)

[Kim Morrison]

#30748 should make master identical to a commit on nightly-testing that succeeded...

[Kim Morrison]

So I think I'm going to go for it. :-)

[Kim Morrison]

We'll then know approximately ~45 minutes later, as CI will run on the push to master, with the new cache.

[Kim Morrison]

We really need to work out a workflow here so that a maintainer can override the restriction about not using cache from the PR...

[Kim Morrison]

Okay, https://github.com/leanprover-community/mathlib4/actions/runs/18681884710/job/53264697924 is the workflow run on for the new attempt at master.

[Kim Morrison]

:popcorn:

[Robin Carlier]

And now lake exe cache get; lake build works! :tada:

[Kevin Buzzard]

Thank you all!

[Michael Rothgang]

Same here!

[Michael Rothgang]

I find it odd that lake build now takes 11 seconds for the "computing jobs" step, even if to do nothing. (It used to be faster, my computer uses Linux and is quite good.) But this is clearly not an error about the cache.

[Kim Morrison]

Is it actually single-threaded during those 11 seconds?

[Kevin Buzzard]

Oh I've been having this problem on my new Mac laptop, it drives me nuts! Edit: actually the thing which drives me nuts is the 10 second pause before "computing jobs" even appears.

[Michael Rothgang]

In my system tray (GNOME on Debian trixie), I see all CPUs are (close to) 100% utilisation for that time. Apparently, I have 20 of them. (Not sure if that's physical or logical cores; you get the idea.) That means "no, not single-threaded", right?

[Michael Rothgang]

(deleted)

[Michael Rothgang]

The output of time lake build (on 3218e4a7b146eea135d23dbeccdf73f7a1921a32 a.k.a. current head, after getting cache) confirms this: 182s of user time.

Full output

$ time lake build
⡿ [2559/2647] Running Mathlib.CategoryTheory.Bicategory.LocallyDiscrete (+ 17 mo⣾ [2919/3096] Running Mathlib.CategoryTheory.Preadditive.Projective.Preserves (+⣷ [3015/3157] Running Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (+ ⣽ [3509/4651] Running Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic ⣾ [4099/5127] Running Mathlib.CategoryTheory.Preadditive.Yoneda.Projective (+ 19⣯ [4242/5214] Running Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty⣻ [4496/5448] Running Mathlib.CategoryTheory.Localization.LocallySmall (+ 17 mor⣽ [4550/5497] Running Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts (+ 20 ⣯ [5552/6621] Running Mathlib.Topology.Algebra.Constructions.DomMulAct (+ 19 mor⣟ [5601/6667] Running Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue (⡿ [5653/6728] Running Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (+ 19 more⢿ [5709/6771] Running Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion (+ 18⣾ [5855/6919] Running Mathlib.Probability.ProbabilityMassFunction.Basic (+ 19 mo⣟ [5990/7085] Running Mathlib.RingTheory.LocalRing.ResidueField.Fiber (+ 19 more⣻ [6453/7248] Running Mathlib.Topology.Maps.Proper.CompactlyGenerated (+ 19 more⣾ [6737/7336] Running Mathlib.Topology.Separation.LinearUpperLowerSetTopology (+⣯ [6852/7389] Running Mathlib.Topology.MetricSpace.HausdorffDimension (+ 20 more⣯ [7180/7396] Running Mathlib.Probability.Process.PartitionFiltration (+ 17 more⣟ [7214/7396] Running Mathlib.Probability.Process.PartitionFiltration (+ 18 more⡿ [7257/7396] Running Mathlib.Probability.Moments.CovarianceBilinDual (+ 18 more⣻ [7321/7396] Running Mathlib.Probability.Moments.CovarianceBilinDual (+ 10 moreBuild completed successfully (7396 jobs).

real 0m17,836s
user 3m2,266s
sys 0m2,300s

[Michael Rothgang]

I have Intel i7-12700H CPUs, i.e. not "ancient and slow".

[joseph hua]

I came across the same issue with my PR that I started before the update. Merging the most recent version of the master branch seems to have fixed it. I don't really understand the discussion here, but as a tl;dr for folks like me - is merging to a newer version of master the right thing to do?

[Kenny Lau]

joseph hua said:

is merging to a newer version of master the right thing to do?

the usual right thing to do is to go to zulip and see if someone else already reported it (90% of the case the answer will be yes) and then follow that thread until Kim figures out how to fix the problem and then celebrate by merging mathlib master