Zulip Chat Archive

Stream: general

Topic: infinite cached failure for comm_semiring S

Eric Wieser (Jan 07 2022 at 12:05):

I'm trying to debug a "fails-quickly" linter error in branch#eric-wieser/caching-failure-for-comm_semiring-S. Following the instructions there, I do an instance search with a deliberately missing [I : module Sᵐᵒᵖ M] argument, and what I get are more lines of diagnostic than fit in my clipboard. It starts off sane, as:

But then for the next 250 thousand lines:

[class_instances] cached failure for comm_semiring S

Eric Wieser (Jan 07 2022 at 12:08):

Unfortunately this is on a branch with a large refactor, so it's difficult to produce a mwe

Anne Baanen (Jan 07 2022 at 12:08):

Sounds like it's this issue appearing again

Eric Wieser (Jan 07 2022 at 12:09):

This seems different though - it doesn't even attempt any further searches, it just gets stuck in an infinite loop recording its cache

Anne Baanen (Jan 07 2022 at 12:10):

True, I guess it's more like this one

Eric Wieser (Jan 07 2022 at 12:21):

Is there any way to get some additional trace messages between the [class_instances] cached failure for comm_semiring S lines?

Anne Baanen (Jan 07 2022 at 12:23):

To see whether it's the same as the second link, trace.type_context.is_def_eq_detail true

Anne Baanen (Jan 07 2022 at 12:24):

Note: this will apparently slow down your computer by a factor 800 or so, if your setup is like mine :P

Eric Wieser (Jan 07 2022 at 12:31):

Maybe things will go better if I run it in a terminal

Eric Wieser (Jan 07 2022 at 12:36):

Yes, this seems more sustainable - maybe I'll find out if something comes after the 250k lines

Eric Wieser (Jan 07 2022 at 12:40):

Here's a bit from the beginning:

[type_context.is_def_eq_detail] [3]: _inst_1 =?= @comm_semiring.to_semiring ?x_134 ?x_136
[type_context.is_def_eq_detail] unfold right: comm_semiring.to_semiring
[type_context.is_def_eq_detail] [4]: _inst_1 =?= @semiring.mk ?x_134 (@comm_semiring.add ?x_134 ?x_136) _ (@comm_semiring.zero ?x_134 ?x_136) _ _
  (@comm_semiring.nsmul ?x_134 ?x_136)
  _
  _
  _
  (@comm_semiring.mul ?x_134 ?x_136)
  _
  _
  _
  _
  _
  (@comm_semiring.one ?x_134 ?x_136)
  _
  _
  (@comm_semiring.npow ?x_134 ?x_136)
  _
  _
[type_context.is_def_eq_detail] on failure: _inst_1 =?= @semiring.mk ?x_134 (@comm_semiring.add ?x_134 ?x_136) _ (@comm_semiring.zero ?x_134 ?x_136) _ _
  (@comm_semiring.nsmul ?x_134 ?x_136)
  _
  _
  _
  (@comm_semiring.mul ?x_134 ?x_136)
  _
  _
  _
  _
  _
  (@comm_semiring.one ?x_134 ?x_136)
  _
  _
  (@comm_semiring.npow ?x_134 ?x_136)
  _
  _
[type_context.is_def_eq_detail] unfold left&right: mul_opposite.semiring
[type_context.is_def_eq_detail] [3]: @semiring.mk ?x_2ᵐᵒᵖ
  (@non_unital_semiring.add ?x_2ᵐᵒᵖ
     (@mul_opposite.non_unital_semiring ?x_2 (@semiring.to_non_unital_semiring ?x_2 ?x_4)))
  _
  (@non_unital_semiring.zero ?x_2ᵐᵒᵖ
     (@mul_opposite.non_unital_semiring ?x_2 (@semiring.to_non_unital_semiring ?x_2 ?x_4)))
  _
  _
  (@non_unital_semiring.nsmul ?x_2ᵐᵒᵖ
     (@mul_opposite.non_unital_semiring ?x_2 (@semiring.to_non_unital_semiring ?x_2 ?x_4)))
  _
  _
  _
  (@non_unital_semiring.mul ?x_2ᵐᵒᵖ
     (@mul_opposite.non_unital_semiring ?x_2 (@semiring.to_non_unital_semiring ?x_2 ?x_4)))
  _
  _
  _
  _
  _
  (@non_assoc_semiring.one ?x_2ᵐᵒᵖ
     (@mul_opposite.non_assoc_semiring ?x_2 (@semiring.to_non_assoc_semiring ?x_2 ?x_4)))
  _
  _
  (@monoid_with_zero.npow ?x_2ᵐᵒᵖ (@mul_opposite.monoid_with_zero ?x_2 (@semiring.to_monoid_with_zero ?x_2 ?x_4)))
  _
  _ =?= @semiring.mk ?x_134ᵐᵒᵖ
  (@non_unital_semiring.add ?x_134ᵐᵒᵖ
     (@mul_opposite.non_unital_semiring ?x_134
        (@semiring.to_non_unital_semiring ?x_134 (@comm_semiring.to_semiring ?x_134 ?x_136))))
  _
  (@non_unital_semiring.zero ?x_134ᵐᵒᵖ
     (@mul_opposite.non_unital_semiring ?x_134
        (@semiring.to_non_unital_semiring ?x_134 (@comm_semiring.to_semiring ?x_134 ?x_136))))
  _
  _
  (@non_unital_semiring.nsmul ?x_134ᵐᵒᵖ
     (@mul_opposite.non_unital_semiring ?x_134
        (@semiring.to_non_unital_semiring ?x_134 (@comm_semiring.to_semiring ?x_134 ?x_136))))
  _
  _
  _
  (@non_unital_semiring.mul ?x_134ᵐᵒᵖ
     (@mul_opposite.non_unital_semiring ?x_134
        (@semiring.to_non_unital_semiring ?x_134 (@comm_semiring.to_semiring ?x_134 ?x_136))))
  _
  _
  _
  _
  _
  (@non_assoc_semiring.one ?x_134ᵐᵒᵖ
     (@mul_opposite.non_assoc_semiring ?x_134
        (@semiring.to_non_assoc_semiring ?x_134 (@comm_semiring.to_semiring ?x_134 ?x_136))))
  _
  _
  (@monoid_with_zero.npow ?x_134ᵐᵒᵖ
     (@mul_opposite.monoid_with_zero ?x_134
        (@semiring.to_monoid_with_zero ?x_134 (@comm_semiring.to_semiring ?x_134 ?x_136))))
  _
  _
