chore: update stage0

This PR removes the transitional `macro_rules` for `repeat`, `while`,
and `repeat ... until` from `Init.While`. After the latest stage0
update, the `@[builtin_macro]` and `@[builtin_doElem_elab]` definitions
in `Lean.Elab.BuiltinDo.Repeat` are picked up directly, so the bootstrap
duplicates in `Init.While` are no longer needed. `Init.While` now only
provides the `Loop` type and its `ForIn` instance.

This PR also adjusts `repeat`'s `ControlInfo` to match `for ... in`: its
`numRegularExits` is now unconditionally `1` rather than `if info.breaks
then 1 else 0`. Reporting `0` when the body has no `break` causes
`inferControlInfoSeq` (in any enclosing sequence whose `ControlInfo` is
inferred — e.g. a surrounding `for`/`if`/`match`/`try` body) to stop
aggregating after the `repeat` and miss any `return`/`break`/`continue`
that follows. The corresponding elaborator then sees the actual control
flow disagree with the inferred info and throws errors like `Early
returning ... but the info said there is no early return`. The new test
in `tests/elab/newdo.lean` pins down the regression. See
[#13437](https://github.com/leanprover/lean4/pull/13437) for further
discussion.

.github/workflows/ci.yml

@@ -279,7 +279,8 @@ jobs:
                 "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
-                "check-stage3": level >= 2,
+                // Done as part of test-bench
+                //"check-stage3": level >= 2,
                 "test": true,
                 // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
                 "test-bench": large && level >= 2,
@@ -291,7 +292,8 @@ jobs:
                 "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
-                "check-stage3": level >= 2,
+                // Done as part of test-bench
+                //"check-stage3": level >= 2,
                 "test": true,
                 "secondary": true,
                 // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`

src/Init/While.lean

@@ -13,10 +13,11 @@ public section
 namespace Lean
 
 /-!
-# `while` and `repeat` loop support
+# `Loop` type backing `repeat`/`while`/`repeat ... until`
 
-The parsers for `repeat`, `while`, and `repeat ... until` are
-`@[builtin_doElem_parser]` definitions in `Lean.Parser.Do`.
+The parsers and elaborators for `repeat`, `while`, and `repeat ... until` live in
+`Lean.Parser.Do` and `Lean.Elab.BuiltinDo.Repeat`. This module only provides the
+`Loop` type (and `ForIn` instance) that those elaborators expand to.
 -/
 
 inductive Loop where
@@ -33,23 +34,4 @@ partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop
 instance [Monad m] : ForIn m Loop Unit where
   forIn := Loop.forIn
 
--- The canonical parsers for `repeat`/`while`/`repeat ... until` live in `Lean.Parser.Do`
--- as `@[builtin_doElem_parser]` definitions. We register the expansion macros here so
--- they are available to `prelude` files in `Init`, which do not import `Lean.Elab`.
-
-macro_rules
-  | `(doElem| repeat%$tk $seq) => `(doElem| for%$tk _ in Loop.mk do $seq)
-
-macro_rules
-  | `(doElem| while%$tk $h : $cond do $seq) =>
-    `(doElem| repeat%$tk if $h:ident : $cond then $seq else break)
-
-macro_rules
-  | `(doElem| while%$tk $cond do $seq) =>
-    `(doElem| repeat%$tk if $cond then $seq else break)
-
-macro_rules
-  | `(doElem| repeat%$tk $seq until $cond) =>
-    `(doElem| repeat%$tk do $seq:doSeq; if $cond then break)
-
 end Lean

src/Lean/Elab/Do/InferControlInfo.lean

@@ -139,8 +139,14 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
     }
   | `(doRepeat| repeat $bodySeq) =>
     let info ← ofSeq bodySeq
+    -- Match `for ... in` and report `numRegularExits := 1` unconditionally. Reporting `0` when
+    -- the body has no `break` causes `ofSeq` (in any enclosing sequence whose `ControlInfo` is
+    -- inferred, e.g. a surrounding `for`/`if`/`match`/`try` body) to stop aggregating after this
+    -- element and miss any `return`/`break`/`continue` that follows. The corresponding elaborator
+    -- then sees the actual control flow disagree with the inferred info and throws errors like
+    -- "Early returning ... but the info said there is no early return". See #13437 for details.
     return { info with
-      numRegularExits := if info.breaks then 1 else 0,
+      numRegularExits := 1,
       continues := false,
       breaks := false
     }

src/Lean/Elab/PreDefinition/Basic.lean

@@ -222,8 +222,8 @@ private def addNonRecAux (docCtx : LocalContext × LocalInstances) (preDef : Pre
     if compile && shouldGenCodeFor preDef then
       compileDecl decl
     if applyAttrAfterCompilation then
+      saveEqnAffectingOptions preDef.declName
       enableRealizationsForConst preDef.declName
-      generateEagerEqns preDef.declName
     addPreDefDocs docCtx preDef
     if applyAttrAfterCompilation then
       applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation

src/Lean/Elab/PreDefinition/EqUnfold.lean

@@ -28,7 +28,7 @@ def getConstUnfoldEqnFor? (declName : Name) : MetaM (Option Name) := do
     trace[ReservedNameAction] "getConstUnfoldEqnFor? {declName} failed, no unfold theorem available"
     return none
   let name := mkEqLikeNameFor (← getEnv) declName eqUnfoldThmSuffix
-  realizeConst declName name do
+  realizeConst declName name <| withEqnOptions declName do
     -- we have to call `getUnfoldEqnFor?` again to make `unfoldEqnName` available in this context
     let some unfoldEqnName ← getUnfoldEqnFor? (nonRec := true) declName | unreachable!
     let info ← getConstInfo unfoldEqnName

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -367,7 +367,7 @@ def mkEqns (declName : Name) (declNames : Array Name) : MetaM (Array Name) := do
     thmNames := thmNames.push name
     -- determinism: `type` should be independent of the environment changes since `baseName` was
     -- added
-    realizeConst declName name (doRealize name info type)
+    realizeConst declName name (withEqnOptions declName (doRealize name info type))
   return thmNames
 where
   doRealize name info type := withOptions (tactic.hygienic.set · false) do

src/Lean/Elab/PreDefinition/Mutual.lean

@@ -69,8 +69,10 @@ def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do
           a.name = `instance_reducible || a.name = `implicit_reducible do
         setIrreducibleAttribute preDef.declName
 
+  for preDef in preDefs do
+    saveEqnAffectingOptions preDef.declName
+
   /-
-  `enableRealizationsForConst` must happen before `generateEagerEqns`
   It must happen in reverse order so that constants realized as part of the first decl
   have realizations for the other ones enabled
   -/
@@ -78,7 +80,6 @@ def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do
     enableRealizationsForConst preDef.declName
 
   for preDef in preDefs do
-    generateEagerEqns preDef.declName
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
 end Lean.Elab.Mutual

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -163,7 +163,7 @@ public def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (r
 /-- Generate the "unfold" lemma for `declName`. -/
 def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
   let name := mkEqLikeNameFor (← getEnv) info.declName unfoldThmSuffix
-  realizeConst info.declNames[0]! name (doRealize name)
+  realizeConst info.declNames[0]! name (withEqnOptions declName (doRealize name))
   return name
 where
   doRealize name := withOptions (tactic.hygienic.set · false) do

src/Lean/Elab/PreDefinition/Structural/Main.lean

@@ -208,11 +208,11 @@ def structuralRecursion
         -/
         registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos fixedParamPerms
     addSmartUnfoldingDef docCtx preDef recArgPos
+  for preDef in preDefs do
+    saveEqnAffectingOptions preDef.declName
   for preDef in preDefs do
     -- must happen in separate loop so realizations can see eqnInfos of all other preDefs
     enableRealizationsForConst preDef.declName
-    -- must happen after `enableRealizationsForConst`
-    generateEagerEqns preDef.declName
   applyAttributesOf preDefsNonRec AttributeApplicationTime.afterCompilation
 
 

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -497,14 +497,21 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) :
 /--
   Searches for a metavariable `g` s.t. `tag` is its exact name.
   If none then searches for a metavariable `g` s.t. `tag` is a suffix of its name.
-  If none, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name. -/
+  If none, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name.
+
+  We erase macro scopes from the metavariable's user name before comparing, so that
+  user-written tags match even when a previous tactic left hygienic macro scopes at
+  the end of the tag (e.g. `e_a.yield._@._internal._hyg.0`, where `yield` is not the
+  literal last component of the name). Case tags written by the user are never
+  macro-scoped, so erasing scopes on the mvar side is sufficient.
+-/
 private def findTag? (mvarIds : List MVarId) (tag : Name) : TacticM (Option MVarId) := do
-  match (← mvarIds.findM? fun mvarId => return tag == (← mvarId.getDecl).userName) with
+  match (← mvarIds.findM? fun mvarId => return tag == (← mvarId.getDecl).userName.eraseMacroScopes) with
   | some mvarId => return mvarId
   | none =>
-  match (← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← mvarId.getDecl).userName) with
+  match (← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← mvarId.getDecl).userName.eraseMacroScopes) with
   | some mvarId => return mvarId
-  | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← mvarId.getDecl).userName
+  | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← mvarId.getDecl).userName.eraseMacroScopes
 
 private def getCaseGoals (tag : TSyntax ``binderIdent) : TacticM (MVarId × List MVarId) := do
   let gs ← getUnsolvedGoals

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -68,7 +68,10 @@ def setGoals (goals : List Goal) : GrindTacticM Unit :=
 
 def pruneSolvedGoals : GrindTacticM Unit := do
   let gs ← getGoals
-  let gs := gs.filter fun g => !g.inconsistent
+  let gs ← gs.filterM fun g => do
+    if g.inconsistent then return false
+    -- The metavariable may have been assigned by `isDefEq`
+    return !(← g.mvarId.isAssigned)
   setGoals gs
 
 def getUnsolvedGoals : GrindTacticM (List Goal) := do
@@ -329,13 +332,19 @@ def liftGoalM (k : GoalM α) : GrindTacticM α := do
   replaceMainGoal [goal]
   return a
 
-def liftAction (a : Action) : GrindTacticM Unit := do
+inductive LiftActionCoreResult where
+  | closed | subgoals
+
+def liftActionCore (a : Action) : GrindTacticM LiftActionCoreResult := do
   let goal ← getMainGoal
   let ka := fun _ => throwError "tactic is not applicable"
   let kp := fun goal => return .stuck [goal]
   match (← liftGrindM <| a goal ka kp) with
-  | .closed _ => replaceMainGoal []
-  | .stuck gs => replaceMainGoal gs
+  | .closed _ => replaceMainGoal []; return .closed
+  | .stuck gs => replaceMainGoal gs; return .subgoals
+
+def liftAction (a : Action) : GrindTacticM Unit := do
+  discard <| liftActionCore a
 
 def done : GrindTacticM Unit := do
   pruneSolvedGoals

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -111,7 +111,9 @@ def evalCheck (tacticName : Name) (k : GoalM Bool)
      This matches the behavior of these tactics in default tactic mode
      where `lia` can close `x > 1 → x + y + z > 0` directly. -/
   if (← read).sym then
-    liftAction <| Action.intros 0 >> Action.assertAll
+    match (← liftActionCore <| Action.intros 0 >> Action.assertAll) with
+    | .closed   => return () -- closed the goal
+    | .subgoals => pure () -- continue
   let recover := (← read).recover
   liftGoalM do
     let progress ← k

src/Lean/Meta/Eqns.lean

@@ -37,12 +37,17 @@ register_builtin_option backward.eqns.deepRecursiveSplit : Bool := {
 These options affect the generation of equational theorems in a significant way. For these, their
 value at definition time, not realization time, should matter.
 
-This is implemented by
- * eagerly realizing the equations when they are set to a non-default value
- * when realizing them lazily, reset the options to their default
+This is implemented by storing their values at definition time (when non-default) in an environment
+extension, and restoring them when the equations are lazily realized.
 -/
 def eqnAffectingOptions : Array (Lean.Option Bool) := #[backward.eqns.nonrecursive, backward.eqns.deepRecursiveSplit]
 
+/-- Environment extension that stores the values of `eqnAffectingOptions` at definition time,
+keyed by declaration name. Only populated when at least one option has a non-default value.
+Stores an association list of (option name, value) pairs for options that differ from defaults. -/
+builtin_initialize eqnOptionsExt : MapDeclarationExtension (Array (Name × DataValue)) ←
+  mkMapDeclarationExtension (asyncMode := .local)
+
 def eqnThmSuffixBase := "eq"
 def eqnThmSuffixBasePrefix := eqnThmSuffixBase ++ "_"
 def eqn1ThmSuffix := eqnThmSuffixBasePrefix ++ "1"
@@ -153,12 +158,30 @@ structure EqnsExtState where
 builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
   registerEnvExtension (pure {}) (asyncMode := .local)
 
+/--
+Runs `act` with the equation-affecting options restored to the values stored for `declName`
+at definition time (or reset to their defaults if none were stored). Use this inside
+`realizeConst` callbacks, which otherwise see the caller-independent `ctx.opts` rather than
+the outer `getEqnsFor?` context. -/
+def withEqnOptions (declName : Name) (act : MetaM α) : MetaM α := do
+  let env ← getEnv
+  let setOpts : Options → Options :=
+    if let some values := eqnOptionsExt.find? env declName then
+      fun os => Id.run do
+        let mut os := eqnAffectingOptions.foldl (fun os o => o.set os o.defValue) os
+        for (name, v) in values do
+          os := os.insert name v
+        return os
+    else
+      fun os => eqnAffectingOptions.foldl (fun os o => o.set os o.defValue) os
+  withOptions setOpts act
+
 /--
 Simple equation theorem for nonrecursive definitions.
 -/
 def mkSimpleEqThm (declName : Name) (name : Name) : MetaM (Option Name) := do
   if let some (.defnInfo info) := (← getEnv).find? declName then
-    realizeConst declName name (doRealize name info)
+    realizeConst declName name (withEqnOptions declName (doRealize name info))
     return some name
   else
     return none
@@ -229,19 +252,22 @@ private def getEqnsFor?Core (declName : Name) : MetaM (Option (Array Name)) := w
 Returns equation theorems for the given declaration.
 -/
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := withLCtx {} {} do
-  -- This is the entry point for lazy equation generation. Ignore the current value
-  -- of the options, and revert to the default.
-  withOptions (eqnAffectingOptions.foldl fun os o => o.set os o.defValue) do
+  withEqnOptions declName do
     getEqnsFor?Core declName
 
 /--
-If any equation theorem affecting option is not the default value, create the equations now.
+If any equation theorem affecting option is not the default value, store the option values
+for later use during lazy equation generation.
 -/
-def generateEagerEqns (declName : Name) : MetaM Unit := do
+def saveEqnAffectingOptions (declName : Name) : MetaM Unit := do
   let opts ← getOptions
-  if eqnAffectingOptions.any fun o => o.get opts != o.defValue then
-    trace[Elab.definition.eqns] "generating eager equations for {declName}"
-    let _ ← getEqnsFor?Core declName
+  let mut nonDefaults : Array (Name × DataValue) := #[]
+  for o in eqnAffectingOptions do
+    if o.get opts != o.defValue then
+      nonDefaults := nonDefaults.push (o.name, KVMap.Value.toDataValue (o.get opts))
+  unless nonDefaults.isEmpty do
+    trace[Elab.definition.eqns] "saving equation-affecting options for {declName}"
+    modifyEnv (eqnOptionsExt.insert · declName nonDefaults)
 
 @[expose] def GetUnfoldEqnFn := Name → MetaM (Option Name)
 

src/Lean/Meta/Tactic/Apply.lean

@@ -128,7 +128,6 @@ def postprocessAppMVars (tacticName : Name) (mvarId : MVarId) (newMVars : Array
     (synthAssignedInstances := true) (allowSynthFailures := false) : MetaM Unit := do
   synthAppInstances tacticName mvarId newMVars binderInfos synthAssignedInstances allowSynthFailures
   -- TODO: default and auto params
-  appendParentTag mvarId newMVars binderInfos
 
 private def dependsOnOthers (mvar : Expr) (otherMVars : Array Expr) : MetaM Bool :=
   otherMVars.anyM fun otherMVar => do
@@ -223,6 +222,7 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
     let e ← instantiateMVars e
     mvarId.assign (mkAppN e newMVars)
     let newMVars ← newMVars.filterM fun mvar => not <$> mvar.mvarId!.isAssigned
+    appendParentTag mvarId newMVars binderInfos
     let otherMVarIds ← getMVarsNoDelayed e
     let newMVarIds ← reorderGoals newMVars cfg.newGoals
     let otherMVarIds := otherMVarIds.filter fun mvarId => !newMVarIds.contains mvarId

src/Lean/Meta/Tactic/Rewrite.lean

@@ -82,6 +82,7 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           postprocessAppMVars `rewrite mvarId newMVars binderInfos
             (synthAssignedInstances := !tactic.skipAssignedInstances.get (← getOptions))
           let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned
