Are commands automatically rolled back on error?

Stream: metaprogramming / tactics

[Jannis Limperg]

I'm writing a command which can throw an error after it's already modified the environment. Does anyone know if these modifications are automatically rolled back when an error occurs? Usually I would use commitIfNoEx for this, but CommandElabM doesn't seem to implement MonadBacktrack.

[Adam Topaz]

looks like the answer is no:

import Lean

open Lean Elab Command

#eval show CommandElabM Unit from do
  elabCommand <| ← `(def $(mkIdent `foo) : Nat := 37)
  throwError "Error"

#eval foo
-- 37

[Adam Topaz]

Is there any reason not to add the following instance?

instance : MonadBacktrack Command.State CommandElabM where
  saveState := get
  restoreState := set