From 3dacd0549edad7bb966cb28766d82eafbaa54d05 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 10 Dec 2025 08:28:38 +0000 Subject: [PATCH] fix: progress bar in tactic combinators --- src/Lean/Elab/Tactic/BuiltinTactic.lean | 16 ++++- src/Lean/Elab/Tactic/Induction.lean | 7 +- tests/lean/snapshotTree.lean | 24 +++++++ tests/lean/snapshotTree.lean.expected.out | 78 +++++++++++++++++++++++ 4 files changed, 122 insertions(+), 3 deletions(-) create mode 100644 tests/lean/snapshotTree.lean create mode 100644 tests/lean/snapshotTree.lean.expected.out diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index 0e29155af3c9..ab4a4767aed7 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/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` diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 4273c2a8e98c..59112e09a2f4 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/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 diff --git a/tests/lean/snapshotTree.lean b/tests/lean/snapshotTree.lean new file mode 100644 index 000000000000..f58640f08ac5 --- /dev/null +++ b/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 diff --git a/tests/lean/snapshotTree.lean.expected.out b/tests/lean/snapshotTree.lean.expected.out new file mode 100644 index 000000000000..ae3e9c54bd98 --- /dev/null +++ b/tests/lean/snapshotTree.lean.expected.out @@ -0,0 +1,78 @@ +[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd + [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 +[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd + [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] + [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven + [Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨16, 2⟩-⟨24, 13⟩ + [Elab.snapshotTree] ⟨16, 2⟩-⟨16, 11⟩ + [Elab.snapshotTree] + [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven + [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 + [Elab.snapshotTree] Lean.Parser.Tactic.induction + [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 + [Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨19, 4⟩-⟨21, 13⟩ + [Elab.snapshotTree] ⟨20, 6⟩-⟨20, 15⟩ + [Elab.snapshotTree] + [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven + [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 + [Elab.snapshotTree] Lean.Parser.Tactic.apply + [Elab.snapshotTree] + [Elab.snapshotTree] + [Elab.snapshotTree] + [Elab.snapshotTree] + [Elab.snapshotTree] + [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven + [Elab.snapshotTree] + [Elab.snapshotTree] + [Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨22, 4⟩-⟨24, 13⟩ + [Elab.snapshotTree] ⟨23, 6⟩-⟨23, 15⟩ + [Elab.snapshotTree] + [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven + [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 + [Elab.snapshotTree] Lean.Parser.Tactic.apply + [Elab.snapshotTree] + [Elab.snapshotTree] + [Elab.snapshotTree] + [Elab.snapshotTree] + [Elab.snapshotTree] + [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven + [Elab.snapshotTree] + [Elab.snapshotTree] + [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven + [Elab.snapshotTree] + [Elab.snapshotTree] + [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven + [Elab.snapshotTree] + [Elab.snapshotTree] + [Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven + [Elab.snapshotTree] + [Elab.snapshotTree] + [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] + [Elab.snapshotTree] + [Elab.snapshotTree] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.logGoalsAccomplishedSnapshotTask + • Goals accomplished! + + [Elab.snapshotTree] Lean.Elab.Command.runLintersAsync +[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd + [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