fix: repeat' should roll back the state (leanprover-community#305)

* fix: `repeat'` should roll back the state

* use repeat1' in repeat1

* rename repeat1 to repeat1'

Std/Lean/Meta/Basic.lean

@@ -350,7 +350,7 @@ or until `maxIters` total calls to `f` have occurred.
 Returns a boolean indicating whether `f` succeeded at least once, and
 all the remaining goals (i.e. those on which `f` failed).
 -/
-def repeat'Core [Monad m] [MonadError m] [MonadMCtx m]
+def repeat'Core [Monad m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m]
     (f : MVarId → m (List MVarId)) (gs : List MVarId) (maxIters := 100000) :
     m (Bool × List MVarId) := do
   let (progress, acc) ← go maxIters false gs [] #[]
@@ -369,9 +369,9 @@ where
       match n with
       | 0 => pure <| (p, acc.push g ++ gs |> stk.foldl .appendList)
       | n+1 =>
-        match ← observing (f g) with
-        | .ok gs' => go n true gs' (gs::stk) acc
-        | .error _ => go n p gs stk (acc.push g)
+        match ← observing? (f g) with
+        | some gs' => go n true gs' (gs::stk) acc
+        | none => go n p gs stk (acc.push g)
 termination_by _ n p gs stk _ => (n, stk, gs)
 
 /--
@@ -380,7 +380,7 @@ then runs `f` again on all of those goals, and repeats until `f` fails on all re
 or until `maxIters` total calls to `f` have occurred.
 Always succeeds (returning the original goals if `f` fails on all of them).
 -/
-def repeat' [Monad m] [MonadError m] [MonadMCtx m]
+def repeat' [Monad m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m]
     (f : MVarId → m (List MVarId)) (gs : List MVarId) (maxIters := 100000) : m (List MVarId) :=
   repeat'Core f gs maxIters <&> (·.2)
 
@@ -390,7 +390,7 @@ then runs `f` again on all of those goals, and repeats until `f` fails on all re
 or until `maxIters` total calls to `f` have occurred.
 Fails if `f` does not succeed at least once.
 -/
-def repeat1' [Monad m] [MonadError m] [MonadMCtx m]
+def repeat1' [Monad m] [MonadError m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m]
     (f : MVarId → m (List MVarId)) (gs : List MVarId) (maxIters := 100000) : m (List MVarId) := do
   let (.true, gs) ← repeat'Core f gs maxIters | throwError "repeat1' made no progress"
   pure gs

Std/Tactic/Basic.lean

@@ -105,10 +105,11 @@ elab "repeat' " tac:tacticSeq : tactic => do
   setGoals (← repeat' (evalTacticAtRaw tac) (← getGoals))
 
 /--
-`repeat1 tac` applies `tac` to main goal at least once. If the application succeeds,
+`repeat1' tac` applies `tac` to main goal at least once. If the application succeeds,
 the tactic is applied recursively to the generated subgoals until it eventually fails.
 -/
-macro "repeat1 " tac:tacticSeq : tactic => `(tactic| focus (($tac); repeat' $tac))
+elab "repeat1' " tac:tacticSeq : tactic => do
+  setGoals (← repeat1' (evalTacticAtRaw tac) (← getGoals))
 
 /-- `subst_eqs` applies `subst` to all equalities in the context as long as it makes progress. -/
 elab "subst_eqs" : tactic => Elab.Tactic.liftMetaTactic1 (·.substEqs)

test/repeat.lean

@@ -0,0 +1,13 @@
+import Std.Tactic.Basic
+import Std.Tactic.GuardMsgs
+
+open Lean Elab Tactic Meta
+
+elab "foo" : tactic => liftMetaTactic fun g => do
+  g.assign (← mkFreshExprMVar (← g.getType))
+  throwError ""
+
+#guard_msgs in
+example : True := by
+  repeat' foo
+  trivial