+          appendParentTag mvarId newMVars binderInfos
           let otherMVarIds ← getMVarsNoDelayed heqIn
           let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·)
           let newMVarIds := newMVarIds ++ otherMVarIds

tests/bench/build/run_bench.sh

@@ -23,6 +23,8 @@ echo ">"
 echo "> Building $STAGE_NEXT..."
 echo ">"
 
+make -C "$BUILD_NEXT" clean-stdlib
+
 LAKE_OVERRIDE_LEAN=true LEAN="$(realpath fake_root/bin/lean)" \
 WRAPPER_PREFIX="$(realpath fake_root)" WRAPPER_OUT="$OUT" \
   lakeprof record -- \

tests/bench/sym/simp_1.lean

@@ -10,7 +10,9 @@ namespace SimpBench
 def getProofSize (r : Sym.Simp.Result) : MetaM Nat :=
   match r with
   | .rfl _ _ => return 0
-  | .step _ p _ _ => p.numObjs
+  | .step _ p _ _ =>
+    let p := ShareCommon.shareCommon' p
+    p.numObjs
 
 def checkWithKernel (r : Sym.Simp.Result) : MetaM Float := do
   match r with

tests/elab/1856.lean.out.expected

@@ -1,4 +1,3 @@
-case h
 α : Type ?u
 inst✝ : DecidableEq α
 i : α

