Skip to content

Commit 3dacd05

Browse files
KhaKha
committed
fix: progress bar in tactic combinators
1 parent 455fd0b commit 3dacd05

File tree

4 files changed

+122
-3
lines changed

4 files changed

+122
-3
lines changed

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

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -85,8 +85,20 @@ where
8585
diagnostics := .empty
8686
stx := tac
8787
inner? := some { stx? := tac, task := inner.resultD default, cancelTk? }
88-
finished := { stx? := tac, task := finished.resultD default, cancelTk? }
89-
next := #[{ stx? := stxs, task := next.resultD default, cancelTk? }]
88+
finished := {
89+
stx? := tac, task := finished.resultD default, cancelTk?
90+
-- Do not report range as it is identical to `inner?`'s and should not cover up
91+
-- incremental reporting done in the latter.
92+
reportingRange := .skip
93+
}
94+
next := #[{
95+
stx? := stxs, task := next.resultD default, cancelTk?
96+
-- Do not fall back to `inherit` if there are no more tactics as that would cover up
97+
-- incremental reporting done in `inner?`. Do use default range in all other cases so that
98+
-- reporting ranges are properly nested.
99+
reportingRange :=
100+
if stxs.getNumArgs == 0 then .skip else SnapshotTask.defaultReportingRange stxs
101+
}]
90102
}
91103
-- Run `tac` in a fresh info tree state and store resulting state in snapshot for
92104
-- incremental reporting, then add back saved trees. Here we rely on `evalTactic`

‎src/Lean/Elab/Tactic/Induction.lean‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -364,7 +364,12 @@ where
364364
stx := mkNullNode altStxs
365365
diagnostics := .empty
366366
inner? := none
367-
finished := { stx? := mkNullNode altStxs, reportingRange := .inherit, task := finished.resultD default, cancelTk? }
367+
finished := {
368+
stx? := mkNullNode altStxs, task := finished.resultD default, cancelTk?
369+
-- Do not cover up progress from `next` as no significant work happens after `next` and
370+
-- before `finished` is resolved.
371+
reportingRange := .skip
372+
}
368373
next := Array.zipWith
369374
(fun stx prom => { stx? := some stx, task := prom.resultD default, cancelTk? })
370375
altStxs altPromises

‎tests/lean/snapshotTree.lean‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
/-!
2+
Sanity-check reported ranges for nested snapshot tree nodes. In particular, ranges of sibling nodes
3+
resolved later should not cover up progress inside earlier nodes.
4+
5+
This test cannot test per se whether such cover-up occurs without a dedicated synchronization
6+
protocol between the test and the involved tactics to control ordering of events like in the
7+
cancellation tests. Instead, it is intended merely to detect timing-independent changes to the
8+
snapshot tree and in the event of such changes, preservation of proper progress reporting needs to
9+
be verified manually.
10+
-/
11+
12+
set_option internal.cmdlineSnapshots false
13+
set_option trace.Elab.snapshotTree true
14+
example : True := by
15+
sleep 0
16+
sleep 100
17+
· next =>
18+
induction 0 with
19+
| zero =>
20+
sleep 100
21+
trivial
22+
| succ n =>
23+
sleep 100
24+
trivial

‎tests/lean/snapshotTree.lean.expected.out‎

