InfoTrees in FrontendM

Stream: lean4

[Adam Topaz]

I have some code which extracts infotrees from an elaborated Lean file and processes them in some way. A minimal version of this code is here:

import Lean

open Lean Elab Frontend

unsafe
def main (args : List String) : IO Unit := do
  let path : System.FilePath := args[0]!
  initSearchPath (← findSysroot)
  enableInitializersExecution
  let inputCtx : Parser.InputContext := Parser.mkInputContext (← IO.FS.readFile path) "<input>"
  let (header, parserState, messages) ← Parser.parseHeader inputCtx
  let (env, messages) ← processHeader header {} messages inputCtx
  let commandState := { Command.mkState env messages {} with infoState.enabled := true }
  go.run { inputCtx } |>.run' { commandState, parserState, cmdPos := parserState.pos }
where go : Elab.Frontend.FrontendM Unit := do
  processCommands
  println! (← get).commandState.infoState.trees.size

When I run this as lake exe foo Test.lean with the contents of Test.lean being

example (a b : Nat) : a + b = b + a := by
  rw [Nat.add_comm]

I get 2 as the output, which is what I expect, if I run this in leanprover/lean4:v4.24.0. When using leanprover/lean4:v4.25.0-rc2, I end up with 1 (just the elabEoi infotree). I couldn't find anything in the release notes that would indicate this change in behavior, but it's possible I didn't look hard enough. Is this a bug, or is there a different way to obtain the infotrees after elaboration in FrontendM?

[Kim Morrison]

Is the change of behavior specific to example (rather than theorem)?

[Adam Topaz]

It's not specific to example, the same happens with theorem. What seems to happen in 4.25.0 is that CommandState.infoState.trees is a singleton after every processCommand step, where the infotree is only the one obtained from elaborating the last command. Here's a standalone code block if anyone wants to test:

import Lean

open Lean Elab Frontend

def file : String := "\
theorem foo (a b : Nat) : a + b = b + a := by
  rw [Nat.add_comm]
"

unsafe
def main : IO Unit := do
  initSearchPath (← findSysroot)
  enableInitializersExecution
  let inputCtx : Parser.InputContext := Parser.mkInputContext file "<input>"
  let (header, parserState, messages) ← Parser.parseHeader inputCtx
  let (env, messages) ← processHeader header {} messages inputCtx
  let commandState := { Command.mkState env messages {} with infoState.enabled := true }
  go.run { inputCtx } |>.run' { commandState, parserState, cmdPos := parserState.pos }
where go : Elab.Frontend.FrontendM Unit := do
  processCommands
  println! (← get).commandState.infoState.trees.size

#eval main

[Thomas Murrills]

Aha, it looks like this recent commit which changed elabCommandTopLevel is responsible! It seems that the new behavior is intentional, and not a bug.

perf: reset InfoState.lazyAssignment before each command (#10744)

This PR fixes a performance regression introduced in #10518. More generally, it ensures both message log and info state are per-command, which has been the case in practice ever since the asynchronous language driver was introduced.

[Adam Topaz]

Great find! Okay, so it seems that indeed I will have to get the infotree after every invokation of processCommand.

[Adam Topaz]

Given this change, it is a bit strange though that InfoState.trees is of type PersistentArray InfoTree and not just InfoTree (or Option InfoTree.

[Kim Morrison]

Does a mutual block return multiple InfoTrees?