mathlib test executable failure

Stream: nightly-testing

[Kim Morrison]

github mathlib4 bot said:

:cross_mark: mathlib_test_executable failed on 73094ff2aa9a2188dd00a9847afc362f6d66b560 (branch: nightly-testing-2025-03-17)

Oh dear! This is a test that runs each day to check that an executable with import Mathlib can actually run.

Today it failed with a bunch of errors like:

././.lake/build/ir/Mathlib/Computability/TMToPartrec.c:2121:26: error: redefinition of 'l_Turing_PartrecToTM2_Cont_x27___sizeOf__1'
LEAN_EXPORT lean_object* l_Turing_PartrecToTM2_Cont_x27___sizeOf__1(lean_object* x_1) {

Any ideas?

[Kim Morrison]

I am guessing that asynchronous elaboration is the cause... Sorry @Sebastian Ullrich!

[Sebastian Ullrich]

@Kim Morrison Thanks, this turned out to be a regression in compile_inductive%. Which wasn't even needed in the breaking file but I nevertheless pushed a fix to nightly-testing... hopefully this will all become obsolete with the new codegen

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 2d1d08870598f86de8f9ca84096c7be87393955e (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 2eda5e7435c2e3e23f7b195a49c4e7043d863533 (branch: master)

[Kim Morrison]

This is new and alarming!

[Kim Morrison]

Oh, it is the wrong test reporting. Actually this is lean4checker.

[Ruben Van de Velde]

error: Lean4CheckerTests/ReplaceAxiom.lean:19:14: function expected at
  { constants := consts, quotInit := env.toKernelEnv.quotInit, diagnostics := env.toKernelEnv.diagnostics,
    const2ModIdx := env.toKernelEnv.const2ModIdx, extensions := Lean.Kernel.Environment.extensions✝ env.toKernelEnv,
    extraConstNames := ∅ }
term has type
  Kernel.Environment
error: Lean4CheckerTests/ReplaceAxiom.lean:32:2: type mismatch
  propext
has type
  (?m.472 ↔ ?m.473) → ?m.472 = ?m.473 : Prop
but is expected to have type
  False : Prop

[Kim Morrison]

It is also the executable test, actually.

[Kim Morrison]

lean4checker is working on its v4.22.0-rc2 tag

[Kim Morrison]

Hmm, and I updated lean4checker's nightly-testing branch to leanprover/lean4:nightly-2025-07-03, and lake test works fine there.

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on ede29a38dfb2b9841d4898ff4525e9504667a057 (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 0faf9c7e5dce691f1a9e2e5dc1aa2499e9acb2e0 (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 4ed2ceba51063e4887ef21baa38f709d1661c301 (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on d3c315dc6c0723c2a561fd5439cfad56722f412b (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 7e05fd873e316333cfff5f644da91ebd62993dee (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on fb6a587d402f3b0288e4784fa2f6d5ff7c41d1e7 (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 97e6e3577558f501ae6f8b6128ddfc329ee5ad2a (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on d19cd93f3db24ca3a2ab957c266dd7e1ce2110fa (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on ba454ce1f3d3aabc948e53f57d8f06854c4f6eb1 (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on a4ebcd794d82f768641a4038a78a8851e77a6561 (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on fd96d2d94a0d2189bf9954f90f66d0afe1e01549 (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 507dd92b9ed9cfd43bd29d1438a458da6705d8a0 (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 3a0740877285c805a03d44b40df45106225dc21b (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on c728e645fccf7166c3ac71ce0c1ca1a32c10a268 (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on bc70da8fd1d791a61ad9089b6a8da1dc671b9198 (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on f1fa81263df46efbfc4d51ae3dd003886cb0b75b (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 6ba5988137ea253926c083cf7aab9c552ba570a5 (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 82ecf95ecd3b4a4620b9cfca5e027cffa258ee22 (branch: master)

[Ruben Van de Velde]

Should we turn this off?

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on bfeab816b74212c75960b441175e5f4e10868a5e (branch: master)

[Kim Morrison]

On the contrary, it needs fixing. I'm guessing this is a consequence of the new compiler.

[Kim Morrison]

✖ [12419/13963] Building Mathlib.Computability.TMToPartrec:c.o

[5432](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5433)trace: .> /home/runner/.elan/toolchains/leanprover--lean4---v4.22.0-rc3/bin/clang -c -o /home/runner/work/mathlib4/mathlib4/.lake/build/ir/Mathlib/Computability/TMToPartrec.c.o.export /home/runner/work/mathlib4/mathlib4/.lake/build/ir/Mathlib/Computability/TMToPartrec.c -I /home/runner/.elan/toolchains/leanprover--lean4---v4.22.0-rc3/include -fstack-clash-protection -fwrapv -fPIC -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /home/runner/.elan/toolchains/leanprover--lean4---v4.22.0-rc3 -nostdinc -isystem /home/runner/.elan/toolchains/leanprover--lean4---v4.22.0-rc3/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING

[5433](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5434)info: stderr:

[5434](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5435)/home/runner/work/mathlib4/mathlib4/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:2350:26: error: redefinition of 'l_Turing_PartrecToTM2_Cont_x27___sizeOf__1'

[5435](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5436) 2350 | LEAN_EXPORT lean_object* l_Turing_PartrecToTM2_Cont_x27___sizeOf__1(lean_object* x_1) {

[5436](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5437) | ^

[5437](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5438)/home/runner/work/mathlib4/mathlib4/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:1698:26: note: previous definition is here

[5438](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5439) 1698 | LEAN_EXPORT lean_object* l_Turing_PartrecToTM2_Cont_x27___sizeOf__1(lean_object* x_1) {

[5439](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5440) | ^

[5440](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5441)/home/runner/work/mathlib4/mathlib4/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:2369:21: error: redefinition of '_init_l_Turing_PartrecToTM2_Cont_x27___sizeOf__inst'

[5441](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5442) 2369 | static lean_object* _init_l_Turing_PartrecToTM2_Cont_x27___sizeOf__inst() {

[5442](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5443) | ^

[5443](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5444)/home/runner/work/mathlib4/mathlib4/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:1742:21: note: previous definition is here

[5444](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5445) 1742 | static lean_object* _init_l_Turing_PartrecToTM2_Cont_x27___sizeOf__inst() {

[5445](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5446) | ^

[5446](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5447)/home/runner/work/mathlib4/mathlib4/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:2377:26: error: redefinition of 'l_Turing_PartrecToTM2_K_x27___sizeOf__1'

[5447](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5448) 2377 | LEAN_EXPORT lean_object* l_Turing_PartrecToTM2_K_x27___sizeOf__1(uint8_t x_1) {

[5448](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5449) | ^

[5449](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5450)/home/runner/work/mathlib4/mathlib4/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:1914:26: note: previous definition is here

[5450](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5451) 1914 | LEAN_EXPORT lean_object* l_Turing_PartrecToTM2_K_x27___sizeOf__1(uint8_t x_1) {

[5451](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5452) | ^

[5452](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5453)/home/runner/work/mathlib4/mathlib4/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:2385:26: error: redefinition of 'l_Turing_PartrecToTM2_K_x27___sizeOf__1___boxed'

[5453](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5454) 2385 | LEAN_EXPORT lean_object* l_Turing_PartrecToTM2_K_x27___sizeOf__1___boxed(lean_object* x_1) {

[5454](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5455) | ^

[5455](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5456)/home/runner/work/mathlib4/mathlib4/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:1922:26: note: previous definition is here

[5456](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5457) 1922 | LEAN_EXPORT lean_object* l_Turing_PartrecToTM2_K_x27___sizeOf__1___boxed(lean_object* x_1) {

[5457](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5458) | ^

[5458](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5459)/home/runner/work/mathlib4/mathlib4/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:2403:21: error: redefinition of '_init_l_Turing_PartrecToTM2_K_x27___sizeOf__inst'

[5459](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5460) 2403 | static lean_object* _init_l_Turing_PartrecToTM2_K_x27___sizeOf__inst() {

[5460](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5461) | ^

[5461](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5462)/home/runner/work/mathlib4/mathlib4/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:1940:21: note: previous definition is here

[5462](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5463) 1940 | static lean_object* _init_l_Turing_PartrecToTM2_K_x27___sizeOf__inst() {

[5463](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5464) | ^

[5464](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5465)5 errors generated.

[5465](https://github.com/leanprover-community/mathlib4/actions/runs/16431224324/job/46432889097#step:10:5466)error: external command '/home/runner/.elan/toolchains/leanprover--lean4---v4.22.0-rc3/bin/clang' exited with code 1

[Kim Morrison]

Actually, it appears to be working on the corresponding nightly-testing run, so I think just waiting a week should suffice.

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 4b54a1d2ef9bf61679ddceab6bcf91163342d641 (branch: master)

[Kim Morrison]

(Cameron has reported this in the meantime as https://github.com/leanprover-community/mathlib4/issues/27017.)

[Kim Morrison]

Kim Morrison said:

Actually, it appears to be working on the corresponding nightly-testing run, so I think just waiting a week should suffice.

Unfortunately, this is not the case and it is a problem on nightly-testing too.

[Kim Morrison]

@Mario Carneiro, as this problem is arising in TMToPartrec, might you be interested in minimising it?

[Mario Carneiro]

will investigate some time tomorrow

[Kim Morrison]

False alarm, I now see Cameron has already got a fix in the works.

[Notification Bot]

40 messages were moved here from #mathlib reviewers > mathlib test executable failure by Kim Morrison.

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 8b7eb3d9b238206030ddc23cd407d0c82db0b922 (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 962b24680e61db073c65145453113f3050db540e (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 595c2c615b545c3421ac5f8b568efee290e73962 (branch: )

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 595c2c615b545c3421ac5f8b568efee290e73962 (branch: master)

[Kim Morrison]

that's a new one

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 593962960e4910da0d0597910c3288ec1c821c82 (branch: )

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 593962960e4910da0d0597910c3288ec1c821c82 (branch: master)

[Kim Morrison]

I've just run this locally under lldb:

% lake env lldb .lake/build/bin/mathlib_test_executable
(lldb) target create ".lake/build/bin/mathlib_test_executable"
Current executable set to '/Users/kim/projects/lean/mathlib4/.lake/build/bin/mathlib_test_executable' (arm64).
(lldb) run
Process 75135 launched: '/Users/kim/projects/lean/mathlib4/.lake/build/bin/mathlib_test_executable' (arm64)
Process 75135 stopped
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x1)
    frame #0: 0x00000001024a3258 mathlib_test_executable`l_CategoryTheory_InducedCategory_category___redArg + 28
mathlib_test_executable`l_CategoryTheory_InducedCategory_category___redArg:
->  0x1024a3258 <+28>: ldr    w8, [x1]
    0x1024a325c <+32>: cmp    w8, #0x1
    0x1024a3260 <+36>: b.lt   0x1024a332c               ; <+240>
    0x1024a3264 <+40>: add    w8, w8, #0x1
Target 0: (mathlib_test_executable) stopped.
(lldb) bt
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x1)
  * frame #0: 0x00000001024a3258 mathlib_test_executable`l_CategoryTheory_InducedCategory_category___redArg + 28
    frame #1: 0x000000010328a594 mathlib_test_executable`initialize_Mathlib_CategoryTheory_FintypeCat + 364
    frame #2: 0x000000010328bb48 mathlib_test_executable`initialize_Mathlib_Order_Category_FinPartOrd + 156
    frame #3: 0x000000010328f830 mathlib_test_executable`initialize_Mathlib_Order_Category_NonemptyFinLinOrd + 360
    frame #4: 0x0000000103294818 mathlib_test_executable`initialize_Mathlib_AlgebraicTopology_SimplexCategory_Basic + 228
    frame #5: 0x00000001032a6170 mathlib_test_executable`initialize_Mathlib_AlgebraicTopology_SimplicialObject_Basic + 140
    frame #6: 0x00000001032a9074 mathlib_test_executable`initialize_Mathlib_AlgebraicTopology_MooreComplex + 184
    frame #7: 0x00000001032ace94 mathlib_test_executable`initialize_Mathlib_AlgebraicTopology_AlternatingFaceMapComplex + 184
    frame #8: 0x00000001032bf1a8 mathlib_test_executable`initialize_Mathlib_AlgebraicTopology_ExtraDegeneracy + 140
    frame #9: 0x00000001032bf77c mathlib_test_executable`initialize_Mathlib_Algebra_Homology_AlternatingConst + 228
    frame #10: 0x0000000105016bb0 mathlib_test_executable`initialize_Mathlib + 28100
    frame #11: 0x0000000100000a44 mathlib_test_executable`initialize_MathlibTest_MathlibTestExecutable + 404
    frame #12: 0x0000000100000b94 mathlib_test_executable`main + 36
    frame #13: 0x0000000198c3b154 dyld`start + 2476

[Kim Morrison]

Reducing the imports from

import Lean
import Std
import Qq
import Batteries
import Aesop
import ProofWidgets
import Mathlib
import Plausible

down to

import Mathlib.CategoryTheory.FintypeCat

in MathlibTest/MathlibTestExecutable.lean preserves the problem:

% lake env lldb .lake/build/bin/mathlib_test_executable
(lldb) target create ".lake/build/bin/mathlib_test_executable"
Current executable set to '/Users/kim/projects/lean/mathlib4/.lake/build/bin/mathlib_test_executable' (arm64).
(lldb) run
Process 76187 launched: '/Users/kim/projects/lean/mathlib4/.lake/build/bin/mathlib_test_executable' (arm64)
Process 76187 stopped
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x1)
    frame #0: 0x00000001014ad028 mathlib_test_executable`l_CategoryTheory_InducedCategory_category___redArg + 28
mathlib_test_executable`l_CategoryTheory_InducedCategory_category___redArg:
->  0x1014ad028 <+28>: ldr    w8, [x1]
    0x1014ad02c <+32>: cmp    w8, #0x1
    0x1014ad030 <+36>: b.lt   0x1014ad0fc               ; <+240>
    0x1014ad034 <+40>: add    w8, w8, #0x1
Target 0: (mathlib_test_executable) stopped.
(lldb) bt
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x1)
  * frame #0: 0x00000001014ad028 mathlib_test_executable`l_CategoryTheory_InducedCategory_category___redArg + 28
    frame #1: 0x000000010171a7b8 mathlib_test_executable`initialize_Mathlib_CategoryTheory_FintypeCat + 364
    frame #2: 0x000000010000093c mathlib_test_executable`initialize_MathlibTest_MathlibTestExecutable + 140
    frame #3: 0x00000001000009d8 mathlib_test_executable`main + 36
    frame #4: 0x0000000198c3b154 dyld`start + 2476

but replacing that with its own imports, i.e.

import Mathlib.CategoryTheory.ConcreteCategory.Basic
import Mathlib.CategoryTheory.Endomorphism
import Mathlib.CategoryTheory.Skeletal
import Mathlib.Data.Finite.Prod

resolves the problem.

So it does seem that one can not make an executable under v4.23.0-rc2 with import Mathlib.CategoryTheory.FintypeCat!

[Kim Morrison]

That file looks perfectly innocuous, so I think it's time to ping @Cameron Zwarich to see if he has any initial guesses.

I'm happy to try to reduce the problem to something Mathlib free, but I'll hold off on that just now.

[Cameron Zwarich]

Thanks @Kim Morrison. I’ll take a look tomorrow. I doubt there will be any need to reduce this.

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on e128198aec7b902f875f8c17ffc6d590d18d0d48 (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on e128198aec7b902f875f8c17ffc6d590d18d0d48 (branch: )

[Cameron Zwarich]

I've got a (one line) fix, just need to write a test. It's due to some ref count optimizations assuming that an arrow type is represented by an actual object rather than a tagged pointer, but in the case of generic code we can have Type 1 : Type 2 and a function type X -> Type 1 that gets erased because it is a type former. When we are forced to represent an erased type for polymorphism reasons, we choose a tagged scalar.

[Cameron Zwarich]

The fix is in #9972. I'll merge it to the release branch once it lands.

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on ea164ea50e661d88b461778418e8cee806e12940 (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on ea164ea50e661d88b461778418e8cee806e12940 (branch: )

[Kim Morrison]

lean#9972

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 8bb991a4a08f76e3acc412600e834b09ec9d55b4 (branch: master)

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 8bb991a4a08f76e3acc412600e834b09ec9d55b4 (branch: )

[Kim Morrison]

We weren't actually expecting a success here, as this bot only tests against the successful nightly-testing-YYYY-MM-DD tags, and one including lean#9972 doesn't exist yet (hopefully soon).

But the fact it says (branch: ) is a bigger problem; this bot was never updated after we split nightly-testing to a separate repo. Fixing now.

[Kim Morrison]

#28673

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[Kim Morrison]

This needs diagnosing, but I haven't got to it in the last few days.

[Kim Morrison]

Moreover, the CI output is a bit weird: it's hard to work out if the failures are about the mathlib_test_executable or lean4checker (or, I suspect, both!)

[Kim Morrison]

It would also be nice if this bot either posted something more like an action item, or said something about whose problem this failure is. :-)

[github mathlib4 bot]

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

[github mathlib4 bot]

:cross_mark: mathlib_test_executable failed on 4994494bf98173a5175569e85b6f5241e0c6085c (branch: master)

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[Bryan Gin-ge Chen]

Both master and nightly-testing-2025-10-29 have some issue with proofWidgets in the mathlib_test_executable step.

On master:

✖ [323/372] Building proofwidgets/widgetJsAll
error: ProofWidgets not up-to-date. Please run `lake exe cache get` to fetch the latest ProofWidgets. If this does not work, report your issue on the Lean Zulip.

On nightly-testing-2025-10-29:

✖ [324/395] Building proofwidgets/widgetJsAll
error: ProofWidgets not up-to-date. Please run `lake exe cache get` to fetch the latest ProofWidgets. If this does not work, report your issue on the Lean Zulip.

[Bryan Gin-ge Chen]

I'll try and make some simple improvements to the workflows here so that the links at least go to the right place. Probably it'd be good to post about leanchecker failures in a separate thread as well.

[Damiano Testa]

What is it about proofWidgets that shows up so often when build errors occur?

[Bryan Gin-ge Chen]

No idea... I would have thought we would also see this error on master but I guess there's something different when you tell lean to compile an executable?

[Damiano Testa]

I don't know, but if there was a way of diagnosing what it is, maybe there might be something that can be done for decreasing the number of times that ProofWidgets is not up-to-date.

[Bryan Gin-ge Chen]

Kim Morrison said:

Moreover, the CI output is a bit weird: it's hard to work out if the failures are about the mathlib_test_executable or lean4checker (or, I suspect, both!)

It's not clear from the messages posted here, but apparently the bot is already posting lean4checker errors to a separate thread: #nightly-testing > lean4checker failure

[Notification Bot]

A message was moved from this topic to #nightly-testing > lean4checker failure by Bryan Gin-ge Chen.

[Bryan Gin-ge Chen]

#31096 makes it so that the bot's zulip messages link to the specific step; this should make the mesages a bit more clear.

I've hooked the bot up to pushes to that branch so we should see some messages here and in the lean4checker thread in an hour or so.

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[Bryan Gin-ge Chen]

Testing of #31096 is done. Note that the "failed" links in the 3 most recent posts in this thread and #nightly-testing > lean4checker failure now take you directly to the relevant step.

I couldn't think of an easy way to link to the line where the error was in the log. Although I believe we could use the wrapper in #30852 to extract the error and post it to Zulip if we wanted.

[Kim Morrison]

Bryan Gin-ge Chen said:

Testing of #31096 is done. Note that the "failed" links in the 3 most recent posts in this thread and #nightly-testing > lean4checker failure now take you directly to the relevant step.

I couldn't think of an easy way to link to the line where the error was in the log. Although I believe we could use the wrapper in #30852 to extract the error and post it to Zulip if we wanted.

:writing:

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[github mathlib4 bot]

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

[Kim Morrison]

This test has not been reporting since November 20 (either here or on the successes thread), because the same workflow runs this and lean4checker, and lean4checker starting OOM'ing around November 20...

[Kim Morrison]

I'm attempting to fix that OOM, but if perhaps someone could look into separating these two daily tasks into separate CI jobs, so they can't interfere?

[Bryan Gin-ge Chen]

I might be able to take a look in a few days. Note to self (or anyone who wants to take this up) we should also make sure that the failure message gets posted in cases like this.

[Bryan Gin-ge Chen]

Kim Morrison said:

I'm attempting to fix that OOM, but if perhaps someone could look into separating these two daily tasks into separate CI jobs, so they can't interfere?

I opened #33046 for this and a few other tweaks.