lean4checker failure

Stream: nightly-testing

[github mathlib4 bot]

:cross_mark: lean4checker failed on b40a06417b06ce02e2cc5f687bb8649ff3d5a42d (branch: nightly-testing-2025-05-01)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 01239f4904a7e86e772ed7cf0e5712134f840718 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 01239f4904a7e86e772ed7cf0e5712134f840718 (branch: nightly-testing-2025-05-02)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 22711cf78da3e4cfdb8a28cce9073f0986ca11dd (branch: nightly-testing-2025-05-03)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 22711cf78da3e4cfdb8a28cce9073f0986ca11dd (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 03bc870a1a65cfea41eecb05a8599288a601629b (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 03bc870a1a65cfea41eecb05a8599288a601629b (branch: nightly-testing-2025-05-03)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 85654a32f979407573b2ec9f682485619970a242 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 85654a32f979407573b2ec9f682485619970a242 (branch: nightly-testing-2025-05-05)

[Ruben Van de Velde]

@Kim Morrison have you looked at what's going wrong?

[Kim Morrison]

This was fixed by rc3 a few hours ago. :fingers_crossed:

[Kim Morrison]

At least, we fixed a bug...

[github mathlib4 bot]

:cross_mark: lean4checker failed on 554d794c8dbf32758e9a66527c898fe904933c56 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on a14c28b31a1787f81fa59756cded637bae0be55a (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on c2eae28089486ed39cfecee5475e2293d28b08f0 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 3008304e7959628b0759667dd5321149ae9b8100 (branch: master)

[Kevin Buzzard]

Error is

Run git clone https://github.com/leanprover/lean4checker
Cloning into 'lean4checker'...
leanprover/lean4:v4.20.0-rc5
error: pathspec 'v4.20.0-rc5' did not match any file(s) known to git
Error: Process completed with exit code 1.

[github mathlib4 bot]

:cross_mark: lean4checker failed on a55bbf799c39feddc50a2a4d2464234ac89fea05 (branch: master)

[Kevin Buzzard]

(same error)

[Mario Carneiro]

I feel like the rate of lean4checker failures has gone way up of late. Maybe we should go back to testing it in CI - the original argument for moving it to a nightly thing was on the assumption that it would usually be green

[Mario Carneiro]

in particular, it should be tested as part of the nightly -> master bump

[github mathlib4 bot]

:cross_mark: lean4checker failed on b16b8f3a78e46e7f35fd5b4a866742284af9aef3 (branch: master)

[Kim Morrison]

The problem is not with frequent breakages, but persistent lack of anyone fixing it. :-)

[Mario Carneiro]

I'm hoping that putting it on the critical path will stop people from putting it off

[Johan Commelin]

Can someone explain what kind of fixes we need here? Changes to lean4checker itself? Who are the people that can do that?

[Mario Carneiro]

I think most of the issues are trivial build failures? Like a function got renamed or such

[Johan Commelin]

And if we put this on the critical path, who becomes responsible for fixing this?

[Mario Carneiro]

probably Kim, unless they ping someone else to handle it

[Mario Carneiro]

it would presumably show up in nightly-testing along with all of the other things that can go wrong

[Johan Commelin]

I'm hesitant to put this in the nightly-testing workflow with its current failure rate.

[Mario Carneiro]

it's only breaking so much because people are "allowed" to ignore it

[Mario Carneiro]

but I think that's wrong, we should not be shipping broken lean4checker any more than we should be shipping a broken quote4 or importGraph package

[Mario Carneiro]

it only acquired this unique status because we didn't want every PR to have to run lean4checker because it is somewhat expensive to run and doesn't yield value most of the time

[Mario Carneiro]

but I don't think that extends to not checking if it even builds

[Kim Morrison]

Every PR checks that lean4checker builds, or at least that is what is claimed in the yml!

[Kim Morrison]

If that's not true I'll fix it urgently.

[Kim Morrison]

An excellent solution would be to refactor CI so both linting and lean4checker (and nanoda and lean4lean) all run in parallel in a follow-up job to the main build.

[Kim Morrison]

If they are in parallel there is no time cost to the contributor, I think; is roughly the speed of linting.

[Kim Morrison]

As an alternative, we could enable it in all nightly-testing and lean-pr-testing branches.

[Kim Morrison]

I'd be happy with either of those options, and they would force me to fix problems. But while I'm feeling desperately behind on grind it's very tempting to not make these changes myself, so it stays somebody-else's-problem... That is, CI changing PRs welcome. :-)

[Damiano Testa]

I've wanted to move the final lint check to a contingent workflow for a while, but have always been worried about making the untestable leap of adding workflow dependencies.

[Damiano Testa]

How about we start with a dependent workflow that runs after the cache has been uploaded and simply retrieves the cache?

[Damiano Testa]

Once that works, migrating the rest should be straightforward, as all CI changes appear to be.

[Damiano Testa]

The main issue is that the contingent setup only runs once it is in master, so there is virtually no testing it.

[Kim Morrison]

I think this would be a good idea, but we are also actively trying to overhaul all of CI to improve security. I would really like to get that change in first (by end of June!), so anyone with available time to make major changes to CI is very much invited to help with that, first. There are a number of open issues there. (If you don't know what I'm talking about because you're a reviewer but not on the maintainers+FRO list, and would like to help on this project, please just ask me!)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 4459088658417ad4ec82b194da3184cbe638b7e0 (branch: nightly-testing-2025-05-29)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 644a2302b0210c65cac2ba7497eba7f90a3cb803 (branch: nightly-testing-2025-05-29)

[github mathlib4 bot]

:cross_mark: lean4checker failed on ac7d8cf03db685fb9230d273bbe09ace3cc370df (branch: nightly-testing-2025-05-29)

[Kim Morrison]

Just some typeclass changes that show up in the expected error output. Fixed on lean4checker's nightly-testing.

[github mathlib4 bot]

:cross_mark: lean4checker failed on 853aa9e9be1affcd90daad6d3a9e05fcb739885c (branch: nightly-testing-2025-06-09)

[github mathlib4 bot]

:cross_mark: lean4checker failed on d596d8c5bbf4a4a56c9d8f2214d1905e0a1b2c30 (branch: nightly-testing-2025-06-11)

[Kim Morrison]

I've pushed a fix, but I think it may represent a problem in lean#8419, which I've asked Joachim about.

[github mathlib4 bot]

:cross_mark: lean4checker failed on 96db0ceb66e5b4d468a52c4c5fc5ac57cc6f8bd9 (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 2d1d08870598f86de8f9ca84096c7be87393955e (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 2eda5e7435c2e3e23f7b195a49c4e7043d863533 (branch: nightly-testing-2025-06-20)

[Kim Morrison]

Uh, that is long out of date...

[Kim Morrison]

I'm leaving on vacation shortly, not sure if I'll have a change to look into this.

[Kyle Miller]

If I understand it correctly, this is only failing because it's running from within mathlib4 instead of mathlib4-nightly-testing, 6/20 is the last tag

[Kyle Miller]

I guess it's failing on mathlib4-nightly-testing too https://github.com/leanprover-community/mathlib4-nightly-testing/actions/runs/16038341471

[github mathlib4 bot]

:cross_mark: lean4checker failed on ede29a38dfb2b9841d4898ff4525e9504667a057 (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 0faf9c7e5dce691f1a9e2e5dc1aa2499e9acb2e0 (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 4ed2ceba51063e4887ef21baa38f709d1661c301 (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on d3c315dc6c0723c2a561fd5439cfad56722f412b (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 7e05fd873e316333cfff5f644da91ebd62993dee (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on fb6a587d402f3b0288e4784fa2f6d5ff7c41d1e7 (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 97e6e3577558f501ae6f8b6128ddfc329ee5ad2a (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on d19cd93f3db24ca3a2ab957c266dd7e1ce2110fa (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on ba454ce1f3d3aabc948e53f57d8f06854c4f6eb1 (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on a4ebcd794d82f768641a4038a78a8851e77a6561 (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on fd96d2d94a0d2189bf9954f90f66d0afe1e01549 (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 507dd92b9ed9cfd43bd29d1438a458da6705d8a0 (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 3a0740877285c805a03d44b40df45106225dc21b (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on c728e645fccf7166c3ac71ce0c1ca1a32c10a268 (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on bc70da8fd1d791a61ad9089b6a8da1dc671b9198 (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on f1fa81263df46efbfc4d51ae3dd003886cb0b75b (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 6ba5988137ea253926c083cf7aab9c552ba570a5 (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 82ecf95ecd3b4a4620b9cfca5e027cffa258ee22 (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on bfeab816b74212c75960b441175e5f4e10868a5e (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 4b54a1d2ef9bf61679ddceab6bcf91163342d641 (branch: nightly-testing-2025-06-20)

[Notification Bot]

This topic was moved here from #mathlib reviewers > lean4checker failure by Kim Morrison.

[github mathlib4 bot]

:cross_mark: lean4checker failed on 8b7eb3d9b238206030ddc23cd407d0c82db0b922 (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 962b24680e61db073c65145453113f3050db540e (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 8271ba972112005e0dbee353ad6d5c4f1ee1c537 (branch: nightly-testing-2025-06-20)

[Sebastian Ullrich]

On my phone but probably just needs removal of extraConstNames arg

[github mathlib4 bot]

:cross_mark: lean4checker failed on 5ebccb65951c70539ba1c36e53e079ac28b3fd23 (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on c9e3dfadd09712e4b3345adec7b5eeb60fa73ed6 (branch: nightly-testing-2025-06-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on a77a0aeac5e8e691c32a65b878b02574930b5f90 (branch: nightly-testing-2025-10-17)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 5c98c223ad372ac3992aa23bd2a4a67cd6a9b13f (branch: nightly-testing-2025-10-17)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 9e574589c15b3b233d3223f1b35871a798cc2748 (branch: nightly-testing-2025-10-19)

[Kim Morrison]

This is some cache problem, not actually anything about lean4checker...?

[github mathlib4 bot]

:cross_mark: lean4checker failed on 560872a203ef726bf76117856ece2872f8cff918 (branch: nightly-testing-2025-10-20)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 4994494bf98173a5175569e85b6f5241e0c6085c (branch: nightly-testing-2025-10-21)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 0a7093c05f7e127e28ad1225001269ad06a4b2f8 (branch: nightly-testing-2025-10-21)

[github mathlib4 bot]

:cross_mark: lean4checker failed on b1e4080ea529b3f4f77f6f6a54e27f8ac31afc64 (branch: nightly-testing-2025-10-21)

[github mathlib4 bot]

:cross_mark: lean4checker failed on b1e4080ea529b3f4f77f6f6a54e27f8ac31afc64 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 97d68c420815bcbd8abc9915155055423d8775c7 (branch: nightly-testing-2025-10-21)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 97d68c420815bcbd8abc9915155055423d8775c7 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on f4dee013552444b4b058a624930590186361ac8e (branch: nightly-testing-2025-10-25)

[github mathlib4 bot]

:cross_mark: lean4checker failed on f4dee013552444b4b058a624930590186361ac8e (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 540c589f9555258461780f6cee59e27234079db9 (branch: nightly-testing-2025-10-26)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 540c589f9555258461780f6cee59e27234079db9 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 0a7fab8b65df0243da3c22ec6ef78f016f20057c (branch: nightly-testing-2025-10-27)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 0a7fab8b65df0243da3c22ec6ef78f016f20057c (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 9ceda6f59820dd51d9b9869ea229ccc593b6699c (branch: nightly-testing-2025-10-27)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 9ceda6f59820dd51d9b9869ea229ccc593b6699c (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 8dfff897ceb432b7ad45538a79db8afee7891446 (branch: nightly-testing-2025-10-29)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 8dfff897ceb432b7ad45538a79db8afee7891446 (branch: master)

[Bryan Gin-ge Chen]

Here are the leanchecker issues:

on master:

 lean4checker found a problem in Batteries.WF
uncaught exception: (kernel) unknown constant '_private.Batteries.WF.0.PSigma.casesOn._arg_pusher'

on nightly-testing-2025-10-29:

✖ [12/18] Building Lean4CheckerTests.ReduceBool (380ms)
error: Lean4CheckerTests/ReduceBool.lean:17:26: Application type mismatch: The argument
  ()
has type
  Unit
but is expected to have type
  Void IO.RealWorld
in the application
  exists_or_touch t ()
error: Lean4CheckerTests/ReduceBool.lean:26:46: Tactic `rfl` failed: The left-hand side
  true
is not definitionally equal to the right-hand side
  Lean.reduceBool foo

⊢ true = Lean.reduceBool foo

[Notification Bot]

A message was moved here from #nightly-testing > mathlib test executable failure by Bryan Gin-ge Chen.

[github mathlib4 bot]

:cross_mark: lean4checker failed on 6db5dd65524a270a0aad12ad8f8b8309b382d365 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 216082faaea7ce724da33feeaeaf56483f7d17ee (branch: nightly-testing-2025-10-29)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 216082faaea7ce724da33feeaeaf56483f7d17ee (branch: master)

[Kim Morrison]

Bryan Gin-ge Chen said:

on nightly-testing-2025-10-29:

✖ [12/18] Building Lean4CheckerTests.ReduceBool (380ms)
error: Lean4CheckerTests/ReduceBool.lean:17:26: Application type mismatch: The argument
  ()
has type
  Unit
but is expected to have type
  Void IO.RealWorld
in the application
  exists_or_touch t ()
error: Lean4CheckerTests/ReduceBool.lean:26:46: Tactic `rfl` failed: The left-hand side
  true
is not definitionally equal to the right-hand side
  Lean.reduceBool foo

⊢ true = Lean.reduceBool foo

Oh, oops, this was long ago removed from the master branch, after we made RealWorld opaque.

I will merge master into nightly-testing to resolve this.

(Although: interesting open problem if anyone feels like hacking: if anything like this still possible after the recent changes to IO?)

[Kim Morrison]

Hmm, maybe someone just did this? As far as I can see ReduceBool is gone on nightly-testing (indeed, nightly-testing coincides with master).

[Kim Morrison]

Bryan Gin-ge Chen said:

Here are the leanchecker issues:

on master:

 lean4checker found a problem in Batteries.WF
uncaught exception: (kernel) unknown constant '_private.Batteries.WF.0.PSigma.casesOn._arg_pusher'

This one I'm still playing with, so far unsuccessfully. It's a module system problem, and I'll escalate to Sebastian shortly if I don't find anything. :-)

[Bryan Gin-ge Chen]

Kim Morrison said:

Hmm, maybe someone just did this? As far as I can see ReduceBool is gone on nightly-testing (indeed, nightly-testing coincides with master).

I forgot to post a comment, but I also noticed that that error disappeared in the logs triggered by my testing above.

[github mathlib4 bot]

:cross_mark: lean4checker failed on be264471a4e199cbdc15f8bbf22da050ba59eea4 (branch: nightly-testing-2025-10-30)

[github mathlib4 bot]

:cross_mark: lean4checker failed on be264471a4e199cbdc15f8bbf22da050ba59eea4 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on f6d49f00dbba01b318a57979ae2bca95a374d157 (branch: nightly-testing-2025-10-31)

[github mathlib4 bot]

:cross_mark: lean4checker failed on f6d49f00dbba01b318a57979ae2bca95a374d157 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on c6541c05ebd2fc0f106db01858adaf8e7a783a79 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on c6541c05ebd2fc0f106db01858adaf8e7a783a79 (branch: nightly-testing-2025-10-31)

[github mathlib4 bot]

:cross_mark: lean4checker failed on e93118937acf127bf5c203937d61eb25802c265a (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on e93118937acf127bf5c203937d61eb25802c265a (branch: nightly-testing-2025-10-31)

[Kim Morrison]

I'm finally catching up on this a bit. I think https://github.com/leanprover/lean4checker/pull/70 will help a bit, just making sure we load the .private parts of the oleans during replay. Hopefully @Sebastian Ullrich can take a look?

But there are more problems, in fact a kernel type mismatch affecting proofs by well-founded recursion.

@Joachim Breitner, do you recognise anything in this gist as having to do with changes there?

[Sebastian Ullrich]

Oh, I didn't know it uses readModuleData. Maybe there should be an easier way to do this but this looks about right.

[Sebastian Ullrich]

Maybe findOLeanParts could be made public at least

[Joachim Breitner]

So this kernel failure comes when replaying a file that was accepted by Lean nicely before?

In the gist I see mentions of WF.fix on the one side but not the other. That could be if some proof required to reduce the well-founded proof was available when lean itself processed the file, but not during replaying.

Although we try to not let the user rely on that. Are there proofs by rfl or decode +kernel that override the transparency here?

[Joachim Breitner]

Does lean4checker accept it in the more where it replays the whole environment?

[Kim Morrison]

Yes, with --fresh it is accepted.

[Kim Morrison]

I guess this file has no imports, so easy enough to minimize...

[Kim Morrison]

Hmm... when copied over to the lean4checker repo, it doesn't find a problem.

[Kim Morrison]

Haven't sorted this out, but did discover that there are going to be further lean4checker failures in Batteries, e.g.

% lake env lean4checker/.lake/build/bin/lean4checker Batteries
lean4checker found a problem in Batteries.Lean.LawfulMonadLift
uncaught exception: (kernel) constant has already been declared 'readThe.eq_1'

[github mathlib4 bot]

:cross_mark: lean4checker failed on fa7b276c71c3a9669b3dfe613c2fd0feec897d4d (branch: nightly-testing-2025-11-03)

[github mathlib4 bot]

:cross_mark: lean4checker failed on fa7b276c71c3a9669b3dfe613c2fd0feec897d4d (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 99382bdb6d83d7551b73335837b9915b8a711433 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 99382bdb6d83d7551b73335837b9915b8a711433 (branch: nightly-testing-2025-11-04)

[github mathlib4 bot]

:cross_mark: lean4checker failed on ef5f4caf0b4f01f48be2c73fbc5a32ec81b3c0fb (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on ef5f4caf0b4f01f48be2c73fbc5a32ec81b3c0fb (branch: nightly-testing-2025-11-05)

[github mathlib4 bot]

:cross_mark: lean4checker failed on c6b32768f84e15b2366579f718d44679e3d4a8ae (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on c6b32768f84e15b2366579f718d44679e3d4a8ae (branch: nightly-testing-2025-11-06)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 7b7099258dce6def5970879a83d3438e1c9d4f4f (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 7b7099258dce6def5970879a83d3438e1c9d4f4f (branch: nightly-testing-2025-11-06)

[github mathlib4 bot]

:cross_mark: lean4checker failed on c468bb75ca2444ed0e116b35a3e653afd6ab448e (branch: nightly-testing-2025-11-08)

[github mathlib4 bot]

:cross_mark: lean4checker failed on c468bb75ca2444ed0e116b35a3e653afd6ab448e (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 4e1b076085d73f91322e3bd2b9383f73ad17c300 (branch: nightly-testing-2025-11-08)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 4e1b076085d73f91322e3bd2b9383f73ad17c300 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 35a04350393d710cc719a762a55dc71fca800064 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 35a04350393d710cc719a762a55dc71fca800064 (branch: nightly-testing-2025-11-10)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 00eaaa3d57d9ef1413d9a2bbd86b2fd1ce3853f2 (branch: nightly-testing-2025-11-11)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 00eaaa3d57d9ef1413d9a2bbd86b2fd1ce3853f2 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 13da915e33c92666c61c94df6e05d1632547f2c7 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 13da915e33c92666c61c94df6e05d1632547f2c7 (branch: nightly-testing-2025-11-12)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 2b55585f6ca88510fa949986e6ed144babdb6b99 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 2b55585f6ca88510fa949986e6ed144babdb6b99 (branch: nightly-testing-2025-11-13)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 48b7eb4c1789b21a9804ba876d458c2e95b45fd7 (branch: nightly-testing-2025-11-14)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 48b7eb4c1789b21a9804ba876d458c2e95b45fd7 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 01c9c6d09c5d72ae24d905d5117bc86a21a9aa36 (branch: nightly-testing-2025-11-15)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 01c9c6d09c5d72ae24d905d5117bc86a21a9aa36 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 1ccd71f89cbbd82ae7d097723ce1722ca7b01c33 (branch: nightly-testing-2025-11-16)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 1ccd71f89cbbd82ae7d097723ce1722ca7b01c33 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 79c8606dff454266fe64ae621d904453c964e71d (branch: nightly-testing-2025-11-17)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 79c8606dff454266fe64ae621d904453c964e71d (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 48d1fe28293a3dec35b08ca9728373fe7302f7fa (branch: nightly-testing-2025-11-18)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 48d1fe28293a3dec35b08ca9728373fe7302f7fa (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 5db9169e8817127f3f75b545720e7fb74e0adf85 (branch: nightly-testing-2025-11-18)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 5db9169e8817127f3f75b545720e7fb74e0adf85 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 0c25ddf80940f9c39ef3405115eb5a4355ad30bc (branch: nightly-testing-2025-12-09)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 0c25ddf80940f9c39ef3405115eb5a4355ad30bc (branch: master)

[Kim Morrison]

(The lean4checker had been killed due to out of memory errors during CI. So these failure messages are positive progress! Sebastian Ullrich is looking at lean4checker soon to take care of the module system fallout.)

[github mathlib4 bot]

:cross_mark: lean4checker failed on d39a7b82e47795088c82998756682fec28c5e8d2 (branch: nightly-testing-2025-12-10)

[github mathlib4 bot]

:cross_mark: lean4checker failed on d39a7b82e47795088c82998756682fec28c5e8d2 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on c671bc4215d64bd9cc8a84fdec9a12bd33fdcd26 (branch: nightly-testing-2025-12-10)

[github mathlib4 bot]

:cross_mark: lean4checker failed on c671bc4215d64bd9cc8a84fdec9a12bd33fdcd26 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on c671bc4215d64bd9cc8a84fdec9a12bd33fdcd26 (branch: master)

[github mathlib4 bot]

:cross_mark: lean4checker failed on 3f5aae8dc2d83cdd3214e158c2b34a756281e3c2 (branch: master)