Restore deletes info

Stream: lean4

[Marcus Rossel]

In the following example, I would have expected "hello" to be logged twice:

import Lean
open Lean Meta Elab Term Tactic

elab "log" s:str : tactic =>
  logInfo s.getString

elab "double_log" t:tactic : tactic => do
  let s ← saveState
  evalTactic t
  s.restore
  evalTactic t
  s.restore

example : True := by
  double_log (log "hello")

Instead, it's not logged at all. As docs#Lean.Elab.Tactic.SavedState.restore has a (restoreInfo := false) argument, I would have thought that logged info does not get restored - that is, is retained. Is there someway to retain the logged info when restoring?

[Kyle Miller]

"Info" is as in "infotrees". The messages are in a separate part of the state.

[Kyle Miller]

You could take a look at docs#Lean.Elab.withoutModifyingStateWithInfoAndMessages to see how it's implemented.

[Kyle Miller]

It modifies the saved state with the messages before restoring:

private def withoutModifyingStateWithInfoAndMessagesImpl (x : TermElabM α) : TermElabM α := do
  let saved ← saveState
  try
    withSaveInfoContext x
  finally
    let saved := { saved with meta.core.infoState := (← getInfoState), meta.core.messages := (← getThe Core.State).messages }
    restoreState saved

[Marcus Rossel]

Thanks! This works :)

import Lean
open Lean Meta Elab Term Tactic

elab "log" s:str : tactic =>
  logInfo s.getString

elab "double_log" t:tactic : tactic => do
  let mut s ← saveState
  evalTactic t
  s := { s with term.meta.core.infoState := (← getInfoState), term.meta.core.messages := (← getThe Core.State).messages }
  s.restore
  evalTactic t
  s := { s with term.meta.core.infoState := (← getInfoState), term.meta.core.messages := (← getThe Core.State).messages }
  s.restore

example : True := by
  double_log (log "hello")