[type_context.is_def_eq_detail] [4]: semiring.mk =?= semiring.mk
[type_context.is_def_eq_detail] [4]: @non_unital_semiring.add ?x_2ᵐᵒᵖ
  (@mul_opposite.non_unital_semiring ?x_2 (@semiring.to_non_unital_semiring ?x_2 ?x_4)) =?= @non_unital_semiring.add ?x_134ᵐᵒᵖ
  (@mul_opposite.non_unital_semiring ?x_134
     (@semiring.to_non_unital_semiring ?x_134 (@comm_semiring.to_semiring ?x_134 ?x_136)))
[class_instances] cached failure for comm_semiring S
[type_context.is_def_eq_detail] [5]: @mul_opposite.non_unital_semiring S (@semiring.to_non_unital_semiring S _inst_1) =?= @mul_opposite.non_unital_semiring S (@semiring.to_non_unital_semiring S (@comm_semiring.to_semiring S ?x_136))
[class_instances] cached failure for comm_semiring S
[type_context.is_def_eq_detail] [6]: @semiring.to_non_unital_semiring S _inst_1 =?= @semiring.to_non_unital_semiring S (@comm_semiring.to_semiring S ?x_136)
[class_instances] cached failure for comm_semiring S
[type_context.is_def_eq_detail] [7]: _inst_1 =?= @comm_semiring.to_semiring S ?x_136
[type_context.is_def_eq_detail] unfold right: comm_semiring.to_semiring
[type_context.is_def_eq_detail] [8]: _inst_1 =?= @semiring.mk S (@comm_semiring.add S ?x_136) _ (@comm_semiring.zero S ?x_136) _ _ (@comm_semiring.nsmul S ?x_136) _ _ _
  (@comm_semiring.mul S ?x_136)
  _
  _
  _
  _
  _
  (@comm_semiring.one S ?x_136)
  _
  _
  (@comm_semiring.npow S ?x_136)
  _
  _
[type_context.is_def_eq_detail] on failure: _inst_1 =?= @semiring.mk S (@comm_semiring.add S ?x_136) _ (@comm_semiring.zero S ?x_136) _ _ (@comm_semiring.nsmul S ?x_136) _ _ _
  (@comm_semiring.mul S ?x_136)
  _
  _
  _
  _
  _
  (@comm_semiring.one S ?x_136)
  _
  _
  (@comm_semiring.npow S ?x_136)
  _
  _
[type_context.is_def_eq_detail] unfold left&right: semiring.to_non_unital_semiring
[type_context.is_def_eq_detail] [7]: @non_unital_semiring.mk S (@semiring.add S _inst_1) _ (@semiring.zero S _inst_1) _ _ (@semiring.nsmul S _inst_1) _ _ _
  (@semiring.mul S _inst_1)
  _
  _
  _
  _
  _ =?= @non_unital_semiring.mk S (@semiring.add S (@comm_semiring.to_semiring S ?x_136)) _
  (@semiring.zero S (@comm_semiring.to_semiring S ?x_136))
  _
  _
  (@semiring.nsmul S (@comm_semiring.to_semiring S ?x_136))
  _
  _
  _
  (@semiring.mul S (@comm_semiring.to_semiring S ?x_136))
  _
  _
  _
  _
  _
