Performance experiments - coq/coq GitHub Wiki
This page is more for failed experiments, as successful ones can get merged (but feel free to add them here too ^^).
Skipping conversion of parameters of constructors and of the domain of lambdas (failed)
When converting fun x : A => e and fun x : A' => e' if I know they
have the same type forall x : A, B I know that A == A' (Pi-injectivity).
Analogously when converting constructors we can skip parameters without breaking soundness.
The experiment fails because the kernel converts application arguments right to left, so if we have P : forall T, T -> ... and convert P (forall A0, ...) (fun x : A0' => ...) and P (forall A1, ...) (fun x : A1' => ...) we look at the lambdas before testing A0 == A1 (which by typing would imply A0' == A1'). This means skipping the lambda annotations skips a chance at early failure. Of course the same is true of skipping constructor parameters. Here's a partial bench: https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/391/console
┌──────────────────────────┬───────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬─────────────────┐
│ │ user time [s] │ CPU cycles │ CPU instructions │ max resident mem [KB] │ mem faults │
│ │ │ │ │ │ │
│ package_name │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-field │ 205.60 461.51 -55.45 % │ 568829876254 1281746757731 -55.62 % │ 819365613062 2059996916568 -60.22 % │ 745460 814356 -8.46 % │ 0 0 +nan % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-real_closed │ 117.40 172.82 -32.07 % │ 324619461164 478365156189 -32.14 % │ 436543675931 699685289928 -37.61 % │ 811412 844848 -3.96 % │ 0 0 +nan % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-algebra │ 157.57 185.61 -15.11 % │ 435515533971 512539927127 -15.03 % │ 559400684428 690239426679 -18.96 % │ 643312 652328 -1.38 % │ 0 0 +nan % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-character │ 255.34 275.70 -7.38 % │ 707539906521 764571391145 -7.46 % │ 986603630955 1085745868624 -9.13 % │ 1099132 1127652 -2.53 % │ 0 5 -100.00 % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-fingroup │ 60.84 64.40 -5.53 % │ 167026713738 177626419100 -5.97 % │ 218191435415 236222596014 -7.63 % │ 588172 593152 -0.84 % │ 0 0 +nan % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-bignums │ 79.67 80.06 -0.49 % │ 219377009283 220962251825 -0.72 % │ 283573204732 286100393647 -0.88 % │ 529324 527276 +0.39 % │ 0 0 +nan % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-ssreflect │ 44.67 44.67 +0.00 % │ 121988881003 122288140972 -0.24 % │ 141851033114 142842125752 -0.69 % │ 536056 537640 -0.29 % │ 0 0 +nan % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-formal-topology │ 37.55 37.42 +0.35 % │ 100801859530 100686387892 +0.11 % │ 125318244163 125809356994 -0.39 % │ 483236 483448 -0.04 % │ 0 0 +nan % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-solvable │ 230.96 201.62 +14.55 % │ 639721848901 558026456354 +14.64 % │ 889219447748 767706053248 +15.83 % │ 840240 841228 -0.12 % │ 0 0 +nan % │
├──────────────────────────┼───────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-odd_order │ 2878.81 1427.47 +101.67 % │ 8004985597716 3963150813359 +101.99 % │ 12823742839111 6663549213977 +92.45 % │ 1406176 1391924 +1.02 % │ 0 0 +nan % │
└──────────────────────────┴───────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴─────────────────┘
If we change the comparison order to left to right (as in #396) the above is alleviated but other places slow down to death: https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/393/console
┌──────────────────────────┬──────────────────────────┬──────────────────────────────────────┬──────────────────────────────────────┬─────────────────────────┬─────────────────┐
│ │ user time [s] │ CPU cycles │ CPU instructions │ max resident mem [KB] │ mem faults │
│ │ │ │ │ │ │
│ package_name │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-field │ 231.34 460.46 -49.76 % │ 640657643986 1278240468084 -49.88 % │ 938840609184 2059983208186 -54.42 % │ 749856 814472 -7.93 % │ 0 0 +nan % │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-real_closed │ 128.33 172.62 -25.66 % │ 354519892910 477561398004 -25.76 % │ 485813524117 699666070629 -30.56 % │ 820416 844836 -2.89 % │ 0 0 +nan % │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-algebra │ 165.87 184.82 -10.25 % │ 457805151555 511415943712 -10.48 % │ 596950648013 690197168687 -13.51 % │ 647160 652284 -0.79 % │ 0 0 +nan % │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-fingroup │ 60.34 64.52 -6.48 % │ 165936604399 177375464335 -6.45 % │ 217866367230 236360925820 -7.82 % │ 586992 593140 -1.04 % │ 0 0 +nan % │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-ssreflect │ 44.44 45.01 -1.27 % │ 121629722412 122142651036 -0.42 % │ 141930184433 142889177229 -0.67 % │ 538080 537696 +0.07 % │ 0 0 +nan % │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-bignums │ 79.58 80.22 -0.80 % │ 219446666227 220754218164 -0.59 % │ 283500824146 286198520125 -0.94 % │ 525864 527396 -0.29 % │ 0 0 +nan % │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-odd_order │ 1491.34 1426.42 +4.55 % │ 4143753719381 3962374851065 +4.58 % │ 6959165055834 6663513117214 +4.44 % │ 1366556 1389552 -1.65 % │ 0 0 +nan % │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-solvable │ 211.22 201.86 +4.64 % │ 584641881650 557846578469 +4.80 % │ 822480782071 767855064436 +7.11 % │ 878612 866188 +1.43 % │ 0 0 +nan % │
├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-character │ 293.63 275.63 +6.53 % │ 814656149843 764490284216 +6.56 % │ 1167220824117 1085807185628 +7.50 % │ 1121104 1127156 -0.54 % │ 0 0 +nan % │
└──────────────────────────┴──────────────────────────┴──────────────────────────────────────┴──────────────────────────────────────┴─────────────────────────┴─────────────────┘
after those developments formal topology didn't finish in ~8h (then I killed it). CI results for #396 at the time insinuate this may be in the corn dependency.
See https://github.com/SkySkimmer/coq/commit/1575ec75346a00955fd2f3f95179e958bbdc8b77 for implementation issues related to badly behaving callers.
Delay Universe Substitution in CClosure
See https://github.com/coq/coq/pull/8747.
┌──────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬──────────────────────────┬──────────────────────┐
│ │ user time [s] │ CPU cycles │ CPU instructions │ max resident mem [KB] │ mem faults │
│ │ │ │ │ │ │
│ package_name │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-hott │ 332.92 341.64 -2.55 % │ 923345431138 946156146841 -2.41 % │ 1406642863391 1440100985649 -2.32 % │ 643632 666792 -3.47 % │ 430 0 +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-sf-lf │ 44.21 44.42 -0.47 % │ 121743835280 122546861357 -0.66 % │ 199315596414 199501609977 -0.09 % │ 423608 422796 +0.19 % │ 128 0 +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-flocq │ 590.32 592.00 -0.28 % │ 1640292423178 1647156759308 -0.42 % │ 2411354196739 2405224361056 +0.25 % │ 1764632 1766556 -0.11 % │ 606 867 -30.10 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-formal-topology │ 58.08 58.24 -0.27 % │ 158304951558 158865962983 -0.35 % │ 239184450169 239985754037 -0.33 % │ 477836 477416 +0.09 % │ 0 0 +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-mathcomp-odd-order │ 1417.46 1420.48 -0.21 % │ 3948768967038 3956033844700 -0.18 % │ 6699320818703 6658637427858 +0.61 % │ 1350972 1359328 -0.61 % │ 261 49 +432.65 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-compcert │ 889.88 891.51 -0.18 % │ 2467456059069 2470265840463 -0.11 % │ 3578096037308 3561391545432 +0.47 % │ 1343276 1349328 -0.45 % │ 617 339 +82.01 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-math-classes │ 249.50 249.83 -0.13 % │ 687224056760 688445471139 -0.18 % │ 900867275902 899805525097 +0.12 % │ 523152 522136 +0.19 % │ 84 81 +3.70 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-fiat-parsers │ 719.68 719.13 +0.08 % │ 1998538693108 1996036522423 +0.13 % │ 3080457738017 3054736560975 +0.84 % │ 2880308 2898680 -0.63 % │ 590 761 -22.47 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-sf-plf │ 74.76 74.68 +0.11 % │ 206677543407 206541556383 +0.07 % │ 301500338389 300926704664 +0.19 % │ 521084 518568 +0.49 % │ 15 0 +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-sf-vfa │ 47.64 47.56 +0.17 % │ 130990748145 131378232688 -0.29 % │ 209993439783 209968706004 +0.01 % │ 542076 533452 +1.62 % │ 28 5 +460.00 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-fiat-core │ 135.46 135.22 +0.18 % │ 376724696562 377146921844 -0.11 % │ 504668380099 504069509866 +0.12 % │ 499292 497676 +0.32 % │ 613 188 +226.06 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-mathcomp-ssreflect │ 65.66 65.54 +0.18 % │ 180023791228 180139505878 -0.06 % │ 257095867228 256804442513 +0.11 % │ 532368 532128 +0.05 % │ 26 257 -89.88 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-fiat-crypto │ 6397.87 6379.31 +0.29 % │ 17792985556962 17744074236815 +0.28 % │ 29252536240733 29120658840711 +0.45 % │ 2723356 2450576 +11.13 % │ 1735 1347 +28.80 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-color │ 740.67 738.32 +0.32 % │ 2053660253546 2044831815430 +0.43 % │ 2478563555420 2468606887351 +0.40 % │ 1371488 1375072 -0.26 % │ 39 113 -65.49 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-mathcomp-fingroup │ 85.43 85.12 +0.36 % │ 236125046171 235251178827 +0.37 % │ 350268845326 348848446344 +0.41 % │ 594012 586388 +1.30 % │ 4 48 -91.67 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-coquelicot │ 104.28 103.85 +0.41 % │ 287965548005 287163328551 +0.28 % │ 388520908545 387043551167 +0.38 % │ 725296 712312 +1.82 % │ 282 13 +2069.23 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-corn │ 1552.32 1545.75 +0.43 % │ 4309382166395 4292619603160 +0.39 % │ 6377647772888 6347727518034 +0.47 % │ 926048 818152 +13.19 % │ 45 60 -25.00 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-geocoq │ 2850.83 2838.13 +0.45 % │ 7925675384464 7888923000596 +0.47 % │ 12703682815750 12579309110573 +0.99 % │ 1287824 1287704 +0.01 % │ 606 190 +218.95 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-bignums │ 99.47 98.88 +0.60 % │ 274747249868 273697891152 +0.38 % │ 394665541113 393829024474 +0.21 % │ 536180 539500 -0.62 % │ 175 43 +306.98 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-lambda-rust │ 2343.50 2329.46 +0.60 % │ 6526599399602 6488604622730 +0.59 % │ 9033098570801 8964156114014 +0.77 % │ 1544608 1450244 +6.51 % │ 141 15 +840.00 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-mathcomp-character │ 296.24 294.30 +0.66 % │ 823620010282 817415400929 +0.76 % │ 1197870057955 1191274757722 +0.55 % │ 1059976 1117428 -5.14 % │ 45 302 -85.10 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-mathcomp-solvable │ 222.11 220.18 +0.88 % │ 617364103658 611819400697 +0.91 % │ 882438288585 875349132855 +0.81 % │ 807792 855168 -5.54 % │ 2 1 +100.00 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-vst │ 1728.61 1712.80 +0.92 % │ 4806190843916 4762314463771 +0.92 % │ 6562293639934 6513293300621 +0.75 % │ 2447808 2225288 +10.00 % │ 1166 868 +34.33 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-unimath │ 1343.67 1331.10 +0.94 % │ 3731593916573 3693996753506 +1.02 % │ 6317397679880 6240478754512 +1.23 % │ 1133008 971376 +16.64 % │ 356 19 +1773.68 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-mathcomp-algebra │ 208.10 205.23 +1.40 % │ 577371493468 569418457780 +1.40 % │ 810525479858 799120309546 +1.43 % │ 648824 640676 +1.27 % │ 293 14 +1992.86 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-mathcomp-real-closed │ 190.92 188.10 +1.50 % │ 531068217299 523597662881 +1.43 % │ 804622480648 790375813147 +1.80 % │ 853992 830204 +2.87 % │ 1 1 +0.00 % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼──────────────────────┤
│ coq-mathcomp-field │ 475.01 467.97 +1.50 % │ 1321459762740 1301256230599 +1.55 % │ 2164466154596 2127074570257 +1.76 % │ 805852 802264 +0.45 % │ 2 19 -89.47 % │
└──────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴──────────────────────────┴──────────────────────┘