tests/elab/2042.lean

@@ -2,8 +2,7 @@
   2 * a
 
 /--
-trace: case h
-x : Nat
+trace: x : Nat
 ⊢ 2 * x = x + x
 -/
 #guard_msgs in
@@ -19,8 +18,7 @@ by
   | a => 2 * a
 
 /--
-trace: case h
-x : Nat
+trace: x : Nat
 ⊢ 2 * x = x + x
 -/
 #guard_msgs in

tests/elab/apply_subgoal_name_issue.lean

@@ -0,0 +1,18 @@
+/-!
+Regression test: `case <ctor>` must keep working after `congr; ext _; cases _`
+even though the subgoal tags produced by `apply`-family tactics now inherit
+the parent tag (without appending the binder name) when only one subgoal is
+left. The case-tag matcher erases macro scopes so that `case yield` still
+matches tags like `e_a.yield._@._internal._hyg.0`.
+-/
+
+example {δ : Type} {m : Type → Type} [Monad m] [LawfulMonad m]
+    (x : m (ForInStep δ))
+    (f g : ForInStep δ → m (ForInStep δ))
+    (h : ∀ a, f a = g a) :
+    (x >>= f) = (x >>= g) := by
+  congr
+  ext step
+  cases step
+  case yield => apply h
+  case done  => apply h

