Timeout on large pattern match

Stream: lean4

[Graham Leach-Krouse]

I'm hitting a deterministic timeout at isDefEq in the language server while trying to handle a large-ish pattern-match on Nat (about 300 cases).

1. Each clause is trivial, going directly to a constructor, something like | 243 => .em_riscv.
2. bumping maxHeartbeats to 400000 breaks through the timeout, although the language server needs to chew on it for a while.

Is this a known issue? Worth reporting on Github? This is on 4.8.0-nightly-2024-03-08.

[Kim Morrison]

I suspected that is a larger pattern match on Nat than anyone has tried before. I think if you're game to minimize it to produce a simple repro, it would be good to report.

[Mario Carneiro]

See also https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20on.20Fin.20isn't.20exhaustive.20for.20large.20matches/near/428048389

[Graham Leach-Krouse]

Thanks! Reported: https://github.com/leanprover/lean4/issues/3935