port Data.Set.Intervals.Instances

Stream: mathlib4

[Moritz Firsching]

In mathlib4#1068, the only thing not working is the the instancecancelCommMonoid; currently giving a time-out. In similar situations, this way of defining an instance works.
Is there any easy fix?

instance cancelCommMonoid {α : Type _} [StrictOrderedCommRing α] [IsDomain α] :
    CancelCommMonoid (Ioc (0 : α) 1) :=
  { Set.Ioc.cancelMonoid, Set.Ioc.commMonoid with }
#align set.Ioc.cancel_comm_monoid Set.Ioc.cancelCommMonoid

[Heather Macbeth]

Have you merged master in the last hour or two, since the fix for the other looping instance came in?

[Heather Macbeth]

Since mathlib4#1335 that is

[Moritz Firsching]

I have now rebased on current head, but still get the timeout

[Maxwell Thum]

It seems to work fine with set_option maxHeartbeats 300000.

[Maxwell Thum]

Is this too long?

[Kevin Buzzard]

It's an indication that there's been a regression which we might want to look into now