mathport fails after mathlib4 update

Stream: mathlib4

[Gabriel Ebner]

These are the changes: https://github.com/leanprover-community/mathlib4/compare/6d86a6ac7aa6eae79181b6bae1fca53be16d2379..090a8a08255671e5d06f2b22131421871f2b373f

[Gabriel Ebner]

Not yet sure what's going on here. After the update mathport takes about two hours and fails in data.polynomial.mirror https://github.com/leanprover-community/mathport/actions/runs/3913731949/jobs/6689971655

[Eric Wieser]

Are we sure this is due to mathlib4 and not mathlib3?

[Gabriel Ebner]

We update mathlib4 12x more frequently than mathlib3. There was no mathlib3 update between the succeeding and failing mathport runs.

[Gabriel Ebner]

Looks like checking the definition in the kernel takes forever. Unfortunately we can't set a timeout, because the timeout is reported as an uncatchable C++ exception. https://github.com/leanprover/lean4/pull/2036

[Johan Commelin]

@Gabriel Ebner Is there anything that stands out to you?

[Johan Commelin]

I wouldn't know where to start looking for an issue. Is it worth bisecting the failure, to see which of these files exactly is causing a problem?

[Gabriel Ebner]

With the dubious translations, I expect this failure mode to occur again sooner or later.

[Johan Commelin]

Aha, so you think it might be an issue of a missing ₓ?

[Eric Wieser]

How was this resolved last time? It seems to be happening again.

The mathport CI is giving the error

Failed to port { package := "Mathbin", mod3 := `ring_theory.subring.basic }

(edit: filed as https://github.com/leanprover-community/mathport/issues/228 to link things on github)

[Eric Wieser]

this run seems to be the first one to have failed.

[Eric Wieser]

It looks like !4#1945 was the change that broke it, based on the timing and https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/subring/basic

[Gabriel Ebner]

These are the last few lines in the output:

[apply] <decl:subring.gi>
[addDecl] START REFINE ring_theory.subring.basic subring.gi
[refineDef] Subring.gi
[translateName] subring.gi -> Subring.gi
[addDecl] FOUND DUBIOUS ring_theory.subring.basic Subring.gi
[apply] position subring.gi
[apply] protected
[apply] <decl:subring.gi.equations._eqn_1>
[addDecl] START REFINE ring_theory.subring.basic subring.gi.equations._eqn_1
[refineThm] Subring.gi.equations._eqn_1
[translateName] subring.gi.equations._eqn_1 -> Subring.gi.equations._eqn_1
[addDecl] START CHECK  ring_theory.subring.basic Subring.gi.equations._eqn_1
[kernel] skipping proof of theorem
[addDecl] stubbing value of Subring.gi.equations._eqn_1
[addDecl] stubbing type of Subring.gi.equations._eqn_1
[addDecl] END CHECK    ring_theory.subring.basic Subring.gi.equations._eqn_1
[apply] position subring.gi.equations._eqn_1
[apply] <decl:subring.closure_eq>
[addDecl] START REFINE ring_theory.subring.basic subring.closure_eq
[refineThm] Subring.closure_eq

[Gabriel Ebner]

And a stacktrace:

#115 0x000000000377609d in lean::type_checker::lazy_delta_reduction_step(lean::expr&, lean::expr&) ()
#116 0x0000000003776d2b in lean::type_checker::lazy_delta_reduction(lean::expr&, lean::expr&) ()
#117 0x0000000003776919 in lean::type_checker::is_def_eq_core(lean::expr const&, lean::expr const&) ()
#118 0x0000000003776ac0 in lean::type_checker::is_def_eq_core(lean::expr const&, lean::expr const&) ()
#119 0x0000000003775006 in lean::type_checker::is_def_eq_app(lean::expr const&, lean::expr const&) ()
#120 0x0000000003776aee in lean::type_checker::is_def_eq_core(lean::expr const&, lean::expr const&) ()
#121 0x0000000003774117 in lean::type_checker::is_def_eq_binding(lean::expr, lean::expr) ()
#122 0x0000000003774458 in lean::type_checker::quick_is_def_eq(lean::expr const&, lean::expr const&, bool) ()
#123 0x00000000037767d6 in lean::type_checker::is_def_eq_core(lean::expr const&, lean::expr const&) ()
#124 0x00000000037792d8 in std::__1::__function::__func<lean_kernel_is_def_eq::$_4, std::__1::allocator<lean_kernel_is_def_eq::$_4>, lean_object* ()>::operator()() ()
#125 0x000000000377b764 in lean_object* lean::catch_kernel_exceptions<lean_object*>(std::__1::function<lean_object* ()> const&) ()
#126 0x0000000003777f82 in lean_kernel_is_def_eq ()
#127 0x00000000011fd3f0 in l_Mathport_Binary_refineLean4Names_isDefEqUpto___lambda__1 ()
#128 0x00000000011fd9e4 in l_Mathport_Binary_refineLean4Names_isDefEqUpto ()
#129 0x0000000001201f85 in l_Mathport_Binary_refineLean4Names_refineThm ()
#130 0x0000000001214f6b in l_Mathport_Binary_refineLean4NamesAndUpdateMap ()
#131 0x00000000015681f8 in l_Mathport_Binary_refineAddDecl ()
#132 0x000000000158287f in l_Mathport_Binary_applyTheoremVal ()
#133 0x00000000015bfeef in l_Array_forInUnsafe_loop___at_Mathport_binport1___spec__1 ()
#134 0x00000000015c0975 in l_Mathport_binport1 ()

[Gabriel Ebner]

i.e., an effectively infinite loop in the kernel defeq function

[Eric Wieser]

While parsing docs4#Subring.closure_eq / docs#subring.closure_eq, right?

[Gabriel Ebner]

Yes.

[Gabriel Ebner]

https://github.com/leanprover-community/mathport/commit/b515f2fb449110ef1010041691f43437c05ebd34