Cryptic failure on PR #26626

Stream: general

[Pierre Quinton]

In #26626, we are having a rather cryptic failure of the build that we cannot solve. This seems unrelated to the content of the PR and @Yaël Dillies said:

This is really weird. If you remove import Mathlib.Order.Category.PartOrd from Mathlib.Order.Category.BddOrd, then the error disappears (but of course you get errors instead telling you that Lean can't find PartOrd). Please raise this on Zulip!

Hence here I am. Any help would be welcome!

[Henrik Böving]

This is a code generator bug, CC @Cameron Zwarich

/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(lean_panic+0xf5) [0x731f4b60cce5]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(lean_array_get_panic+0x69) [0x731f4b60d599]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(l_Std_Range_forIn_x27_loop___at___Lean_IR_ToIR_lowerLet_spec__2___redArg+0xba) [0x731f479efafa]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(l_Lean_IR_ToIR_lowerLet+0xa029) [0x731f479e6aa9]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(l_Lean_IR_ToIR_lowerLet_lowerNonObjectFields___redArg+0x30) [0x731f479f20a0]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(l_Lean_IR_ToIR_lowerLet+0xaf8b) [0x731f479e7a0b]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(l_Lean_IR_ToIR_lowerLet_lowerNonObjectFields___redArg+0x30) [0x731f479f20a0]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(l_Lean_IR_ToIR_lowerLet+0xaf8b) [0x731f479e7a0b]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(l_Lean_IR_ToIR_lowerDecl+0x64f) [0x731f479f502f]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(lean_apply_4+0xbb7) [0x731f4b61dea7]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(l_Lean_IR_ToIR_M_run___redArg+0x89) [0x731f479d19d9]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(l_Array_forIn_x27Unsafe_loop___at___Lean_IR_toIR_spec__0+0x100) [0x731f479f60d0]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(l_Lean_IR_toIR+0x20) [0x731f479f6420]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_PassManager_run+0xe72) [0x731f47470972]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_main___lam__1+0x20) [0x731f47473b30]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_main___lam__1___boxed+0x16) [0x731f47473fe6]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(lean_apply_5+0x86a) [0x731f4b61f37a]
/home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_CompilerM_run___redArg+0x118) [0x731f474e4358]

[Eric Wieser]

Does merging master to get rc3 help?

[Pierre Quinton]

@Eric Wieser Apparently it did not.

[Cameron Zwarich]

Thankfully, I can reproduce this locally. Thanks for reporting!

[Cameron Zwarich]

The (compiler-internal) issue here is that the constructor BoundedOrder.mk got all the way to code generation while being underapplied:

[Compiler.extractClosed] size: 3
    def BddOrd.instInhabited._closed_0 : lcAny → lcAny → BoundedOrder lcAny lcAny :=
      let _x.1 := PUnit.unit;
      let _x.2 := PUnit.unit;
      let _x.3 := BoundedOrder.mk _x.2 _x.2;
      return _x.3
[Compiler.extractClosed] size: 9
    def BddOrd.instInhabited : BddOrd :=
      let _x.1 := PUnit.instCompleteAtomicBooleanAlgebra;
      cases _x.1 : BddOrd
      | CompleteBooleanAlgebra.mk toCompleteLattice le_sup_inf toHasCompl toSDiff toHImp inf_compl_le_bot top_le_sup_compl sdiff_eq himp_eq =>
        let _x.2 := CompleteLattice.toCompleteSemilatticeInf._redArg toCompleteLattice;
        cases _x.2 : BddOrd
        | CompleteSemilatticeInf.mk toPartialOrder toInfSet sInf_le le_sInf =>
          let _x.3 := PUnit.unit;
          let _x.4 := BddOrd.instInhabited._closed_0;
          let _x.5 := mk toPartialOrder _x.4;
          return _x.5

For whatever reason, this starts appearing after the elimDeadBranches pass. Disabling the pass fixes the problem.

[Cameron Zwarich]

if I were to attempt a workaround for this particular issue (although there are other failures downstream, so I don't know if the same thing will happen there), it would be to create a simpler manual Inhabited instance for BddOrd.

[Pierre Quinton]

This is certainly out of my skill set, I don't understand most of these things

[Cameron Zwarich]

I have a fix. After I make a test case and merge it I’ll try to make a workaround for your PR.

[Cameron Zwarich]

The fix was in lean4#9209. Here's the workaround:

diff --git a/Mathlib/Order/CompleteBooleanAlgebra.lean b/Mathlib/Order/CompleteBooleanAlgebra.lean
index 077496926b..f7bcecd067 100644
--- a/Mathlib/Order/CompleteBooleanAlgebra.lean
+++ b/Mathlib/Order/CompleteBooleanAlgebra.lean
@@ -823,6 +823,7 @@ namespace PUnit

 variable (s : Set PUnit.{u + 1})

+@[inline]
 instance instCompleteAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra PUnit where
   __ := PUnit.instBooleanAlgebra
   sSup _ := unit
@@ -833,6 +834,7 @@ instance instCompleteAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra PUnit w
   le_sInf _ _ _ := trivial
   iInf_iSup_eq _ := rfl

+@[inline]
 instance instCompleteBooleanAlgebra : CompleteBooleanAlgebra PUnit := inferInstance

 @[simp]

I assume that you probably want to add some sort of comment indicating that this should be removed when the fix is integrated, but I don't know the preferred format for such comments.

[Pierre Quinton]

Do we know when the fix will be released? If it is soon, then we can probably wait, this PR is not critical.

[Pierre Quinton]

Maybe we should rerun tests on this PR to see if it works?

[Eric Wieser]

You can merge master again to make that happen

[Pierre Quinton]

Oh right, sorry about that!

[Bryan Gin-ge Chen]

It looks like the toolchain mathlib is on (v4.22.0-rc3) doesn't include the fix in lean#9209 yet. Presumably it will be in the next release, but that might not come for a few weeks, depending on vacation schedules, etc.