leanprover
perf: experiment: reduce primitive recursive functions directly
This PR is an experiment: What if the kernel would recognize primitiely recursive functions and treat them as recursors themselves. In paticular reduce them only when applied to a construtor, and then to the RHS directly.
Builds on top of #10548
Here are the benchmark results for commit 50c6490075a65e9411bd1cc60275b6def6e438b6. There were significant changes against commit 9fc18b8ab462cb9100d37a23814ebbac330e8577:
Benchmark Metric Change
=====================================================
+ big_beq_rec branches -2.8% (-261.7 σ)
+ big_beq_rec instructions -3.0% (-293.0 σ)
+ big_beq_rec task-clock -2.3% (-26.9 σ)
+ grind_ring_5.lean branch-misses -3.3% (-34.6 σ)
+ grind_ring_5.lean branches -10.1% (-621.0 σ)
+ grind_ring_5.lean instructions -10.8% (-711.1 σ)
+ grind_ring_5.lean maxrss -4.6% (-20.2 σ)
+ mut_rec_wf branches -2.5% (-213.7 σ)
+ mut_rec_wf instructions -2.6% (-221.6 σ)
+ reduceMatch instructions -1.0% (-29.1 σ)
Here are the benchmark results for commit b0692312c651883e340f0138a143548f9ea74968. There were significant changes against commit 9fc18b8ab462cb9100d37a23814ebbac330e8577:
Benchmark Metric Change
========================================================================
+ Init.Data.BitVec.Lemmas branch-misses -2.2% (-33.8 σ)
+ big_beq_rec branch-misses -3.9% (-26.3 σ)
+ big_beq_rec branches -2.8% (-133.7 σ)
+ big_beq_rec instructions -3.0% (-159.6 σ)
+ grind_ring_5.lean branches -11.1% (-597.4 σ)
+ grind_ring_5.lean instructions -11.9% (-498.5 σ)
+ grind_ring_5.lean maxrss -5.2% (-103.1 σ)
+ mut_rec_wf branches -2.5% (-227.7 σ)
+ mut_rec_wf instructions -2.6% (-174.8 σ)
+ reduceMatch instructions -1.1% (-23.0 σ)
- stdlib grind cutsat 24.8% (96.6 σ)
+ stdlib let-to-have transformation -1.2% (-526.2 σ)
Here are the benchmark results for commit 7fa3a2a8bbef3e07ad27ac96ebcb1127a9d634d5. There were significant changes against commit 9fc18b8ab462cb9100d37a23814ebbac330e8577:
Benchmark Metric Change
=====================================================================
+ big_beq_rec branches -2.8% (-117.3 σ)
+ big_beq_rec instructions -3.0% (-125.6 σ)
+ grind_ring_5.lean branch-misses -5.7% (-30.6 σ)
+ grind_ring_5.lean branches -12.2% (-1768.3 σ)
+ grind_ring_5.lean instructions -13.0% (-1889.8 σ)
+ mut_rec_wf branches -2.5% (-897.8 σ)
+ mut_rec_wf instructions -2.6% (-526.1 σ)
+ reduceMatch instructions -1.1% (-75.7 σ)
+ stdlib grind ac -17.4% (-33.5 σ)
+ stdlib grind dsimp -18.6% (-33.3 σ)
- workspaceSymbols with new ranges wall-clock 6.1% (23.8 σ)
Here are the benchmark results for commit 358c2cfe06b6a0cade339b34c9e15c56678c6813. There were significant changes against commit 9fc18b8ab462cb9100d37a23814ebbac330e8577:
Benchmark Metric Change
=====================================================
+ big_beq_rec branches -2.8% (-113.9 σ)
+ big_beq_rec instructions -3.0% (-118.0 σ)
- channel.lean unbounded_seq 4.1%
+ grind_ring_5.lean branches -22.7% (-145.5 σ)
+ grind_ring_5.lean instructions -24.1% (-125.7 σ)
+ grind_ring_5.lean maxrss -12.2% (-33.6 σ)
+ grind_ring_5.lean task-clock -23.7% (-30.4 σ)
+ grind_ring_5.lean wall-clock -23.5% (-28.2 σ)
+ mut_rec_wf branches -2.5% (-190.7 σ)
+ mut_rec_wf instructions -2.6% (-171.8 σ)
+ reduceMatch instructions -1.1% (-41.9 σ)
- riscv-ast.lean branch-misses 1.4% (33.5 σ)
+ stdlib task-clock -1.2% (-29.3 σ)
Here are the benchmark results for commit 6aa113c830a04e5fb515e1c950a7220df4e52f05. There were significant changes against commit 9fc18b8ab462cb9100d37a23814ebbac330e8577:
Benchmark Metric Change
====================================================================
+ Init.Data.BitVec.Lemmas branch-misses -2.1% (-85.5 σ)
+ big_beq_rec branches -2.8% (-263.1 σ)
+ big_beq_rec instructions -3.0% (-206.4 σ)
+ grind_ring_5.lean branch-misses -19.4% (-43.5 σ)
+ grind_ring_5.lean branches -32.0% (-908.2 σ)
+ grind_ring_5.lean instructions -34.1% (-850.6 σ)
+ grind_ring_5.lean maxrss -18.3% (-60.8 σ)
+ grind_ring_5.lean task-clock -34.2% (-34.4 σ)
+ grind_ring_5.lean wall-clock -33.9% (-34.7 σ)
+ iterators (compiled) maxrss -1.7% (-23.1 σ)
+ mut_rec_wf branch-misses -3.0% (-27.7 σ)
+ mut_rec_wf branches -2.5% (-317.9 σ)
+ mut_rec_wf instructions -2.6% (-302.9 σ)
+ reduceMatch instructions -1.0% (-41.6 σ)
+ stdlib grind ac -21.6% (-87.8 σ)
- stdlib maxrss 3.0% (195.1 σ)
+ workspaceSymbols with new ranges maxrss -1.7% (-23.1 σ)
Here are the benchmark results for commit 94d2a9ab0b4c43a2c0c5bea65bcc4f15034c277c. The entire run failed. Found no significant differences.
Here are the benchmark results for commit c9a2413da89fb487f34205170b4777d898d729a4. There were significant changes against commit 9fc18b8ab462cb9100d37a23814ebbac330e8577:
Benchmark Metric Change
======================================================
+ big_beq_rec branches -2.8% (-156.8 σ)
+ big_beq_rec instructions -3.0% (-168.1 σ)
+ grind_ring_5.lean branch-misses -20.7% (-41.8 σ)
+ grind_ring_5.lean branches -34.3% (-3916.9 σ)
+ grind_ring_5.lean instructions -36.4% (-3832.9 σ)
+ grind_ring_5.lean maxrss -19.4% (-107.1 σ)
+ grind_ring_5.lean task-clock -35.9% (-47.8 σ)
+ grind_ring_5.lean wall-clock -35.6% (-48.5 σ)
+ mut_rec_wf branches -2.5% (-83.4 σ)
+ mut_rec_wf instructions -2.6% (-76.0 σ)
+ reduceMatch instructions -1.1% (-47.5 σ)
+ stdlib grind ac -18.1% (-57.2 σ)
+ stdlib grind dsimp -22.9% (-32.7 σ)