| /-! | |
| 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 |