Not enough heartbeats for omega?

Stream: lean4

[Ilmārs Cīrulis]

Not really a #mwe, but got this message when trying omega in some situation. (The last omega.) I copied it into https://live.lean-lang.org/ and had the same problem here.

(deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached
use `set_option maxHeartbeats <num>` to set the limit
use `set_option diagnostics true` to get diagnostic information

Does this mean something bad?

[Kim Morrison]

I'd be a little surprised if it is actually omega here, as it shouldn't spend much time inside of whnf. (But it is possible!)

A #mwe would be great.

You might also try replacing your simp with simp?, accepting the suggestion, and seeing if that solves the problem.

[Ilmārs Cīrulis]

Tried to make #mwe, for now it's only 50 lines instead of 100. Here

[Ilmārs Cīrulis]

Will poke it a bit more, maybe make it even smaller.

[Ilmārs Cīrulis]

Ok, it seems I can't make them smaller. :|

mwe2 and mwe3 is the best I have got.

[Kim Morrison]

Oh, I see. You have many disjunctions in the hypotheses. omega is extremely dumb handling branches: it tries without either branch, then when it fails it picks the first disjunction it sees and splits it and retries.

This is suitable for problems with one or two disjunctions, but omega is not suited for splitting many disjunctions.

[Kim Morrison]

For now, you will need to provide the logic yourself. Eventually we will have better tactics for this, but perhaps not until next year.

[Ilmārs Cīrulis]

Oh, nice! Now I know the explanation.

Thank you very much!