Setting maxHeartbeats as a lake flag

Stream: lean4

[Adam Topaz]

I have a file with main : IO Unit which essentially obtains an environment from some file and uses it with docs#Lean.Elab.ContextInfo.runMetaM to execute some run : MetaM Unit. I am trying to run this with lake env lean --run filename.lean, but I'm exceeding the heartbeat limit. I know for a fact that running run with #eval run works if I set the max heartbeats to 0, but I don't know how to set this option in the command line with lake. I'm sure it's easy to do, I just don't know the right flag the use. Any hints?

[Mario Carneiro]

looks like you should be able to set maxHeartbeats inside the ContextInfo you pass to that function

[Adam Topaz]

you mean by manually setting options := ...?

[Mario Carneiro]

import Lean
open Lean Elab
example {α} (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
  let info := {info with options := Core.maxHeartbeats.set info.options 0 }
  info.runMetaM lctx x

[Adam Topaz]

Thanks Mario!