feat: incremental next and tactic if (#4459)

src/Init/Tactics.lean

@@ -267,7 +267,9 @@ syntax (name := case') "case' " sepBy1(caseArg, " | ") " => " tacticSeq : tactic
 `next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with
 inaccessible names to the given names.
 -/
-macro "next " args:binderIdent* " => " tac:tacticSeq : tactic => `(tactic| case _ $args* => $tac)
+macro "next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
+  -- Limit ref variability for incrementality; see Note [Incremental Macros]
+  withRef arrowTk `(tactic| case _ $args* =>%$arrowTk $tac)
 
 /-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
 syntax (name := allGoals) "all_goals " tacticSeq : tactic

src/Init/TacticsExtra.lean

@@ -31,15 +31,19 @@ private def expandIfThenElse
       pure (hole, #[case])
   let (posHole, posCase) ← mkCase thenTk pos `(?pos)
   let (negHole, negCase) ← mkCase elseTk neg `(?neg)
-  `(tactic| (open Classical in refine%$ifTk $(← mkIf posHole negHole); $[$(posCase ++ negCase)]*))
+  `(tactic| ((open Classical in refine%$ifTk $(← mkIf posHole negHole)); $[$(posCase ++ negCase)]*))
 
 macro_rules
   | `(tactic| if%$tk $h : $c then%$ttk $pos else%$etk $neg) =>
-    expandIfThenElse tk ttk etk pos neg fun pos neg => `(if $h : $c then $pos else $neg)
+    -- Limit ref variability for incrementality; see Note [Incremental Macros]
+    withRef tk do
+      expandIfThenElse tk ttk etk pos neg fun pos neg => `(if $h : $c then $pos else $neg)
 
 macro_rules
   | `(tactic| if%$tk $c then%$ttk $pos else%$etk $neg) =>
-    expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg)
+    -- Limit ref variability for incrementality; see Note [Incremental Macros]
+    withRef tk do
+      expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg)
 
 /--
 `iterate n tac` runs `tac` exactly `n` times.

tests/lean/interactive/incrementalCombinator.lean

@@ -41,3 +41,21 @@ def spaceHave : True := by
               --^ insert: " "
               --^ collectDiagnostics
     dbg_trace "sh"
+
+-- RESET
+def next : True := by
+  next =>
+    dbg_trace "n 0"
+    dbg_trace "n 1"
+                --^ sync
+                --^ insert: ".5"
+
+-- RESET
+def if : True := by
+  if h : True then
+    dbg_trace "i 0"
+    dbg_trace "i 1"
+                --^ sync
+                --^ insert: ".5"
+  else
+    skip

tests/lean/interactive/incrementalCombinator.lean.expected.out

@@ -54,3 +54,9 @@ sh
    "fullRange":
    {"start": {"line": 1, "character": 24},
     "end": {"line": 6, "character": 18}}}]}
+n 0
+n 1
+n 1.5
+i 0
+i 1
+i 1.5

tests/lean/run/by_cases.lean

@@ -7,3 +7,14 @@ example : True := by
 example (p : Prop) : True := by
   if p then ?foo else trivial
   case foo => trivial
+
+/-! Should not accidentally leak `open Classical` into branches. -/
+
+/--
+error: failed to synthesize
+  Decidable p
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+example (p : Prop) : True := by
+  if p then exact decide p else trivial