[type_context.is_def_eq_detail] [8]: @semiring.add S _inst_1 =?= @semiring.add S (@comm_semiring.to_semiring S ?x_136)
[class_instances] cached failure for comm_semiring S
[type_context.is_def_eq_detail] [9]: _inst_1 =?= @comm_semiring.to_semiring S ?x_136
[type_context.is_def_eq_detail] unfold right: comm_semiring.to_semiring
[type_context.is_def_eq_detail] [10]: _inst_1 =?= @semiring.mk S (@comm_semiring.add S ?x_136) _ (@comm_semiring.zero S ?x_136) _ _ (@comm_semiring.nsmul S ?x_136) _ _ _
  (@comm_semiring.mul S ?x_136)
  _
  _
  _
  _
  _
  (@comm_semiring.one S ?x_136)
  _
  _
  (@comm_semiring.npow S ?x_136)
  _
  _
[type_context.is_def_eq_detail] on failure: _inst_1 =?= @semiring.mk S (@comm_semiring.add S ?x_136) _ (@comm_semiring.zero S ?x_136) _ _ (@comm_semiring.nsmul S ?x_136) _ _ _
  (@comm_semiring.mul S ?x_136)
  _
  _
  _
  _
  _
  (@comm_semiring.one S ?x_136)
  _
  _
  (@comm_semiring.npow S ?x_136)
  _
  _
[type_context.is_def_eq_detail] [9]: @semiring.add S _inst_1 =?= @comm_semiring.add S ?x_136
[type_context.is_def_eq_detail] [10]: semiring.add =?= comm_semiring.add
[type_context.is_def_eq_detail] on failure: semiring.add =?= comm_semiring.add
[type_context.is_def_eq_detail] on failure: @semiring.add S _inst_1 =?= @comm_semiring.add S ?x_136
[class_instances] cached failure for comm_semiring S
[type_context.is_def_eq_detail] on failure: @non_unital_semiring.mk S (@semiring.add S _inst_1) _ (@semiring.zero S _inst_1) _ _ (@semiring.nsmul S _inst_1) _ _ _
  (@semiring.mul S _inst_1)
  _
  _
  _
  _
  _ =?= @non_unital_semiring.mk S (@semiring.add S (@comm_semiring.to_semiring S ?x_136)) _
  (@semiring.zero S (@comm_semiring.to_semiring S ?x_136))
  _
  _
  (@semiring.nsmul S (@comm_semiring.to_semiring S ?x_136))
  _
  _
  _
  (@semiring.mul S (@comm_semiring.to_semiring S ?x_136))
  _
  _
  _
  _
  _

Eric Wieser (Jan 07 2022 at 12:40):

Indeed, this looks more like exponential blow-up than an infinite loop, there's no obvious fixed period of repetition

Eric Wieser (May 06 2022 at 11:21):

I've updated the description of #10716 with an example of where the timeout does and does not occur

Eric Wieser (May 06 2022 at 11:24):

The timeout disappears if I add

attribute [irreducible] mul_opposite.add_comm_monoid

Eric Wieser (May 06 2022 at 11:40):

Apparently this is the fix:

 instance [semiring α] : semiring αᵐᵒᵖ :=
-{ .. mul_opposite.non_unital_semiring α, .. mul_opposite.non_assoc_semiring α,
+{ one := 1,
+  zero := 0,
+  add := (+),
+  mul := (*),
+  .. mul_opposite.non_unital_semiring α, .. mul_opposite.non_assoc_semiring α,
   .. mul_opposite.monoid_with_zero α }

Eric Wieser (May 06 2022 at 11:40):

Should .. just be defined to mean this automatically?

Eric Rodriguez (May 06 2022 at 11:41):

what's the difference? I thought this was how .. was defined

Eric Wieser (May 06 2022 at 11:43):

The one := 1 version uses opposite.has_one, the ..-only version uses mul_one_class.to_has_one $ ... $ non_unital_semiring.to_non_unital_non_assoc_semiring $ mul_opposite.non_unital_semiring

Eric Wieser (May 06 2022 at 11:43):

Basically, I'm suggesting that .. should unfold all reducible definitions

Eric Wieser (May 06 2022 at 11:45):

Or alternative, we need a tactic by reduced foo which basically amounts to

begin
   have :=  foo,
   dsimp only at this,  -- or whatever the right level of "unfold reducible things" is
   exact this
end

Scott Morrison (May 06 2022 at 12:54):

@Eric Wieser, hopefully dsimp_result { exact foo } already does this.

Scott Morrison (May 06 2022 at 12:54):

You can pass the usual dsimp arguments to dsimp_result. There is also simp_result.

Scott Morrison (May 06 2022 at 12:54):

Neither have been battle-tested much!

Eric Wieser (May 06 2022 at 12:54):

docs#tactic.interactive.dsimp_result

Scott Morrison (May 06 2022 at 12:55):

I think they have only been used inside other tactic implementations to date, not out in the wild. :-)

Last updated: Dec 20 2023 at 11:08 UTC