maxHeartbeats in ContextInfo.runMetaM

Stream: lean4

[Adam Topaz]

I'm trying to run a fairly expensive computation in the MetaM monad by visiting some nodes in an infotree and using Lean.Elab.ContextInfo.runMetaM. I tried setting the maxHeartbeats to 0, but I'm still hitting deterministic timeouts. I think I must be doing something wrong in setting the maxHeartbeats option. Here is a somewhat minimal example:

import Lean

open Lean Elab Frontend

def main : IO Unit := do
  searchPathRef.set compile_time_search_path%
  unsafe enableInitializersExecution
  let input ← IO.FS.readFile ".lake/packages/mathlib/Mathlib/Algebra/Homology/Bifunctor.lean"
  let inputCtx : Lean.Parser.InputContext := Lean.Parser.mkInputContext input "<input>"
  let (header, parserState, messages) ← Lean.Parser.parseHeader inputCtx
  let options : Options := maxHeartbeats.set {} 0
  let (env, messages) ← processHeader header options messages inputCtx
  let cmdState := Command.mkState env messages options
  let cmdState := { cmdState with infoState.enabled := true }
  let s ← IO.processCommands inputCtx parserState cmdState <&> Frontend.State.commandState
  let trees := s.infoState.trees
  for tree in trees do
    tree.visitM' fun ctxInfo info _ => do
      let .ofTermInfo info := info | return
      let ctxInfo := { ctxInfo with options := maxHeartbeats.set ctxInfo.options 0 }
      ctxInfo.runMetaM info.lctx <| do
        let tp := ← Meta.inferType info.expr
        discard <| Meta.whnf tp
        println! ← getRemainingHeartbeats

(run it in a project with mathlib).
This doesn't hit a deterministic timeout, but it at least demonstrates that the remaining heartbeats is decreasing when I would expect it not to. What am I doing wrong?

[Eric Wieser]

You need to set the maxheartbeats in the core state I think; the ones in options have no effect

[Eric Wieser]

@loogle "withHeartbeats"

[loogle]

:search: Lean.withHeartbeats

[Eric Wieser]

(nevermind, I'm thinking of something else)

[Adam Topaz]

docs#Lean.Core.State

[Adam Topaz]

Where in the state?

[Adam Topaz]

Is it in docs#Lean.Core.Context maybe?

[Eric Wieser]

(deleted)

[Eric Wieser]

Adam Topaz said:

Is it in docs#Lean.Core.Context maybe?

Yes, that's what I was thinking of, thanks!

[Adam Topaz]

Should this be considered a bug in ContextInfo.runCoreM?

[Eric Wieser]

Another possible bug here is that src#ContextInfo.runCoreM does not set initHeartbeats, and so the hearbeat counter resets to zero each time

[Eric Wieser]

In fact I think this _is_ the bug, because if IO.getNumHeartbeats is greater than your limit before you even start, then you can'd do anything in CoreM

[Eric Wieser]

I have a patch somewhere fixing 5-10 "didn't propagate hearbeats" issues like this, but won't be able to find it now until after my vacation

[Adam Topaz]

That actually explains most issues I’ve been encountering. I thought I had a memory leak somewhere at some point, but I’m now quite sure it’s the bug Eric describes above.

[Adam Topaz]

In case it helps anyone else, for now I'm using the following, which works for my purposes:

namespace Lean.Elab.ContextInfo

def runCoreM' (info : ContextInfo) (x : CoreM α) : IO α := do
  let initHeartbeats ← IO.getNumHeartbeats
  Prod.fst <$> x.toIO
    { currNamespace := info.currNamespace,
      openDecls := info.openDecls,
      fileName := "<InfoTree>",
      fileMap := default,
      initHeartbeats := initHeartbeats,
      maxHeartbeats := maxHeartbeats.get info.options,
      options := info.options }
    { env := info.env, ngen := info.ngen }

def runMetaM' (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
  Prod.fst <$> info.runCoreM' (x.run { lctx := lctx } { mctx := info.mctx })

def ppGoals' (ctx : ContextInfo) (goals : List MVarId) : IO Format :=
  if goals.isEmpty then
    return "no goals"
  else
    ctx.runMetaM' {} (return Std.Format.prefixJoin "\n" (← goals.mapM (Meta.ppGoal ·)))

[Damiano Testa]

I think that Kyle recently made some of the monadic lift functions keep track of more of the available context. If I remember correctly, these changes have been merged into core, but may not have trickled down to mathlib yet.

[Damiano Testa]

Maybe lean4#5800?

[Adam Topaz]

The functions I’m using are all from core

[Damiano Testa]

Ok, besides, I don't think that the heartbeats were present in Kyle's extra context.

[Eric Wieser]

I think my diagnosis above must have been incorrect, as src#Lean.Core.CoreM.toIO sets initHeartbeats after all