Set `maxHeartbeats` for `Lean.Environment.unsafeRunMetaM`?

Stream: lean4

[fiforeach]

When building my project using lake build I receive the error message

PANIC at Lean.Environment.unsafeRunMetaM Lean.LibrarySuggestions.SymbolFrequency:75:24: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)

I tried setting the option maxHeartbeats in the offending file and also as an option to lean using the -D flag (by setting moreLeanArgs in the lakefile.lean), but this does not seem to increase the heartbeats allowed for whnf, which is consistently being reported as 200000.

Is it possible to increase the number of heartbeats for this operation?

When I open the file in VSCode, the file gets compiled (after a long time) without any warnings/messages appearing. Is there something different going on there or are the messages simply being suppressed?

[Jovan Gerbscheid]

You can inspect the definition of unsafeRunMetaM:

unsafe def _root_.Lean.Environment.unsafeRunMetaM [Inhabited α] (env : Environment) (x : MetaM α) : α :=
   match unsafeEIO ((((withoutExporting x).run' {} {}).run' { fileName := "symbolFrequency", fileMap := default } { env })) with
   | Except.ok a => a
   | Except.error ex => panic! match unsafeIO ex.toMessageData.toString with
     | Except.ok s => s
     | Except.error ex => ex.toString

The Core.Context that is passed into the ocmputation is { fileName := "symbolFrequency", fileMap := default }, which sets the default values

  initHeartbeats : Nat := 0
  maxHeartbeats  : Nat := getMaxHeartbeats options

In particular initHeartbeats being set to 0 is a very very bad idea, because if the initial heartbeats are actually much higher, then you will reach the maxHeartbeats much sooner, or even immediately.

You can use withCurrHeartbeats in your MetaM function to set the initHeartbeats to the current number.

[Jovan Gerbscheid]

Though I also wonder why you are using unsafeRunMetaM

[fiforeach]

Jovan Gerbscheid said:

Though I also wonder why you are using unsafeRunMetaM

Thanks a lot for the input. Sorry, I should have been more explicit about my problem. I myself am not using any metaprogramming at all. The file I have is a large file with many (mutual) inductive definitions and nothing else.

[Jovan Gerbscheid]

Aha I see. Well we'll probably need a #mwe to help further.

[fiforeach]

I am not entirely sure about the "minimality" of this example, but on my machine this gives the observed behavior:

mutual

inductive A0 where
| mk : A0
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A0

inductive A1 where
| mk : A1
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A1

inductive A2 where
| mk : A2
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A2

inductive A3 where
| mk : A3
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A3

inductive A4 where
| mk : A4
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A4

inductive A5 where
| mk : A5
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A5

inductive A6 where
| mk : A6
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A6

inductive A7 where
| mk : A7
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A7

inductive A8 where
| mk : A8
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A8

inductive A9 where
| mk : A9
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A9

inductive A10 where
| mk : A10
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A10

inductive A11 where
| mk : A11
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A11

inductive A12 where
| mk : A12
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A12

inductive A13 where
| mk : A13
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A13

inductive A14 where
| mk : A14
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A14

inductive A15 where
| mk : A15
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A15

inductive A16 where
| mk : A16
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A16

inductive A17 where
| mk : A17
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A17

inductive A18 where
| mk : A18
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A18

inductive A19 where
| mk : A19
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A19

inductive A20 where
| mk : A20
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A20

inductive A21 where
| mk : A21
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A21

inductive A22 where
| mk : A22
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A22

inductive A23 where
| mk : A23
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A23

inductive A24 where
| mk : A24
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A24

inductive A25 where
| mk : A25
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A25

inductive A26 where
| mk : A26
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A26

inductive A27 where
| mk : A27
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A27

inductive A28 where
| mk : A28
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A28

inductive A29 where
| mk : A29
| combine : A0 → A1 → A2 → A3 → A4 → A5 → A6 → A7 → A8 → A9 → A10 → A11 → A12 → A13 → A14 → A15 → A16 → A17 → A18 → A19 → A20 → A21 → A22 → A23 → A24 → A25 → A26 → A27 → A28 → A29 → A29

end

Note the following:

1. The above file compiles without increasing maxHeartbeats (but gives the aforementioned warning)
2. Using set_option maxHeartbeats does not change the warning