tests/elab/consumePPHint.lean.out.expected

@@ -1,5 +1,4 @@
 consumePPHint.lean:8:8-8:14: warning: declaration uses `sorry`
-case a
 ⊢ q
     (have x := 0;
     x + 1)

tests/elab/convInConv.lean.out.expected

@@ -10,7 +10,6 @@ y : Nat
 | (fun x => x + y = 0) = fun x => False
 y : Nat
 | fun x => x + y = 0
-case h
 y x : Nat
 | y + x = 0
 y : Nat

tests/elab/inductionCheckAltNames.lean

@@ -10,7 +10,7 @@ axiom elimEx (motive : Nat → Nat → Sort u) (x y : Nat)
 error: Invalid alternative name `lower2`: Expected `lower`
 ---
 error: unsolved goals
-case upper.h
+case upper
 q d : Nat
 ⊢ q + d.succ > q
 ---
@@ -62,7 +62,7 @@ theorem invalidWildCard (p: Nat) : p ≤ q ∨ p > q := by
 error: Invalid alternative name `lower2`: There are no unhandled alternatives
 ---
 error: unsolved goals
-case lower.h
+case lower
 p delta✝ : Nat
 ⊢ p > p + delta✝.succ
 -/

tests/elab/meta.lean

@@ -100,7 +100,6 @@ x y : Nat
 h : x = y
 ⊢ y = x
 -----
