ElabTermM and saveState

Stream: lean4 dev

[Joachim Breitner]

I want to store the state of my currentElabTermM context and resume it later. If I write

      let savedState ← saveState
      restoreState savedState

that seems to be a proper no-op, as expected. But if I saveState in two different places, and then restore them later, I get unknown free variable '.
Is saveState here not a good way of doing that?

(Sorry for begin rather vague, I should try to #mwe this issue.)

[Joachim Breitner]

Here is a #mwe that doesn’t quite reproduce the issue I am facing, but certainly demonstrates a misunderstanding on my side:

import Mathlib.Tactic.RunCmd
open Lean Elab Term Command Meta

set_option autoImplicit false

elab (name := demo) "demo" : command => liftTermElabM do
    let expr ← elabTerm (← `(term|fun x => x)) none
    let Expr.lam n d b c := expr | unreachable!
    let (body,s) ← withoutModifyingState $ withLocalDecl n c d fun x => do
        let b' := b.instantiate1 x
        check b'
        dbg_trace "Inside : {((← getLCtx).find? b'.fvarId!).isSome}"
        pure (b', ← saveState)
    -- let (_body,_s) ← withoutModifyingState $  withLocalDecl n c d fun x => do
    --     let b' := b.instantiate1 x
    --     check b'
    --     pure (b', ← saveState)
    -- variable is not available, this is expected:
    dbg_trace "Outside 1: {((← getLCtx).find? body.fvarId!).isSome}"
    check body -- shouldn't this fail, because the local decl is not available
    restoreState s
    -- variable still not available, this is unexpected
    dbg_trace "Outside 2: {((← getLCtx).find? body.fvarId!).isSome}"
    dbg_trace "{body}"

demo

The b' inside the withLocalDecl is the FVar that was introduced by withLocalDecl. It is in scope, as the dbg_trace shows.
Outside, it is no longer part of the of the environment, as expected. (Oddly, check doesn’t complain).
But after restoreSTate is it still not part of the local context. Why?

[Joachim Breitner]

Ah, saveState and restore doesn’t actually touch the MetaM Context! Does that mean that these states are not meant to be restored in a different context?

[Joachim Breitner]

So this looks like it might work; I am not sure how kosher that is:

import Mathlib.Tactic.RunCmd
open Lean Elab Term Command Meta

set_option autoImplicit false

elab (name := demo) "demo" : command => liftTermElabM do
    let expr ← elabTerm (← `(term|fun x => x)) none
    let Expr.lam n d b c := expr | unreachable!
    let (body,s,mc) ← withoutModifyingState $ withLocalDecl n c d fun x => do
        let b' := b.instantiate1 x
        check b'
        dbg_trace "Inside : {((← getLCtx).find? b'.fvarId!).isSome}"
        pure (b', ← saveState, ← readThe Meta.Context)
    -- let (_body,_s) ← withoutModifyingState $  withLocalDecl n c d fun x => do
    --     let b' := b.instantiate1 x
    --     check b'
    --     pure (b', ← saveState)
    -- variable is not available, this is expected:
    dbg_trace "Outside 1: {((← getLCtx).find? body.fvarId!).isSome}"
    check body -- shouldn't this fail, because the local decl is not available
    withTheReader Meta.Context  (fun _ => mc) $ do
      restoreState s
      -- variable still not available, this is unexpected
      dbg_trace "Outside 2: {((← getLCtx).find? body.fvarId!).isSome}"
      dbg_trace "{body}"

demo

[Jannis Limperg]

Looks okay to me, though not exactly idiomatic. I would save the LocalContext in which body is valid, rather than the MetaM.Context.

[Joachim Breitner]

Hmm, make sense, but I’d be worried about breaking invariants, e.g. between lctx and localInstances then:

structure Context where
  config            : Config               := {}
  /-- Local context -/
  lctx              : LocalContext         := {}
  /-- Local instances in `lctx`. -/
  localInstances    : LocalInstances       := #[]

[Jannis Limperg]

Ah yes, you'll need the LocalInstances as well. But withLCtx would have told you this as well.

[Jannis Limperg]

Other than that, I don't think there are any invariants attached to LocalContext; after all, withContext is an ever-popular function.

[Joachim Breitner]

Thanks! Changed accordingly.