Large slowdown of Coq with OCaml 5.0 #11926
Description
We have not yet investigated where the time is spent, but @jhjourdan suggested I report the issue already. Things will become easier to reproduce once Coq 8.17.0 is released, which should be soon.
Below is a comparison of the time needed to compile various Coq-related Opam packages. NEW is OCaml 5.0 while OLD is OCaml 4.14. Package coq-core builds the Coq binaries, so Coq itself is not run. Other packages do run Coq to compile .v files, starting with coq-stdlib for Coq's standard library. As can be seen, Coq runs from 10% to 50% slower when compiled with OCaml 5.
The table below contains only a small selection of what I consider to be representative of Coq user developments. See rocq-prover/rocq#15494 for the complete tables.
┌─────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬──────────────────────────┐
│ │ user time [s] │ CPU cycles │ CPU instructions │ max resident mem [KB] │
│ │ │ │ │ │
│ package_name │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┤
│ coq-core │ 108.77 115.56 -5.88 │ 448176242336 475316383968 -5.71 │ 514833338600 484621682946 6.23 │ 349008 348540 0.13 │
│ coq-mathcomp-odd-order │ 460.19 420.33 9.48 │ 2105740732942 1925971651287 9.33 │ 3636963772697 3240724888710 12.23 │ 1660816 1548300 7.27 │
│ coq-unimath │ 1413.84 1286.34 9.91 │ 6449325705965 5870103915729 9.87 │ 12337978851391 10949635771154 12.68 │ 2610752 1595128 63.67 │
│ coq-bedrock2 │ 424.71 384.84 10.36 │ 1939859579088 1759094439924 10.28 │ 3939338066859 3438424521822 14.57 │ 1637572 960636 70.47 │
│ coq-mathcomp-field │ 102.61 92.87 10.49 │ 469145106933 425015888266 10.38 │ 800728664311 708580479443 13.00 │ 1207896 991884 21.78 │
│ coq-mathcomp-algebra │ 67.13 60.61 10.76 │ 306004188492 276943140328 10.49 │ 445538650133 389421431816 14.41 │ 778480 592284 31.44 │
│ coq-corn │ 884.20 787.11 12.33 │ 4027754587020 3592264603042 12.12 │ 6564781087980 5685800395118 15.46 │ 1227808 953876 28.72 │
│ coq-category-theory │ 876.81 780.11 12.40 │ 4005299774130 3564940614845 12.35 │ 6882470483447 5999346368760 14.72 │ 1691800 950456 78.00 │
│ coq-geocoq │ 754.20 664.75 13.46 │ 3435148027480 3032125535685 13.29 │ 5768255706915 4962353357381 16.24 │ 1386692 1044540 32.76 │
│ coq-coquelicot │ 40.32 35.09 14.90 │ 181669608454 156892061130 15.79 │ 259364772318 216191351923 19.97 │ 1029252 795264 29.42 │
│ coq-verdi │ 55.87 46.44 20.31 │ 253830568044 210894419676 20.36 │ 401185193644 324441924701 23.65 │ 761628 542540 40.38 │
│ coq-math-classes │ 108.57 89.00 21.99 │ 491023018742 404117277870 21.51 │ 738331588513 580845820789 27.11 │ 609912 503888 21.04 │
│ coq-hott │ 204.14 160.98 26.81 │ 924133893279 729612021105 26.66 │ 1481436404912 1160692706313 27.63 │ 740224 590128 25.43 │
│ coq-color │ 285.95 219.88 30.05 │ 1292347301747 996517976184 29.69 │ 1963372763085 1467553366877 33.79 │ 1664020 1208376 37.71 │
│ coq-stdlib │ 601.49 406.86 47.84 │ 2507810116636 1738015228647 44.29 │ 1973667764774 1429571108104 38.06 │ 996288 718004 38.76 │
│ coq-fiat-core │ 91.89 56.42 62.87 │ 401157873653 243392412738 64.82 │ 609702670266 357553599029 70.52 │ 625444 481032 30.02 │
└─────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴──────────────────────────┘