-case h
 x y : Nat
 h : x = y
 ⊢ x = y

tests/elab/newdo.lean

@@ -489,4 +489,18 @@ example : IO Bool := do
   for (x, y) in ([] : List (Nat × Nat)) do count := count + 1
   return Float.abs count > 0
 
+-- A `repeat` (without `break`) followed by an early `return` inside an enclosing `for`. The for
+-- elaborator computes the loop body's `ControlInfo` via `inferControlInfoSeq`, which stops
+-- aggregating once it encounters an element with `numRegularExits := 0`. If `repeat` reported
+-- `numRegularExits := 0` for break-less bodies, the trailing `return 2` would be skipped during
+-- inference and the for elaborator would later throw "Early returning ... but the info said there
+-- is no early return". This test pins down that `repeat` reports `numRegularExits := 1`, matching
+-- `for ... in`.
+example : IO Nat := do
+  for _ in [1, 2] do
+    repeat
+      pure ()
+    return 2
+  return 1
+
 end Repros

tests/elab/rflTacticErrors.lean

@@ -505,28 +505,24 @@ is not definitionally equal to the right-hand side
 example : S true false  := by with_reducible apply_rfl -- Error
 /--
 error: unsolved goals
-case a
 ⊢ true = true
 -/
 #guard_msgs in
 example : S true true   := by apply_rfl -- Error (left-over goal)
 /--
 error: unsolved goals
