aesop nontermination

Stream: lean4

[Yicheng Qian]

I'm evaluating aesop on Mathlib4, and I found that in some cases it does not terminate even with very small maxHeartbeats. This causes trouble for my evaluation.

import Mathlib.RingTheory.FiniteType

set_option maxHeartbeats 1500

theorem mem_adjoin_support.{u_1, u_2} {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddMonoid M]
  (f : AddMonoidAlgebra R M) : f ∈ Algebra.adjoin R (AddMonoidAlgebra.of' R M '' ↑f.support) := by
  aesop

Are there any ways to let aesop terminate on the above example?

[Yicheng Qian]

(deleted)

[Yicheng Qian]

The gdb stack trace seems to indicate that the process is stuck in lean_is_expr_def_eq

(gdb) thread 2
[Switching to thread 2 (Thread 0x7ffff101e640 (LWP 40964))]
#0  0x00007ffff7e5e455 in lean_alloc_small () from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
(gdb) bt 100
#0  0x00007ffff7e5e455 in lean_alloc_small () from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#1  0x00007ffff7a64760 in l_Lean_Level_hasParam ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#2  0x00007ffff7a647ae in l_Lean_Level_hasParam___boxed ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#3  0x00007ffff7e3ffa5 in lean_apply_1 () from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#4  0x00007ffff32f7789 in l_List_any___rarg () from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#5  0x00007ffff60fad2f in l_Lean_Expr_const___override ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#6  0x00007ffff7b3562a in lean::update_const(lean::expr const&, lean::list_ref<lean::level> const&) ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#7  0x00007ffff7b76fd5 in lean::instantiate_mvars_fn::visit(lean::expr const&) ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#8  0x00007ffff7b785eb in lean::instantiate_mvars_fn::visit_app_default(lean::expr const&) ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#9  0x00007ffff7b778b7 in lean::instantiate_mvars_fn::visit_app(lean::expr const&) ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#10 0x00007ffff7b77145 in lean::instantiate_mvars_fn::visit(lean::expr const&) ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#11 0x00007ffff7b78560 in lean::instantiate_mvars_fn::visit_app_default(lean::expr const&) ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#12 0x00007ffff7b778b7 in lean::instantiate_mvars_fn::visit_app(lean::expr const&) ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#13 0x00007ffff7b77145 in lean::instantiate_mvars_fn::visit(lean::expr const&) ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#14 0x00007ffff7b78560 in lean::instantiate_mvars_fn::visit_app_default(lean::expr const&) ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#15 0x00007ffff7b778b7 in lean::instantiate_mvars_fn::visit_app(lean::expr const&) ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#16 0x00007ffff7b77145 in lean::instantiate_mvars_fn::visit(lean::expr const&) ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#17 0x00007ffff7b754cd in lean_instantiate_expr_mvars ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#18 0x00007ffff7a890cb in l_Lean_instantiateExprMVars___at_Lean_instantiateMVarsCore___spec__1___rarg ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#19 0x00007ffff7a89686 in l_Lean_instantiateMVarsCore___lambda__1 ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#20 0x00007ffff7e41c76 in lean_apply_2 () from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#21 0x00007ffff3475106 in l_runST___rarg () from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#22 0x00007ffff6b7ae93 in l_Lean_instantiateMVars___at___private_Lean_Meta_Basic_0__Lean_Meta_isClassApp_x3f___spec__1 ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#23 0x00007ffff6d04033 in l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_cacheResult ()
--Type <RET> for more, q to quit, c to continue without paging--
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#24 0x00007ffff6d06115 in l_Lean_Meta_isExprDefEqAuxImpl___lambda__2 ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#25 0x00007ffff6d0d334 in l_Lean_Meta_isExprDefEqAuxImpl___lambda__3 ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#26 0x00007ffff7e47f0e in lean_apply_5 () from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#27 0x00007ffff6c2e431 in l_Lean_withTraceNodeBefore___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_checkTypesAndAssign___spec__1 ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#28 0x00007ffff6c10c85 in lean_is_expr_def_eq ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#29 0x00007ffff6c14629 in l_Std_Range_forIn_x27_loop___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqArgsFirstPass___spec__1___lambda__2
    () from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#30 0x00007ffff6c161d7 in l_Std_Range_forIn_x27_loop___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqArgsFirstPass___spec__1 ()
   from /home/indprinciples/.elan/toolchains/leanprover--lean4---v4.15.0/lib/lean/libleanshared.so
#31 0x00007ffff6c18fe4 in l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqArgsFirstPass ()

[Sebastian Ullrich]

It appears this is the case because aesop by default runs individual steps without heartbeat limits

  aesop (config := { maxSimpHeartbeats := 10000, maxRuleHeartbeats := 10000, maxUnfoldHeartbeats := 10000 })

@Jannis Limperg Shouldn't some minimum computation of global and local limit be done here?