fix: progress bar in tactic combinators

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -85,8 +85,20 @@ where
         diagnostics := .empty
         stx := tac
         inner? := some { stx? := tac, task := inner.resultD default, cancelTk? }
-        finished := { stx? := tac, task := finished.resultD default, cancelTk? }
-        next := #[{ stx? := stxs, task := next.resultD default, cancelTk? }]
+        finished := {
+          stx? := tac, task := finished.resultD default, cancelTk?
+          -- Do not report range as it is identical to `inner?`'s and should not cover up
+          -- incremental reporting done in the latter.
+          reportingRange := .skip
+        }
+        next := #[{
+          stx? := stxs, task := next.resultD default, cancelTk?
+          -- Do not fall back to `inherit` if there are no more tactics as that would cover up
+          -- incremental reporting done in `inner?`. Do use default range in all other cases so that
+          -- reporting ranges are properly nested.
+          reportingRange :=
+            if stxs.getNumArgs == 0 then .skip else SnapshotTask.defaultReportingRange stxs
+        }]
       }
       -- Run `tac` in a fresh info tree state and store resulting state in snapshot for
       -- incremental reporting, then add back saved trees. Here we rely on `evalTactic`

src/Lean/Elab/Tactic/Induction.lean

@@ -364,7 +364,12 @@ where
           stx := mkNullNode altStxs
           diagnostics := .empty
           inner? := none
-          finished := { stx? := mkNullNode altStxs, reportingRange := .inherit, task := finished.resultD default, cancelTk? }
+          finished := {
+            stx? := mkNullNode altStxs, task := finished.resultD default, cancelTk?
+            -- Do not cover up progress from `next` as no significant work happens after `next` and
+            -- before `finished` is resolved.
+            reportingRange := .skip
+          }
           next := Array.zipWith
             (fun stx prom => { stx? := some stx, task := prom.resultD default, cancelTk? })
             altStxs altPromises

tests/lean/snapshotTree.lean

@@ -0,0 +1,24 @@
+/-!
+Sanity-check reported ranges for nested snapshot tree nodes. In particular, ranges of sibling nodes
+resolved later should not cover up progress inside earlier nodes.
+
+This test cannot test per se whether such cover-up occurs without a dedicated synchronization
+protocol between the test and the involved tactics to control ordering of events like in the
+cancellation tests. Instead, it is intended merely to detect timing-independent changes to the
+snapshot tree and in the event of such changes, preservation of proper progress reporting needs to
+be verified manually.
+-/
+
+set_option internal.cmdlineSnapshots false
+set_option trace.Elab.snapshotTree true
+example : True := by
+  sleep 0
+  sleep 100
+  · next =>
+    induction 0 with
+    | zero =>
+      sleep 100
+      trivial
+    | succ n =>
+      sleep 100
+      trivial

tests/lean/snapshotTree.lean.expected.out