Lines changed: 78 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,78 @@
1+
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd<no range>
2+
[Elab.snapshotTree] Lean.Language.instInhabitedDynamicSnapshot⟨13, 0⟩-⟨13, 39⟩
3+
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩
4+
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩
5+
[Elab.snapshotTree] Lean.Elab.Command.runLintersAsync<range inherited>
6+
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd<no range>
7+
[Elab.snapshotTree] Lean.Elab.Command.elabMutualDef⟨14, 0⟩-⟨24, 13⟩
8+
[Elab.snapshotTree] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabHeaders⟨14, 0⟩-⟨24, 13⟩
9+
[Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨15, 2⟩-⟨24, 13⟩
10+
[Elab.snapshotTree] ⟨15, 2⟩-⟨15, 9⟩
11+
[Elab.snapshotTree] <range inherited>
12+
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
13+
[Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨16, 2⟩-⟨24, 13⟩
14+
[Elab.snapshotTree] ⟨16, 2⟩-⟨16, 11⟩
15+
[Elab.snapshotTree] <range inherited>
16+
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
17+
[Elab.snapshotTree] Lean.cdot⟨17, 2⟩-⟨24, 13⟩
18+
[Elab.snapshotTree] Lean.Parser.Tactic.«tacticNext_=>_»⟨17, 2⟩-⟨24, 13⟩
19+
[Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval⟨17, 4⟩-⟨24, 13⟩
20+
[Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval<no range>
21+
[Elab.snapshotTree] Lean.Parser.Tactic.induction<range inherited>
22+
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo⟨18, 4⟩-⟨24, 13⟩
23+
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo<no range>
24+
[Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨19, 4⟩-⟨21, 13⟩
25+
[Elab.snapshotTree] ⟨20, 6⟩-⟨20, 15⟩
26+
[Elab.snapshotTree] <range inherited>
27+
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
28+
[Elab.snapshotTree] Lean.Parser.Tactic.tacticTrivial⟨21, 6⟩-⟨21, 13⟩
29+
[Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval⟨21, 6⟩-⟨21, 13⟩
30+
[Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval<no range>
31+
[Elab.snapshotTree] Lean.Parser.Tactic.apply<range inherited>
32+
[Elab.snapshotTree] <range inherited>
33+
[Elab.snapshotTree] <range inherited>
34+
[Elab.snapshotTree] <no range>
35+
[Elab.snapshotTree] <range inherited>
36+
[Elab.snapshotTree] <range inherited>
37+
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
38+
[Elab.snapshotTree] <no range>
39+
[Elab.snapshotTree] <range inherited>
40+
[Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨22, 4⟩-⟨24, 13⟩
41+
[Elab.snapshotTree] ⟨23, 6⟩-⟨23, 15⟩
42+
[Elab.snapshotTree] <range inherited>
43+
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
44+
[Elab.snapshotTree] Lean.Parser.Tactic.tacticTrivial⟨24, 6⟩-⟨24, 13⟩
45+
[Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval⟨24, 6⟩-⟨24, 13⟩
46+
[Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval<no range>
47+
[Elab.snapshotTree] Lean.Parser.Tactic.apply<range inherited>
48+
[Elab.snapshotTree] <range inherited>
49+
[Elab.snapshotTree] <range inherited>
50+
[Elab.snapshotTree] <no range>
51+
[Elab.snapshotTree] <range inherited>
52+
[Elab.snapshotTree] <range inherited>
53+
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
54+
[Elab.snapshotTree] <no range>
55+
[Elab.snapshotTree] <range inherited>
56+
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
57+
[Elab.snapshotTree] <no range>
58+
[Elab.snapshotTree] <range inherited>
59+
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
60+
[Elab.snapshotTree] <no range>
61+
[Elab.snapshotTree] <range inherited>
62+
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
63+
[Elab.snapshotTree] <no range>
64+
[Elab.snapshotTree] <range inherited>
65+
[Elab.snapshotTree] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabFunValues⟨14, 0⟩-⟨14, 0⟩
66+
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩
67+
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩
68+
[Elab.snapshotTree] <no range>
69+
[Elab.snapshotTree] <no range>
70+
[Elab.snapshotTree] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.logGoalsAccomplishedSnapshotTask<no range>
71+
• Goals accomplished!
72+
73+
[Elab.snapshotTree] Lean.Elab.Command.runLintersAsync<range inherited>
74+
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd<no range>
75+
[Elab.snapshotTree] Lean.Language.instInhabitedDynamicSnapshot⟨25, 0⟩-⟨25, 0⟩
76+
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩
77+
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩
78+
[Elab.snapshotTree] Lean.Elab.Command.runLintersAsync<range inherited>

0 commit comments

Comments
 (0)