Tactic.SavedState.restore

Stream: lean4

[Marcus Rossel]

The result of calling Tactic.SavedState.restore is different depending on how variables were introduced into the local context:

import Lean
open Lean Meta Elab Tactic

elab "ex" : tactic => do
  let t ← getMainTarget
  let s ← saveState
  evalTactic <| ← `(tactic|simp only [Nat.zero_add])
  s.restore
  logInfo <| ← ppExpr t

example (a b : Nat) : 0 + a = b := by
  ex -- 0 + a = b

example : ∀ (a b : Nat), 0 + a = b := by
  intro a b
  ex -- 0 + _uniq.2298 = _uniq.2301

How can I restore the correct context in the second example?

[Siddhartha Gadgil]

I would guess that you need to also restore the Core, Meta and Elabstates.

[Kyle Miller]

When you see _uniq.1234 variables, that indicates that you have the wrong local context in the current state -- this is how fvars are pretty printed if the local context is wrong.

Since you're working with the main goal, you could do this:

elab "ex" : tactic => withMainContext do
  let t ← getMainTarget
  let s ← saveState
  evalTactic <| ← `(tactic|simp only [Nat.zero_add])
  s.restore
  logInfo <| ← ppExpr t

[Kyle Miller]

Also, no need to do ppExpr yourself if you use m! message strings.

logInfo m!"{t}"

[Eric Wieser]

Siddhartha Gadgil said:

I would guess that you need to also restore the Core, Meta and Elabstates.

These are already included in docs#Tactic.SavedState

[Kyle Miller]

By the way, there's a combinator wrapping up saveState/restoreState:

  withoutModifyingState do
    evalTactic <| ← `(tactic|simp only [Nat.zero_add])

[Eric Wieser]

@Kyle Miller, how is the wrong local context showing up in the original version? Is it not being restored correctly with the rest of the state?

[Kyle Miller]

That's a good question, and I'm not sure. The local context is part of the reader state, so I thought it wasn't supposed to be modifiable.

[Kyle Miller]

I know though that in a tactic you can't count on the local context being set to anything sensible.

[Jannis Limperg]

The restoreState is a red herring:

import Lean
open Lean Meta Elab Tactic

elab "ex" : tactic => do
  let t ← getMainTarget
  logInfo <| ← ppExpr t

example (a b : Nat) : 0 + a = b := by
  ex -- 0 + a = b

example : ∀ (a b : Nat), 0 + a = b := by
  intro a b
  ex -- 0 + _uniq.924 = _uniq.927

The real issue is that in both examples, the local context in which ex is run is that of the initial goal. But in the second example, the printed expression lives in the local context of the goal produced by intro a b.

In general, as Kyle says, the local context is not mutable and is therefore not part of the SavedState that gets saved by saveState and restored by restoreState.

[Patrick Massot]

To be clear, the normal way to fix Jannis' example is

elab "ex" : tactic => do
  let t ← getMainTarget
  withMainContext do
  logInfo <| ← ppExpr t