@@ -0,0 +1,78 @@
+[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd<no range> 
+  [Elab.snapshotTree] Lean.Language.instInhabitedDynamicSnapshot⟨13, 0⟩-⟨13, 39⟩ 
+  [Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩ 
+  [Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩ 
+  [Elab.snapshotTree] Lean.Elab.Command.runLintersAsync<range inherited> 
+[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd<no range> 
+  [Elab.snapshotTree] Lean.Elab.Command.elabMutualDef⟨14, 0⟩-⟨24, 13⟩ 
+    [Elab.snapshotTree] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabHeaders⟨14, 0⟩-⟨24, 13⟩ 
+      [Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨15, 2⟩-⟨24, 13⟩ 
+        [Elab.snapshotTree] ⟨15, 2⟩-⟨15, 9⟩ 
+          [Elab.snapshotTree] <range inherited> 
+        [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+        [Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨16, 2⟩-⟨24, 13⟩ 
+          [Elab.snapshotTree] ⟨16, 2⟩-⟨16, 11⟩ 
+            [Elab.snapshotTree] <range inherited> 
+          [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+          [Elab.snapshotTree] Lean.cdot⟨17, 2⟩-⟨24, 13⟩ 
+            [Elab.snapshotTree] Lean.Parser.Tactic.«tacticNext_=>_»⟨17, 2⟩-⟨24, 13⟩ 
+              [Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval⟨17, 4⟩-⟨24, 13⟩ 
+                [Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval<no range> 
+                [Elab.snapshotTree] Lean.Parser.Tactic.induction<range inherited> 
+                  [Elab.snapshotTree] _private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo⟨18, 4⟩-⟨24, 13⟩ 
+                    [Elab.snapshotTree] _private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo<no range> 
+                    [Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨19, 4⟩-⟨21, 13⟩ 
+                      [Elab.snapshotTree] ⟨20, 6⟩-⟨20, 15⟩ 
+                        [Elab.snapshotTree] <range inherited> 
+                      [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+                      [Elab.snapshotTree] Lean.Parser.Tactic.tacticTrivial⟨21, 6⟩-⟨21, 13⟩ 
+                        [Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval⟨21, 6⟩-⟨21, 13⟩ 
+                          [Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval<no range> 
+                          [Elab.snapshotTree] Lean.Parser.Tactic.apply<range inherited> 
+                            [Elab.snapshotTree] <range inherited> 
+                              [Elab.snapshotTree] <range inherited> 
+                            [Elab.snapshotTree] <no range> 
+                            [Elab.snapshotTree] <range inherited> 
+                              [Elab.snapshotTree] <range inherited> 
+                        [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+                        [Elab.snapshotTree] <no range> 
+                          [Elab.snapshotTree] <range inherited> 
+                    [Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨22, 4⟩-⟨24, 13⟩ 
+                      [Elab.snapshotTree] ⟨23, 6⟩-⟨23, 15⟩ 
+                        [Elab.snapshotTree] <range inherited> 
+                      [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+                      [Elab.snapshotTree] Lean.Parser.Tactic.tacticTrivial⟨24, 6⟩-⟨24, 13⟩ 
+                        [Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval⟨24, 6⟩-⟨24, 13⟩ 
+                          [Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval<no range> 
+                          [Elab.snapshotTree] Lean.Parser.Tactic.apply<range inherited> 
+                            [Elab.snapshotTree] <range inherited> 
+                              [Elab.snapshotTree] <range inherited> 
+                            [Elab.snapshotTree] <no range> 
+                            [Elab.snapshotTree] <range inherited> 
+                              [Elab.snapshotTree] <range inherited> 
+                        [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+                        [Elab.snapshotTree] <no range> 
+                          [Elab.snapshotTree] <range inherited> 
+                  [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+                  [Elab.snapshotTree] <no range> 
+                    [Elab.snapshotTree] <range inherited> 
+              [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+              [Elab.snapshotTree] <no range> 
+                [Elab.snapshotTree] <range inherited> 
+            [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range> 
+            [Elab.snapshotTree] <no range> 
+              [Elab.snapshotTree] <range inherited> 
+      [Elab.snapshotTree] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabFunValues⟨14, 0⟩-⟨14, 0⟩ 
+  [Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩ 
+  [Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩ 
+  [Elab.snapshotTree] <no range> 
+  [Elab.snapshotTree] <no range> 
+  [Elab.snapshotTree] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.logGoalsAccomplishedSnapshotTask<no range> 
+      • Goals accomplished!
+
+  [Elab.snapshotTree] Lean.Elab.Command.runLintersAsync<range inherited> 
+[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd<no range> 
+  [Elab.snapshotTree] Lean.Language.instInhabitedDynamicSnapshot⟨25, 0⟩-⟨25, 0⟩ 
+  [Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩ 
+  [Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩ 
+  [Elab.snapshotTree] Lean.Elab.Command.runLintersAsync<range inherited>