-case a
 ⊢ true = true
 -/
 #guard_msgs in
 example : S true true   := by with_reducible apply_rfl -- Error (left-over goal)
 /--
 error: unsolved goals
-case a
 ⊢ false = true
 -/
 #guard_msgs in
 example : S false false := by apply_rfl -- Error (left-over goal)
 /--
 error: unsolved goals
-case a
 ⊢ false = true
 -/
 #guard_msgs in

tests/elab/sym_interactive_bugs.lean

@@ -0,0 +1,21 @@
+
+example (p q : Prop) : p → q → p ∧ q := by
+  sym =>
+    intro hp hq
+    apply And.intro
+    apply hp
+    apply hq
+
+register_sym_simp chainSimp where
+  post := ground >> rewrite [Nat.add_zero, Nat.zero_add]
+
+example (x y : Nat) (h : x ≤ y) : (1 - 1) + x  ≤ y + (1 + 0) := by
+  sym =>
+    simp chainSimp
+    -- In the following tactic the goal is closed while preprocessing the target
+    lia
+
+example : ∃ x, x = a := by
+  sym =>
+    apply Exists.intro
+    apply Eq.refl

tests/elab/sym_simp_3.lean

@@ -5,7 +5,7 @@ elab "sym_simp" "[" declNames:ident,* "]" : tactic => do
   let rewrite ← Sym.mkSimprocFor (← declNames.getElems.mapM fun s => realizeGlobalConstNoOverload s.raw) Sym.Simp.dischargeSimpSelf
   let methods : Sym.Simp.Methods := {
     pre  := Sym.Simp.simpControl
-    post := Sym.Simp.evalGround.andThen rewrite
+    post := Sym.Simp.evalGround >> rewrite
   }
   liftMetaTactic1 fun mvarId => Sym.SymM.run do
     let mvarId ← Sym.preprocessMVar mvarId

