maxHeartbeats ignored in some cases?

Stream: general

[Valentin Robert]

I am running into an issue while modifying the SAIL RISC-V Lean output where a function definition fails. What is odd, is that the error message complains about a very small maximum number of heartbeats:

  tactic 'simp' failed, nested error:
  (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached
  Use `set_option maxHeartbeats <num>` to set the limit.

What is weird is that:

• the Lean command sets the max heartbeats to 1 million (-D maxHeartbeats=1000000),
• the Lean file starts with setting max heartbeats to 1 billion (set_option maxHeartbeats 1_000_000_000)

so I'm not sure why the max heartbeats is 200k in this error message.

The code might have other issues, and I might be able to extract a repo reproducing this issue, so it might take me a while...

In the meantime, does anyone know under what conditions this error message would not use either of my explicitly set max hearbeats?

[Aaron Liu]

maybe if they were unset for some reason

[Yury G. Kudryashov]

An #mwe would help.

[Jovan Gerbscheid]

Could it be that the limit is locally divided by 5?

[Kevin Buzzard]

I was guessing that it could be some section issue (e.g. something set in a section and gets unset when the section ends, or something like this) but I agree with Yury that this is the kind of thing where speculation is a bit of a waste of time when a #mwe would probably enable people to answer the question immediately.