Lean4lean CI hanging

Stream: Equational

[Terence Tao]

The most recent PRs are not passing CI due to Lean4Lean hanging, see https://github.com/teorth/equational_theories/actions/runs/15838296584/job/44646243572?pr=1255 and https://github.com/teorth/equational_theories/actions/runs/15850635493/job/44682964502?pr=1256 . Anyone have any idea what is happening here?

[Mario Carneiro]

@Pietro Monticone the lean4lean build script should report what commit it checked out

[Mario Carneiro]

the relevant part of the log is this:

2025-06-24T00:57:16.5467393Z adding thmDecl Law3959_implies_Law4369
2025-06-24T00:57:16.5467844Z adding thmDecl Equation2741_implies_Equation3214
2025-06-24T00:57:17.4968265Z Error: index out of bounds
2025-06-24T00:57:17.4968699Z backtrace:
2025-06-24T00:57:17.5502144Z /home/runner/work/equational_theories/equational_theories/lean4lean/.lake/build/bin/lean4lean(lean_panic+0xf5) [0x55cee8d8fff5]
2025-06-24T00:57:17.5505143Z /home/runner/work/equational_theories/equational_theories/lean4lean/.lake/build/bin/lean4lean(lean_array_get_panic+0x69) [0x55cee8d908c9]
2025-06-24T00:57:17.5507143Z /home/runner/work/equational_theories/equational_theories/lean4lean/.lake/build/bin/lean4lean(l_Lean_PersistentEnvExtension_getModuleEntries_unsafe__1___rarg+0xbb) [0x55cee2245b9b]
2025-06-24T00:57:17.5509122Z /home/runner/work/equational_theories/equational_theories/lean4lean/.lake/build/bin/lean4lean(l_Lean_getStructureInfo_x3f+0x72) [0x55cee3e4a4f2]
2025-06-24T00:57:17.5511015Z /home/runner/work/equational_theories/equational_theories/lean4lean/.lake/build/bin/lean4lean(l_Lean_isStructure+0x6) [0x55cee3e4dfa6]
2025-06-24T00:57:17.5512985Z /home/runner/work/equational_theories/equational_theories/lean4lean/.lake/build/bin/lean4lean(l_Lean_PrettyPrinter_Delaborator_delabStructureInstance+0x3db) [0x55cee38eb53b]
2025-06-24T00:57:17.5514848Z /home/runner/work/equational_theories/equational_theories/lean4lean/.lake/build/bin/lean4lean(lean_apply_7+0x1ed) [0x55cee8da848d]
2025-06-24T00:57:17.5516739Z /home/runner/work/equational_theories/equational_theories/lean4lean/.lake/build/bin/lean4lean(l_List_firstM___at_Lean_PrettyPrinter_Delaborator_delabFor___spec__1+0x160) [0x55cee29f7ce0]
2025-06-24T00:57:17.5519114Z /home/runner/work/equational_theories/equational_theories/lean4lean/.lake/build/bin/lean4lean(l_Lean_PrettyPrinter_Delaborator_delabFor+0x1b7) [0x55cee29f88a7]
2025-06-24T00:57:17.5521033Z /home/runner/work/equational_theories/equational_theories/lean4lean/.lake/build/bin/lean4lean(lean_apply_7+0x9a8) [0x55cee8da8c48]

[Mario Carneiro]

Two days ago I pushed a fix for errors of this form, so it's interesting you are only now getting the error

[Terence Tao]

We haven't had much PR activity recently

[Mario Carneiro]

The question is whether this run is using a version of lean4lean before or after that fix. Having the commit in the log would answer it definitively, but based on the timing it seems like it should be after

[Pietro Monticone]

I’m not very familiar with this since I’ve never touched the lean4lean_checker/main.py script.

@Shreyas Srinivas could you take a look?

If necessary I will be able to take a look at it in a few hours.

[Mario Carneiro]

oh, you were on the git blame, I should have looked more carefully

[Mario Carneiro]

I managed to reproduce it locally on l4l master

[Shreyas Srinivas]

I will only have time to look at it in a few hours from now

[Mario Carneiro]

recommend you just remove l4l from the build for now if you are impatient to get things through

