Build error in Tactic file

Stream: mathlib4

[Christian Krause]

Hi again,
I am having issues with my PR #30130 where I just changed some normal mathlib files, but CI complains about missing definitions in tactic files. I tried merging master, but it didn't help. I am out of my depth here, so I'd appreaciate someone looking at it to show me what went wrong.
(I would have posted this in my thread from yesterday but I can't find it).

[Kevin Buzzard]

The error is

error: Mathlib/Tactic/ReduceModChar.lean:74:14: failed to compile definition, compiler IR check failed at normIntNumeral'. Error: depends on declaration 'Tactic.ReduceModChar.normBareNumeral', which has no executable code; consider marking definition as 'noncomputable'

[Damiano Testa]

I can reproduce the error locally.

[Damiano Testa]

I suspect that the tactic file imports the files with your changes and something there is affecting the tactic.

[Damiano Testa]

ReduceModChar I think uses smul. I wonder if your new smul instances is confusing the tactic.

[Christian Krause]

Ohh ok, I suppose it has something to do with the changes in Mathlib/GroupTheory/GroupAction/Defs.lena. I'll try to find out what is going on.

[Damiano Testa]

I am not sure, actually, since even reverting these changes does not seem to fix the error, at least locally.

[Christian Krause]

Ok, but Mathlib/GroupTheory/FreeGroup/Orbit.lean is just importet in Mathlib.lean, Mathlib/RingTheory/Kaehler/TensorProduct.lean is just changing a proof and Mathlib/Dynamics/Flow.lean is surely not relevant...?

[Damiano Testa]

I agree that if the files are not imported by the tactic one, they should not affect it. I am not really understanding what is going on.

[Christian Krause]

I tried replacing the beta i introduced with a new variable gamma in Action/Defs.lean (because beta is used later in the file and maybe this is something about explicit vs implicit arguments). Otherwise I have no idea... (I just realized that this should not fix the error because reverting all the changes doesn't fix it...)

[Damiano Testa]

I don't know enough about Qq to know what it might be synthesizing and where it might get stuck. I'll ping @Anne Baanen, as the author of the ReduceModChar tactic!

[Yaël Dillies]

This also happens in bors right now: https://github.com/leanprover-community/mathlib4/actions/runs/18710984072/job/53359169237

[Yaël Dillies]

and it also happened to @Stefan Kebekus in #30630, but he closed the PR and reopened a new one instead of reporting :sad:

[Yaël Dillies]

(nothing against you, Stefan, but in the face of an error you don't understand, the primary instinct should be to go complain on Zulip, not shuffle things around across PRs)

[Sebastian Ullrich]

So random PRs appear to be affected but not master?

[Sebastian Ullrich]

Might be a cache bug around the new .ir files

[Damiano Testa]

It looks like bors is unable to merge anything, since it runs into this issue.

[Sebastian Ullrich]

It would be great if someone could confirm building from scratch fixes things - just has to be up to a broken file

[Damiano Testa]

I also just confirmed that the cache on master works.

[Damiano Testa]

In the context of the PR above, I did a rebuild by reverting to master a file upstream of where the error was, running lake build and still getting errors.

[Damiano Testa]

I did not however build from scratch.

[Yong-Gyu Choi]

I'm having a similar issue with my PR #29960 with error message

error: Mathlib/MeasureTheory/Integral/Bochner/Basic.lean:1442:2:
(interpreter) unknown declaration 'Mathlib.Meta.Positivity.evalIntegral'

Locally in the master branch with lake exe cache get, adding anything to Mathlib.LinearAlgebra.TensorProduct.Tower gives me the same error if I do lake build Mathlib.MeasureTheory.Integral.Bochner.Basic.

[Damiano Testa]

I did the rebuild:

• I checked out the PR above,
• removed the .lake dir and
• built the tactic file.

Now there are no errors.

[Sebastian Ullrich]

Thanks! So we should likely revert the cache changes as well as all package bumps related to it for now

[Bryan Gin-ge Chen]

Which changes are these exactly? Is it #30772?

[Sebastian Ullrich]

I believe so. Reverting the toolchain should be optional but it doesn't hurt.

[Sebastian Ullrich]

This does not include the changes to cache but that too should be okay as long as no dependencies make use of the module system

[Bryan Gin-ge Chen]

Thanks, I've opened #30785.

[Sebastian Ullrich]

Thanks!

[Bryan Gin-ge Chen]

I've put it on the queue after the currently running batch. If anyone objects, I can take it off again.

[Bryan Gin-ge Chen]

Unfortunately the builds are still failing: https://github.com/leanprover-community/mathlib4/actions/runs/18716744507/job/53377985563

Do we need to go back further?

[Bryan Gin-ge Chen]

Should we revert #30740 and #30748 perhaps?

[Sebastian Ullrich]

It might be, I only just learned that the rc1 bump already included some modulized packages. I'm taking a look at the specific failure right now but that doesn't have to delay reverting.

[Bryan Gin-ge Chen]

OK, I've put #30788 on the queue.

[Sebastian Ullrich]

@Mario Carneiro The root issue seems to be that all .olean.server/private files fetched from the cache are (almost) empty

$ ls -lh .lake/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.*
-rw-rw-r-- 1 sebastian sebastian  28K Oct 22 15:11 .lake/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.ilean
-rw-rw-r-- 1 sebastian sebastian   16 Oct 22 15:11 .lake/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.ilean.hash
-rw-rw-r-- 1 sebastian sebastian 639K Oct 22 15:11 .lake/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.ir
-rw-rw-r-- 1 sebastian sebastian   16 Oct 22 15:11 .lake/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.ir.hash
-rw-rw-r-- 1 sebastian sebastian  25K Oct 22 15:11 .lake/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.olean
-rw-rw-r-- 1 sebastian sebastian   16 Oct 22 15:11 .lake/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.olean.hash
-rw-rw-r-- 1 sebastian sebastian   96 Oct 22 15:11 .lake/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.olean.private
-rw-rw-r-- 1 sebastian sebastian   16 Oct 22 15:11 .lake/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.olean.private.hash
-rw-rw-r-- 1 sebastian sebastian   96 Oct 22 15:11 .lake/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.olean.server
-rw-rw-r-- 1 sebastian sebastian   16 Oct 22 15:11 .lake/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.olean.server.hash
-rw-rw-r-- 1 sebastian sebastian  247 Oct 22 15:11 .lake/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.trace
$ ls -lh .lake2/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.*
-rw-rw-r-- 1 sebastian sebastian  28K Oct 22 15:12 .lake2/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.ilean
-rw-rw-r-- 1 sebastian sebastian   16 Oct 22 15:12 .lake2/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.ilean.hash
-rw-rw-r-- 1 sebastian sebastian 639K Oct 22 15:12 .lake2/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.ir
-rw-rw-r-- 1 sebastian sebastian   16 Oct 22 15:12 .lake2/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.ir.hash
-rw-rw-r-- 1 sebastian sebastian  25K Oct 22 15:12 .lake2/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.olean
-rw-rw-r-- 1 sebastian sebastian   16 Oct 22 15:12 .lake2/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.olean.hash
-rw-rw-r-- 1 sebastian sebastian 1.2M Oct 22 15:12 .lake2/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.olean.private
-rw-rw-r-- 1 sebastian sebastian   16 Oct 22 15:12 .lake2/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.olean.private.hash
-rw-rw-r-- 1 sebastian sebastian 8.0K Oct 22 15:12 .lake2/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.olean.server
-rw-rw-r-- 1 sebastian sebastian   16 Oct 22 15:12 .lake2/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.olean.server.hash
-rw-rw-r-- 1 sebastian sebastian 2.7K Oct 22 15:12 .lake2/packages/plausible/.lake/build/lib/lean/Plausible/DeriveArbitrary.trace

Second directory is from a local build

[Bryan Gin-ge Chen]

What's the right way of making the build depend on a new version of a bad cache file? I've hit this error twice now:

https://github.com/leanprover-community/mathlib4/actions/runs/18720505499/job/53397344367#step:8:19

After downloading the cache, in the step checking that lake build --no-build works:

✖ [2/755] Building Mathlib.Tactic.Linter.Header
error: target is out-of-date and needs to be rebuilt

The first time I tried to fix it by adding some whitespace to the aforementioned file, but I guess that wasn't enough?

[Bryan Gin-ge Chen]

Ah, I guess I added the whitespace to the module doc. Maybe adding it to a docstring would have worked.

[Sebastian Ullrich]

Hmm, I'm surprised this happens even with the revert

[Bryan Gin-ge Chen]

Ran into the same error again: https://github.com/leanprover-community/mathlib4/actions/runs/18723044360/job/53404947721?pr=30788#step:8:19

Not sure what to do at this point -- I could merge this manually, but I'm afraid of leaving master on a state with a broken cache file.

[Bryan Gin-ge Chen]

I guess the big mystery to me is why nothing is still being uploaded in the cache upload steps -- they all seem to be rejected because they are already present. Have I still not managed to tweak the code enough to generate new oleans?

[Bryan Gin-ge Chen]

Ah, maybe the issue is that the changes to Cache on master make it impossible to properly verify the build from the PR branch? I guess the PRs I'm trying to revert were both merged into master without going through bors as well.

[Bryan Gin-ge Chen]

I'll revert the whitespace changes I made and then merge #30788 manually -- feel free to tell me this is a bad idea!

[Bryan Gin-ge Chen]

Done. master is building now, if the cache is still broken here then I'm really out of ideas.

[Emily Riehl]

Someone advised me NOT to merge this into downstream projects yet due to some bug with continuous integration. See eg this PR which didn't generate any checks. Or should I not worry about this and merge anyway?

[Bryan Gin-ge Chen]

There were some issues with the mathlib cache with v4.25.0-rc2 so I have moved mathlib back to v4.24.0; I would recommend also holding off on upgrading to v4.25.0-rc2 until at least after Kim gets back online to advise.

(I think the fact that the auto-generated PR didn't generate any checks is probably unrelated to the version bump. #announce is probably not the place to discuss it though.)

[Notification Bot]

2 messages were moved here from #announce > releases of new Lean versions by Riccardo Brasca.

[Riccardo Brasca]

This is the right topic, isn't it?

[Bryan Gin-ge Chen]

@Riccardo Brasca I think those messages were fine in the announce topic -- it's probably a good idea to let people know there are currently some issues with mathlib's cache and v4.25.0-rc2. I just meant I didn't want to get into a discussion about the CI in that thread.

[Riccardo Brasca]

I didn't think about that, would you mind write some sort of "official" message in the announce topic? It seems more appropriate that Emily's question.

[Bryan Gin-ge Chen]

Unfortunately it looks like the build on master failed with the same cache error: https://github.com/leanprover-community/mathlib4/actions/runs/18723067296/job/53405707259

I'll hold off from making any more changes until Kim or Sebastian are back.

edit: just checked again and master is actually green. I was looking at the wrong tab above, whoops!

[Emily Riehl]

Thanks for moving the message. I never know which channel to use. Is there a users guide somewhere ;)?

[Riccardo Brasca]

We are somehow strict only with #announce , that we try to keep as small as possible (literally just the announcement, without any discussion). Anyway no worries!

[Riccardo Brasca]

Often there is a discussion topic for anything being announced.

[Kenny Lau]

Is it fixed now? I see some PR's merging master

[Bryan Gin-ge Chen]

I hope so, but I'm a bit hesitant to declare victory until someone can explain what exactly went wrong.

[Sebastian Ullrich]

I think troubles with merging the fix are likely from the split cache executable setup in CI that makes it depend on the state of both the PR and master, though I can't completely explain it either

[Kim Morrison]

Okay, just arriving here after a good night's sleep. :-)

Here's I think the plan:

• :check: I'm going to delete the existing v4.25.0-rc1 and v4.25.0-rc2 tags from Mathlib/repl/Cslib now.
• :check: We make sure the announcement thread has a warning that people shouldn't be bumping their Mathlib dependencies past v4.24.0 for now.
• [ ] #30805 In the Mathlib CI step, when we verify that the cache works, we should change lake build --no-build to lake build --no-build --rehash. This would have detected the underlying problem, and alerted us to the bug in leantar.
• [ ] We need to fix the problem in leantar (it produces the wrong .olean.server and .olean.private files).
• [ ] We can then re-merge #30740, #30748, #30772 (i.e. revert the revert PRs #30785 and #30788), but remembering to update to the new version of leantar. Probably as with these PRs, we are going to have to squash merge by hand, as CI will still be confused by the change in behaviour in cache contained in the PR.
• [ ] We then just re-tag Mathlib with v4.25.0-rc2 (perhaps waiting until one more PR successfully lands?).
• [ ] We run lake update in repl and Cslib and retag those.
• [ ] We update the announcement thread.

[Chris Henson]

One piece of confusion today has been PRs from branches with a toolchain differing from Mathlib. Could we check for this in a pull request workflow and suggest to merge master? Today is an exceptional situation in having a toolchain reversion, but this seems more generally relevant for older PRs too.

[Kim Morrison]

In the past we've decided this was too much churn, and given that most PRs merge just fine even across toolchain changes, this wasn't worth it.

[Kim Morrison]

But on days like today, it would be nice to be more conservative!

[Chris Henson]

I figured it had been discussed, and I agree that it is relatively uncommon. I think it could be minimally invasive if it is just a comment on the PR along the lines of "If this PR is potentially toolchain sensitive (grind, simp, etc.) consider merging master". If the consensus changes, feel free to ping me to add this.

[Bryan Gin-ge Chen]

@Chris Henson Ah, I didn't realize you were worried about the toolchain difference when you merged master into #30803. Sorry if my message came off as condescending. Let me take your PR off the queue again and delegate.

[Kim Morrison]

I've reproduced the leangz problem in the leangz repository itself, and added a (failing) cargo test test case: https://github.com/digama0/leangz/pull/4

[Chris Henson]

@Bryan Gin-ge Chen No worries. It should be fine I think now, you can leave it on.

[Kim Morrison]

Okay, Claude says it understands the problem in leangz

[Kim Morrison]

@Mario Carneiro, I just put up https://github.com/digama0/leangz/pull/5, with Claude's fix.

[Kim Morrison]

I don't understand, but it's a two line change so hopefully you can say whether it is nonsense or not.

[Kim Morrison]

If it is nonsense, hopefully https://github.com/digama0/leangz/pull/4 is still useful as a test case!

[Mario Carneiro]

Can you point me to a bug case?

[Kim Morrison]

#mathlib4 > Build error in Tactic file @ 💬

[Kim Morrison]

and https://github.com/digama0/leangz/pull/4 contains 3 explicit oleans which don't roundtrip.

[Mario Carneiro]

Is this on mathlib master?

[Kim Morrison]

It was on master but has been reverted.

[Kim Morrison]

SHA incoming

[Kim Morrison]

52404eb9d41e2d814169199b4930ff4279847223

[Mario Carneiro]

(I wanted to test leangz on mathlib first before releasing it on master, and finally release a non -pre release)

[Kim Morrison]

i.e. if you git checkout 52404eb9d41e2d814169199b4930ff4279847223 and lake exe cache get you should see truncated .olean.server and .olean.private files

[Kim Morrison]

Mario Carneiro said:

(I wanted to test leangz on mathlib first before releasing it on master, and finally release a non -pre release)

Sorry about moving too quickly, I should have asked you about the "pre" status.

[Mario Carneiro]

there is a selftest feature in leangz which is not yet module-aware, that will do a roundtrip of every file in mathlib

[Mario Carneiro]

but I couldn't test it at the time because there weren't any interesting files to test

[Mario Carneiro]

IIUC even now there aren't that many module files

[Kim Morrison]

There are no module files in Mathlib itself, but on that 52404 commit above, all the dependencies are module files.

[Mario Carneiro]

the added leangz test infrastructure is much appreciated

[Mario Carneiro]

@Kim Morrison: added self-test and ran it on all of the oleans in 52404eb, and released v0.1.16-pre4

[Bryan Gin-ge Chen]

I've opened #30807 which reverts #30785 and #30788. Going to sign off for the night soon, so feel free to push the leantar updates, etc. to it and merge while I'm gone.

[Kim Morrison]

I've updated #30807 to use v0.1.16-pre4

[Kim Morrison]

@Mario Carneiro, we're failing in CI while trying to upload the cache, with:

uncaught exception: failure in /home/lean/.cache/mathlib/leantar-0.1.15 #
[/home/lean/.cache/mathlib/1829cd72ae91ee2a.ltar, ./.lake/build/lib/lean/Mathlib.trace, -c,
git=mathlib4@3976ee441f89218bfb5d49b29dcb0e328e4b2076, ./.lake/build/lib/lean/Mathlib.olean,
./.lake/build/lib/lean/Mathlib.olean.hash, ./.lake/build/lib/lean/Mathlib.ilean,
./.lake/build/lib/lean/Mathlib.ilean.hash, ./.lake/build/ir/Mathlib.c, ./.lake/build/ir/Mathlib.c.hash]:

thread 'main' panicked at /project/src/ltar.rs:275:24:
bad .trace file

[Sebastian Ullrich]

@Kim Morrison That's master leantar, right? I'd suggest force-merging the leantar update first, then the actual bump should be able to pass regular CI

[Kim Morrison]

Done.

[Kim Morrison]

and trying again on #30807.

[Kim Morrison]

I've merged, let's see what happens on master this time.

[Kim Morrison]

(cache will be unavailable on master for about 40 minutes)

[Kim Morrison]

back from climbing, everything seems to have merged, and nothing is on fire!