Performance of `interval_cases`

Stream: general

[Eric Wieser]

I was surprised to find that tactic#interval_cases struggles on intervals with more than one or two items, for instance:

import tactic.interval_cases

set_option profiler true

example (i < 5) : true := by interval_cases i; trivial  -- 985ms
example (i < 6) : true := by interval_cases i; trivial  -- 1.88s
example (i < 7) : true := by interval_cases i; trivial  -- 3.35s
example (i < 8) : true := by interval_cases i; trivial  -- 6.2s

The runtime appears to be exponential in the length of the interval!

Does this look like a deep refl causing the issue?

[Mario Carneiro]

yeah, this is a known issue. I started working on a replacement but it got delayed