tests/elab_fail/conv1.lean.out.expected

@@ -9,14 +9,13 @@ x y : Nat
 case x
 x y : Nat
 ⊢ x + y = y.add x
-case a
 a b : Nat
 | foo (0 + a) (b + 0)
-case a.x
+case x
 a b : Nat
 | 0 + a
 
-case a.y
+case y
 a b : Nat
 | b + 0
 a b : Nat
@@ -55,13 +54,10 @@ x y : Nat
 ⊢ f x (x.add y) y = y + x
 x y : Nat
 | x + y
-case h.h
 a b : Nat
 | 0 + a + b
-case h.h
 a b : Nat
 | a + b
-case h.h
 a b : Nat
 | 0 + a + b
 p : Nat → Prop
@@ -83,7 +79,6 @@ x : Nat
 p : Prop
 x : Nat
 ⊢ (True → p) → p
-case h
 x : Nat
 | 0 + x
 p : Prop

tests/elab_fail/decreasing_by.lean.out.expected

@@ -19,7 +19,6 @@ n m : Nat
 n m : Nat
 ⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (dec1 n, 100) (n, m)
 decreasing_by.lean:85:0-85:22: error: unsolved goals
-case a
 n m : Nat
 ⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (n, dec2 m) (n, m)
 

tests/elab_fail/inductionErrors.lean.out.expected

@@ -1,9 +1,9 @@
 inductionErrors.lean:11:12-11:27: error: unsolved goals
-case lower.h
+case lower
 p d : Nat
 ⊢ p ≤ p + d.succ
 inductionErrors.lean:12:12-12:27: error: unsolved goals
-case upper.h
+case upper
 q d : Nat
 ⊢ q + d.succ > q
 inductionErrors.lean:16:19-16:26: error(lean.unknownIdentifier): Unknown identifier `elimEx2`

tests/elab_fail/mutwf1.lean.out.expected

@@ -1,5 +1,4 @@
 mutwf1.lean:21:2-21:6: error: unsolved goals
-case h.a
 n : Nat
 h : n ≠ 0
 ⊢ n.sub 0 ≠ 0
@@ -7,6 +6,5 @@ mutwf1.lean:31:22-31:29: error: failed to prove termination, possible solutions:
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation
   - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
-case h
 n : Nat
 ⊢ n + 1 < n

tests/server_interactive/6594.lean.out.expected

@@ -4,12 +4,11 @@
  "goals": ["case right\n⊢ True"]}
 {"textDocument": {"uri": "file:///6594.lean"},
  "position": {"line": 9, "character": 2}}
-{"rendered": "```lean\ncase a\n⊢ True ∧ True\n```",
- "goals": ["case a\n⊢ True ∧ True"]}
+{"rendered": "```lean\n⊢ True ∧ True\n```", "goals": ["⊢ True ∧ True"]}
 {"textDocument": {"uri": "file:///6594.lean"},
  "position": {"line": 13, "character": 2}}
-{"rendered": "```lean\ncase a.right\n⊢ True\n```",
- "goals": ["case a.right\n⊢ True"]}
+{"rendered": "```lean\ncase right\n⊢ True\n```",
+ "goals": ["case right\n⊢ True"]}
 {"textDocument": {"uri": "file:///6594.lean"},
  "position": {"line": 20, "character": 2}}
 {"rendered": "```lean\ncase right\n⊢ True\n```",