[Mario Carneiro]

or use lean4checker instead

[Shreyas Srinivas]

we already have lean4checker

[Mario Carneiro]

(I appreciate you all using this program in production though)

[Shreyas Srinivas]

I added it back when there was some AI experimentation, to be extra certain and because it gave me a chance to play with l4l

[Shreyas Srinivas]

equational#1257 disables lean4lean. It is ready for merge once CI is green.

[Shreyas Srinivas]

The most likely source of error is a toolchain mismatch. The toolchain matching in the script works on assumptions about how lake update behaved on math projects at the time the script was written

[Shreyas Srinivas]

This might have changed since then

[Shreyas Srinivas]

Update : The toolchains match.

[Mario Carneiro]

The error-in-error-reporting issue has been fixed; now you get the following error:

$ lean4lean equational_theories.Generated.All4x4Tables.Refutation1
lean4lean found a problem in equational_theories.Generated.All4x4Tables.Refutation1:
(kernel) application type mismatch
  @id
    (@Eq Bool
      (Decidable.decide
        (MemoFinOp.IsTable 7
          (@List.cons Nat 1132518468420096
            (@List.cons Nat 1409586792104196
              (@List.cons Nat 845550278803461
                (@List.cons Nat 567352345232646
                  (@List.cons Nat 3315748636161
                    (@List.cons Nat 286972635775746 (@List.cons Nat 1688858534151171 (@List.nil Nat)))))))))
        (MemoFinOp.decidableIsTable 7
          (@List.cons Nat 1132518468420096
            (@List.cons Nat 1409586792104196
              (@List.cons Nat 845550278803461
                (@List.cons Nat 567352345232646
                  (@List.cons Nat 3315748636161
                    (@List.cons Nat 286972635775746 (@List.cons Nat 1688858534151171 (@List.nil Nat))))))))))
      Bool.true)
    (@Eq.refl Bool Bool.true)
argument has type
  @Eq Bool Bool.true Bool.true
but function has type
  @Eq Bool
      (Decidable.decide
        (MemoFinOp.IsTable 7
          (@List.cons Nat 1132518468420096
            (@List.cons Nat 1409586792104196
              (@List.cons Nat 845550278803461
                (@List.cons Nat 567352345232646
                  (@List.cons Nat 3315748636161
                    (@List.cons Nat 286972635775746 (@List.cons Nat 1688858534151171 (@List.nil Nat)))))))))
        (MemoFinOp.decidableIsTable 7
          (@List.cons Nat 1132518468420096
            (@List.cons Nat 1409586792104196
              (@List.cons Nat 845550278803461
                (@List.cons Nat 567352345232646
                  (@List.cons Nat 3315748636161
                    (@List.cons Nat 286972635775746 (@List.cons Nat 1688858534151171 (@List.nil Nat))))))))))
      Bool.true →
    @Eq Bool
      (Decidable.decide
        (MemoFinOp.IsTable 7
          (@List.cons Nat 1132518468420096
            (@List.cons Nat 1409586792104196
              (@List.cons Nat 845550278803461
                (@List.cons Nat 567352345232646
                  (@List.cons Nat 3315748636161
                    (@List.cons Nat 286972635775746 (@List.cons Nat 1688858534151171 (@List.nil Nat)))))))))
        (MemoFinOp.decidableIsTable 7
          (@List.cons Nat 1132518468420096
            (@List.cons Nat 1409586792104196
              (@List.cons Nat 845550278803461
                (@List.cons Nat 567352345232646
                  (@List.cons Nat 3315748636161
                    (@List.cons Nat 286972635775746 (@List.cons Nat 1688858534151171 (@List.nil Nat))))))))))
      Bool.true

[Mario Carneiro]

(I'm out of time to look into this, it might be a few days before I can debug more)

[Shreyas Srinivas]

But lean4checker passed

[Mario Carneiro]

oh, it was actually easy to fix, lean4lean wasn't implementing some of the new kernel accelerated functions (bitwise ops were added as new primitives in the last release)

[Mario Carneiro]

because the functions are implemented with well founded recursion, lean can't actually compute them if not for kernel acceleration