MonadBacktrack for CanonM

Stream: lean4

[Heather Macbeth]

I tried to do a saveState in CanonM and learned that there was no docs#Lean.MonadBacktrack instance for that monad. Is this a fundamental difficulty, or is it something which could be implemented and just hasn't been done yet?

[Daniel Weber]

import Lean.Meta.Canonicalizer

namespace Lean.Meta.Canonicalizer

instance : MonadBacktrack (State × SavedState) CanonM where
  saveState := do return (← get, ← Meta.saveState)
  restoreState b := do
    set b.1
    b.2.restore

should work, I think

[Jannis Limperg]

This will be inefficient because the CanonM State uses Std.HashMap, which is non-persistent. That is, the whole map will be copied for every snapshot.

[Mario Carneiro]

that's possibly okay if you don't snapshot too much

[Kim Morrison]

I guess one should put a note warning about this on the instance doc-string. It's a pity that hovering over save and restore can't show such doc-strings!

[Kim Morrison]

Heather, why are you trying to backtrack here in the first place. Do you actually want to backtrack the CanonM state, or only the lower layers?

[Heather Macbeth]

After seeing Jannis' warning, I indeed switched to backtracking only the MetaM layer, and this seems to work fine. (I hadn't realised I could do that.)