Performance experiments

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 % │
└──────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴──────────────────────────┴──────────────────────┘

Converting in the right order in the kernel

https://github.com/coq/coq/pull/19038