Skip to content

Commit

Permalink
reduce repetition amount in scaling test to reduce flakiness
Browse files Browse the repository at this point in the history
  • Loading branch information
alexkeizer committed Jan 28, 2025
1 parent 50ea152 commit 077c1e8
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions tests/lean/run/ac_nf.lean
Original file line number Diff line number Diff line change
Expand Up @@ -72,12 +72,12 @@ local macro "repeat_add" n:num "with" x:term : term =>

/-
This test showcases that the runtime of `ac_nf'` is not a bottleneck:
* The current example runs in about 250ms with a disabled kernel, or ~5 seconds with,
showing that the tactic runtime is tiny compared to the proof-checking time, and
* Putting in 125 for the repitition amount wil give a `maximum recursion depth has been reached`
* Testing with 100 as the repetition amount runs in about 200ms with `skipKernelTC` set,
or ~3.3 seconds without (c.q. 2.3s for `ac_rfl`), and
* Putting in 125 for the repetition amount wil give a `maximum recursion depth has been reached`
error thrown by simp anyway, so the runtime is not a limiting factor to begin with.
-/
set_option debug.skipKernelTC true in
example (x y : BitVec 64) :
(repeat_add 124 with x + y) = (repeat_add 124 with x) + (repeat_add 124 with y) := by
(repeat_add 100 with x + y) = (repeat_add 100 with x) + (repeat_add 100 with y) := by
ac_nf'; rfl

0 comments on commit 077c1e8

Please sign in to comment.