Actually rely on the environment to compute canonical data. #21075

ppedrot · 2025-09-07T12:36:12Z

Adding some assertions shows that we're playing fast and loose with canonical names, but let's try at least this variant to assess the overall breakage / performance impact.

ppedrot · 2025-09-07T12:48:42Z

@coqbot bench

coqbot-app · 2025-09-07T22:01:19Z

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                       coq-fourcolor │ 1341.53  1347.99  -0.48 │ 12467149791698  12457031359629   0.08 │  969956   967916   0.21 │
│ coq-neural-net-interp-computed-lite │  233.96   234.73  -0.33 │  2261165748444   2256668067077   0.20 │  848592   845920   0.32 │
│                       coq-fiat-core │   59.12    59.15  -0.05 │   360035043219    355519659648   1.27 │  487752   485144   0.54 │
│                        rocq-runtime │   73.17    73.19  -0.03 │   528640012073    528377888931   0.05 │  490340   487560   0.57 │
│                           rocq-core │    6.23     6.23   0.00 │    38588800141     38368429485   0.57 │  440768   439720   0.24 │
│               coq-engine-bench-lite │  125.88   125.83   0.04 │   944434419242    939993107475   0.47 │  980504   980520  -0.00 │
│                           rocq-elpi │   14.25    14.23   0.14 │   102101639389    101981467189   0.12 │  555996   555980   0.00 │
│                        coq-coqprime │   51.98    51.85   0.25 │   361411378123    358058573107   0.94 │  808372   808256   0.01 │
│                            coq-core │    2.68     2.67   0.37 │    18295174832     18250422699   0.25 │   93472    93536  -0.07 │
│                      rocq-equations │    8.48     8.44   0.47 │    59032983682     58865880192   0.28 │  401816   398268   0.89 │
│              coq-mathcomp-odd-order │  574.19   571.44   0.48 │  4169721883916   4136174421351   0.81 │ 2588268  2583464   0.19 │
│                 rocq-mathcomp-field │  163.13   162.18   0.59 │  1250953668007   1244799273216   0.49 │ 2044628  2031484   0.65 │
│                             coq-vst │  852.94   847.73   0.61 │  6484506081647   6415534055322   1.08 │ 2215840  2071660   6.96 │
│                 rocq-metarocq-utils │   23.17    23.02   0.65 │   152269933252    150255350207   1.34 │  587612   582468   0.88 │
│                           coq-color │  250.59   248.94   0.66 │  1578778828007   1559355085033   1.25 │ 1132668  1136216  -0.31 │
│                         coq-coqutil │   46.06    45.73   0.72 │   289501457137    286520042285   1.04 │  561936   560128   0.32 │
│          coq-performance-tests-lite │  904.76   897.68   0.79 │  7368283307682   7270203686029   1.35 │ 2070424  2192172  -5.55 │
│              rocq-mathcomp-fingroup │   24.72    24.51   0.86 │   161446381446    159707552506   1.09 │  563904   563692   0.04 │
│                         coq-unimath │ 1789.62  1773.50   0.91 │ 14956371625175  14798595131573   1.07 │ 1085004  1091004  -0.55 │
│                            coq-hott │  158.76   157.08   1.07 │  1096868403937   1085312321017   1.06 │  477068   459772   3.76 │
│                        coq-bedrock2 │  350.33   346.40   1.13 │  2948476318924   2909884733195   1.33 │  850060   850840  -0.09 │
│                    coq-fiat-parsers │  282.42   279.05   1.21 │  2177325706739   2138178171607   1.83 │ 2347628  2013976  16.57 │
│          rocq-metarocq-translations │   16.02    15.81   1.33 │   114256656454    112356467389   1.69 │  783176   773040   1.31 │
│                        coq-compcert │  311.82   307.59   1.38 │  2049563004756   2019008345749   1.51 │ 1298800  1202572   8.00 │
│                            coq-corn │  685.51   676.14   1.39 │  4732102716101   4661754632926   1.51 │  727188   668184   8.83 │
│                rocq-metarocq-common │   42.29    41.67   1.49 │   273350889874    268973008565   1.63 │  902572   901980   0.07 │
│                        rocq-bignums │   28.65    28.20   1.60 │   184797403923    181479163387   1.83 │  481728   481264   0.10 │
│              rocq-mathcomp-solvable │   97.73    96.18   1.61 │   674092179859    667729515163   0.95 │ 1116092  1118172  -0.19 │
│                         rocq-stdlib │  449.98   442.73   1.64 │  1592566451626   1577936792952   0.93 │  638828   645224  -0.99 │
│         coq-rewriter-perf-SuperFast │  483.48   475.09   1.77 │  3792245689466   3742120146131   1.34 │ 1236892  1226548   0.84 │
│                      coq-coquelicot │   40.50    39.79   1.78 │   243176437728    240395685223   1.16 │  837884   835600   0.27 │
│               coq-mathcomp-analysis │  967.45   950.45   1.79 │  7251096082800   7211488965700   0.55 │ 2122048  2107824   0.67 │
│                 coq-category-theory │  620.78   609.80   1.80 │  4580096884718   4529788279844   1.11 │ 1027788  1005864   2.18 │
│               rocq-mathcomp-algebra │  297.78   292.39   1.84 │  2216674394993   2207411915881   0.42 │ 1472676  1458004   1.01 │
│                        coq-rewriter │  345.90   339.01   2.03 │  2605398169363   2535274524593   2.77 │ 1363432  1304136   4.55 │
│               rocq-metarocq-erasure │  504.55   493.91   2.15 │  3466902322082   3391523373840   2.22 │ 1915364  1908468   0.36 │
│              rocq-metarocq-template │   82.82    80.86   2.42 │   570661679921    560819140681   1.76 │ 1027816  1035236  -0.72 │
│             rocq-mathcomp-character │   93.94    91.66   2.49 │   659022999112    653570607465   0.83 │ 1590244  1588632   0.10 │
│           rocq-metarocq-safechecker │  328.66   320.38   2.58 │  2473240397018   2412048380720   2.54 │ 1891200  1853960   2.01 │
│                    coq-math-classes │   88.71    86.41   2.66 │   539320475425    529615277734   1.83 │  515336   513096   0.44 │
│                 rocq-metarocq-pcuic │  649.68   631.20   2.93 │  4159951553392   4081414241409   1.92 │ 1904084  1939288  -1.82 │
│                           coq-verdi │   45.66    44.34   2.98 │   304679991046    292476525648   4.17 │  527104   526864   0.05 │
│                   coq-iris-examples │  367.29   356.50   3.03 │  2420990888348   2359188666378   2.62 │ 1109604  1084832   2.28 │
│             rocq-mathcomp-ssreflect │    1.36     1.31   3.82 │     9201754699      9159950359   0.46 │  605684   605776  -0.02 │
│                      coq-verdi-raft │  555.81   528.26   5.22 │  3889113705537   3669810096188   5.98 │  821408   816200   0.64 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-fiat-crypto-with-bedrock (in NEW)

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                     TOP 25 SLOW DOWNS                                                     │
│                                                                                                                           │
│  OLD     NEW     DIFF    %DIFF    Ln                  FILE                                                                │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   9.79    10.6  0.7733    7.90%   673  coq-rewriter/src/Rewriter/Rewriter/Wf.v.html                                       │
│ 32.112  32.822  0.7100    2.21%    97  coq-vst/veric/binop_lemmas5.v.html                                                 │
│ 40.889  41.596  0.7070    1.73%   834  coq-vst/veric/binop_lemmas4.v.html                                                 │
│   21.1    21.8  0.6839    3.24%   651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                          │
│   4.89    5.50  0.6117   12.51%  1576  coq-rewriter/src/Rewriter/Language/UnderLetsProofs.v.html                          │
│   22.9    23.5  0.6025    2.63%    79  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html │
│   2.86    3.45  0.5922   20.69%   597  coq-verdi-raft/theories/RaftProofs/AllEntriesLogProof.v.html                       │
│  0.259   0.845  0.5859  226.30%    12  rocq-stdlib/theories/MSets/MSets.v.html                                            │
│   7.32    7.79  0.4619    6.31%   356  coq-rewriter/src/Rewriter/Rewriter/Wf.v.html                                       │
│   9.06    9.52  0.4601    5.08%   434  coq-mathcomp-odd-order/theories/PFsection12.v.html                                 │
│   1.46    1.89  0.4305   29.54%  1209  coq-rewriter/src/Rewriter/Rewriter/InterpProofs.v.html                             │
│   1.11    1.50  0.3932   35.55%  1142  rocq-stdlib/theories/FSets/FMapAVL.v.html                                          │
│   3.62    4.01  0.3892   10.74%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html      │
│   5.86    6.24  0.3747    6.39%   819  coq-rewriter/src/Rewriter/Rewriter/InterpProofs.v.html                             │
│  0.917    1.29  0.3708   40.46%   215  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                 │
│   1.90    2.27  0.3690   19.43%   427  coq-verdi-raft/theories/RaftProofs/AllEntriesLogProof.v.html                       │
│   8.60    8.97  0.3672    4.27%  1393  coq-rewriter/src/Rewriter/Language/UnderLetsProofs.v.html                          │
│   1.85    2.21  0.3650   19.76%   647  coq-verdi-raft/theories/RaftProofs/AllEntriesLogProof.v.html                       │
│   48.7    49.0  0.3635    0.75%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html        │
│   18.9    19.3  0.3597    1.90%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                  │
│  0.433   0.790  0.3562   82.17%   200  rocq-stdlib/theories/Numbers/HexadecimalNat.v.html                                 │
│   7.40    7.75  0.3506    4.74%  3379  rocq-metarocq-safechecker/safechecker/theories/PCUICSafeConversion.v.html          │
│  0.913    1.26  0.3436   37.63%   813  rocq-stdlib/theories/MSets/MSetRBT.v.html                                          │
│   5.62    5.95  0.3305    5.88%   628  coq-bedrock2/bedrock2/src/bedrock2Examples/LAN9250.v.html                          │
│   1.51    1.81  0.3048   20.18%   449  coq-verdi-raft/theories/RaftProofs/AllEntriesLogProof.v.html                       │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                          TOP 25 SPEED UPS                                                           │
│                                                                                                                                     │
│  OLD    NEW    DIFF     %DIFF    Ln                    FILE                                                                         │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   200    198  -1.6380   -0.82%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│  62.9   62.2  -0.7491   -1.19%   608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                   │
│  23.6   23.0  -0.5433   -2.30%    12  coq-fourcolor/theories/proof/job554to562.v.html                                               │
│  39.2   38.7  -0.4869   -1.24%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                    │
│  36.6   36.2  -0.4827   -1.32%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                  │
│  2.89   2.44  -0.4583  -15.84%   607  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                     │
│  31.0   30.6  -0.4463   -1.44%    12  coq-fourcolor/theories/proof/job254to270.v.html                                               │
│  2.74   2.33  -0.4109  -15.00%   240  coq-category-theory/Construction/Comma/Adjunction.v.html                                      │
│  25.1   24.7  -0.3776   -1.51%    12  coq-fourcolor/theories/proof/job291to294.v.html                                               │
│  29.0   28.7  -0.3638   -1.25%    12  coq-fourcolor/theories/proof/job589to610.v.html                                               │
│ 1.426  1.074  -0.3520  -24.68%   937  coq-vst/veric/binop_lemmas2.v.html                                                            │
│  25.0   24.7  -0.3436   -1.37%    12  coq-fourcolor/theories/proof/job299to302.v.html                                               │
│  24.0   23.7  -0.3411   -1.42%    12  coq-fourcolor/theories/proof/job486to489.v.html                                               │
│  30.0   29.6  -0.3386   -1.13%    12  coq-fourcolor/theories/proof/job165to189.v.html                                               │
│  25.5   25.1  -0.3339   -1.31%    12  coq-fourcolor/theories/proof/job499to502.v.html                                               │
│  25.2   24.9  -0.3092   -1.23%    12  coq-fourcolor/theories/proof/job223to226.v.html                                               │
│  21.4   21.1  -0.3021   -1.41%    12  coq-fourcolor/theories/proof/job542to545.v.html                                               │
│  24.4   24.1  -0.2996   -1.23%    12  coq-fourcolor/theories/proof/job319to322.v.html                                               │
│ 0.480  0.181  -0.2992  -62.36%   374  rocq-stdlib/theories/Sorting/SetoidList.v.html                                                │
│  2.73   2.45  -0.2755  -10.09%  1001  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│  19.5   19.2  -0.2707   -1.39%    12  coq-fourcolor/theories/proof/job507to510.v.html                                               │
│  24.7   24.4  -0.2609   -1.06%    12  coq-fourcolor/theories/proof/job503to506.v.html                                               │
│  25.6   25.4  -0.2552   -1.00%    12  coq-fourcolor/theories/proof/job466to485.v.html                                               │
│  19.9   19.6  -0.2492   -1.25%    12  coq-fourcolor/theories/proof/job546to549.v.html                                               │
│  20.4   20.2  -0.2479   -1.21%    12  coq-fourcolor/theories/proof/job283to286.v.html                                               │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

We first check for label equality, which is fast, before trying to normalize then name. The kernel guarantees that aliased names have the same label, so this is sound.

ppedrot · 2025-09-10T07:51:55Z

@coqbot run full ci

ppedrot · 2025-09-10T09:27:09Z

@coqbot bench

coqbot-app · 2025-09-10T18:38:13Z

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                            coq-core │    2.64     2.66  -0.75 │    18267552051     18305873315  -0.21 │   93744    93636   0.12 │
│                        rocq-runtime │   73.15    73.18  -0.04 │   530565357622    530403426252   0.03 │  493196   494180  -0.20 │
│             rocq-mathcomp-ssreflect │    1.29     1.29   0.00 │     9205183946      9160778767   0.48 │  605816   605780   0.01 │
│                        coq-coqprime │   51.98    51.79   0.37 │   361372443190    358325962037   0.85 │  807540   806232   0.16 │
│                 rocq-mathcomp-field │  161.39   160.73   0.41 │  1250562454820   1245298189302   0.42 │ 2048820  2060140  -0.55 │
│                           rocq-elpi │   14.13    14.06   0.50 │   102131002057    102014308937   0.11 │  556688   556276   0.07 │
│ coq-neural-net-interp-computed-lite │  234.33   233.02   0.56 │  2260253443757   2257457924418   0.12 │  846456   845388   0.13 │
│                      rocq-equations │    8.51     8.46   0.59 │    59080712509     58915340207   0.28 │  398536   398440   0.02 │
│                         rocq-stdlib │  444.73   441.55   0.72 │  1597085394814   1582153222281   0.94 │  630524   633820  -0.52 │
│                rocq-metarocq-common │   42.05    41.73   0.77 │   272196786204    269346289468   1.06 │  894792   894176   0.07 │
│                       coq-fourcolor │ 1344.12  1333.76   0.78 │ 12467276312264  12458165602558   0.07 │  968144   965868   0.24 │
│                            coq-hott │  157.46   156.24   0.78 │  1095971848809   1087431716738   0.79 │  475068   466816   1.77 │
│                           rocq-core │    6.17     6.12   0.82 │    38731586076     38525352564   0.54 │  439716   439800  -0.02 │
│               rocq-mathcomp-algebra │  294.87   292.31   0.88 │  2215306846572   2207495156271   0.35 │ 1468852  1467724   0.08 │
│               coq-engine-bench-lite │  125.59   124.31   1.03 │   946989195909    939210294016   0.83 │ 1077256  1078840  -0.15 │
│                 coq-category-theory │  620.89   613.90   1.14 │  4565546176506   4529413612233   0.80 │  916640  1005584  -8.85 │
│         coq-rewriter-perf-SuperFast │  472.49   467.15   1.14 │  3771188721405   3742637405312   0.76 │ 1234960  1224372   0.86 │
│                             coq-vst │  851.60   841.72   1.17 │  6476515143290   6418036055232   0.91 │ 2210972  2057240   7.47 │
│                         coq-unimath │ 1795.76  1773.16   1.27 │ 14949318297043  14799854911147   1.01 │ 1090056  1076940   1.22 │
│                    coq-fiat-parsers │  280.49   276.85   1.31 │  2160920651830   2139165472630   1.02 │ 2002048  2015144  -0.65 │
│                        coq-bedrock2 │  352.28   347.65   1.33 │  2934242567985   2918005962187   0.56 │  834492   849444  -1.76 │
│                            coq-corn │  685.90   676.85   1.34 │  4715335217406   4664956457101   1.08 │  724724   726996  -0.31 │
│                    coq-math-classes │   87.89    86.72   1.35 │   535198561122    530090254472   0.96 │  513928   513840   0.02 │
│                 rocq-metarocq-pcuic │  643.86   634.89   1.41 │  4145005883745   4082435000337   1.53 │ 1884352  1878496   0.31 │
│                           coq-color │  251.48   247.92   1.44 │  1580642636882   1562303784975   1.17 │ 1144904  1142056   0.25 │
│               coq-mathcomp-analysis │  959.87   945.73   1.50 │  7249999414269   7212795176599   0.52 │ 2134448  2150888  -0.76 │
│           rocq-metarocq-safechecker │  324.98   320.19   1.50 │  2429713492056   2413876780318   0.66 │ 1882508  1878928   0.19 │
│              rocq-metarocq-template │   81.67    80.44   1.53 │   568164753273    561967509300   1.10 │ 1033256  1034776  -0.15 │
│          coq-performance-tests-lite │  909.93   896.17   1.54 │  7361554899501   7270819275482   1.25 │ 2071228  2192316  -5.52 │
│                       coq-fiat-core │   58.92    57.97   1.64 │   360120740599    355882494278   1.19 │  485244   483420   0.38 │
│                        coq-rewriter │  342.67   337.09   1.66 │  2569253877792   2535107632865   1.35 │ 1365640  1310324   4.22 │
│                         coq-coqutil │   45.97    45.19   1.73 │   289540798996    286968521482   0.90 │  561820   560020   0.32 │
│                      coq-coquelicot │   40.58    39.88   1.76 │   243750712519    241005014606   1.14 │  842196   841488   0.08 │
│                 rocq-metarocq-utils │   23.12    22.70   1.85 │   152010194395    150505832046   1.00 │  586160   591212  -0.85 │
│                        coq-compcert │  312.94   307.19   1.87 │  2047332511314   2022912028835   1.21 │ 1203700  1293984  -6.98 │
│          rocq-metarocq-translations │   15.98    15.68   1.91 │   113989072514    112549260743   1.28 │  781368   785520  -0.53 │
│              rocq-mathcomp-fingroup │   24.97    24.42   2.25 │   161454977015    159752728530   1.07 │  561684   560000   0.30 │
│                        rocq-bignums │   28.80    28.16   2.27 │   184777145643    181939933222   1.56 │  479976   480836  -0.18 │
│              coq-mathcomp-odd-order │  579.02   565.35   2.42 │  4169310003485   4137301987078   0.77 │ 2602248  2597720   0.17 │
│              rocq-mathcomp-solvable │   98.02    95.70   2.42 │   674031096370    667939425856   0.91 │ 1121772  1116280   0.49 │
│                           coq-verdi │   44.86    43.79   2.44 │   298371075414    292380997281   2.05 │  536536   524592   2.28 │
│             rocq-mathcomp-character │   93.68    91.44   2.45 │   658888550070    653919436749   0.76 │ 1588764  1586624   0.13 │
│               rocq-metarocq-erasure │  502.22   489.56   2.59 │  3445003627566   3392942800272   1.53 │ 1828956  1944768  -5.96 │
│                      coq-verdi-raft │  542.03   527.77   2.70 │  3744599739032   3670363669862   2.02 │  818756   816412   0.29 │
│                   coq-iris-examples │  368.32   356.81   3.23 │  2403668087085   2359974184087   1.85 │ 1128388  1068584   5.60 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-fiat-crypto-with-bedrock (in NEW)

🐢 Top 25 slow downs

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                          TOP 25 SLOW DOWNS                                                          │
│                                                                                                                                     │
│  OLD     NEW     DIFF   %DIFF    Ln                    FILE                                                                         │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   95.9    98.9  2.9225   3.05%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│   96.1    98.8  2.7585   2.87%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│   62.9    64.5  1.5947   2.53%   608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                   │
│   5.22    6.57  1.3434  25.73%   130  coq-category-theory/Functor/Strong/Product.v.html                                             │
│    198     199  1.2533   0.63%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│   23.6    24.4  0.7883   3.34%    12  coq-fourcolor/theories/proof/job486to489.v.html                                               │
│   23.2    24.0  0.7729   3.33%    12  coq-fourcolor/theories/proof/job295to298.v.html                                               │
│   22.5    23.3  0.7601   3.37%    79  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html            │
│   17.7    18.4  0.7000   3.95%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                     │
│   47.7    48.4  0.6915   1.45%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                   │
│   8.93    9.62  0.6888   7.71%   434  coq-mathcomp-odd-order/theories/PFsection12.v.html                                            │
│ 40.718  41.388  0.6700   1.65%   834  coq-vst/veric/binop_lemmas4.v.html                                                            │
│ 31.422  32.068  0.6460   2.06%    97  coq-vst/veric/binop_lemmas5.v.html                                                            │
│   3.68    4.31  0.6238  16.94%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                 │
│   2.23    2.86  0.6220  27.85%   607  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                     │
│   24.2    24.8  0.5943   2.46%    12  coq-fourcolor/theories/proof/job503to506.v.html                                               │
│   19.1    19.7  0.5718   2.99%    12  coq-fourcolor/theories/proof/job490to494.v.html                                               │
│   23.1    23.6  0.5367   2.32%    12  coq-fourcolor/theories/proof/job554to562.v.html                                               │
│   18.3    18.7  0.4269   2.33%    12  coq-fourcolor/theories/proof/job207to214.v.html                                               │
│   26.3    26.7  0.4216   1.60%    12  coq-fourcolor/theories/proof/job531to534.v.html                                               │
│   22.9    23.3  0.3906   1.70%    12  coq-fourcolor/theories/proof/job495to498.v.html                                               │
│   1.17    1.56  0.3871  33.10%  1252  rocq-metarocq-erasure/erasure/theories/ErasureFunction.v.html                                 │
│   27.0    27.4  0.3664   1.36%    12  coq-fourcolor/theories/proof/job287to290.v.html                                               │
│   12.1    12.5  0.3625   2.99%   930  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html         │
│   21.0    21.3  0.3408   1.62%   479  rocq-metarocq-erasure/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v.html              │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                     TOP 25 SPEED UPS                                                     │
│                                                                                                                          │
│  OLD      NEW      DIFF     %DIFF    Ln                 FILE                                                             │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  0.988     0.269  -0.7195  -72.79%    12  rocq-stdlib/theories/MSets/MSets.v.html                                        │
│   21.5      21.1  -0.4750   -2.21%   651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                      │
│ 34.637    34.206  -0.4310   -1.24%   147  coq-vst/veric/expr_lemmas4.v.html                                              │
│  0.545     0.123  -0.4227  -77.49%  1177  rocq-stdlib/theories/Reals/Abstract/ConstructiveReals.v.html                   │
│   2.68      2.32  -0.3621  -13.50%   240  coq-category-theory/Construction/Comma/Adjunction.v.html                       │
│  0.525     0.172  -0.3534  -67.26%   374  rocq-stdlib/theories/Sorting/SetoidList.v.html                                 │
│  0.934     0.601  -0.3334  -35.69%   170  rocq-stdlib/theories/Numbers/HexadecimalNat.v.html                             │
│   1.82      1.49  -0.3297  -18.13%   313  rocq-stdlib/theories/Strings/Byte.v.html                                       │
│   1.46      1.13  -0.3296  -22.52%  1142  rocq-stdlib/theories/FSets/FMapAVL.v.html                                      │
│    1.4     1.084  -0.3160  -22.57%   937  coq-vst/veric/binop_lemmas2.v.html                                             │
│   38.5      38.1  -0.3095   -0.80%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html │
│  3.991      3.76  -0.2310   -5.79%   241  coq-vst/floyd/subsume_funspec.v.html                                           │
│   19.6      19.3  -0.2289   -1.17%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html              │
│   29.7      29.4  -0.2258   -0.76%    12  coq-fourcolor/theories/proof/job165to189.v.html                                │
│  0.229   0.00767  -0.2216  -96.65%   111  coq-mathcomp-odd-order/theories/BGsection6.v.html                              │
│  0.222  0.000797  -0.2214  -99.64%   714  rocq-metarocq-erasure/erasure/theories/EReorderCstrs.v.html                    │
│  0.219   0.00343  -0.2155  -98.43%    77  rocq-metarocq-erasure/erasure/theories/EReorderCstrs.v.html                    │
│  0.220   0.00418  -0.2154  -98.10%    79  coq-mathcomp-odd-order/theories/BGsection9.v.html                              │
│  0.536     0.321  -0.2152  -40.13%   634  rocq-stdlib/theories/setoid_ring/Field_theory.v.html                           │
│  0.210   0.00374  -0.2058  -98.21%   228  rocq-metarocq-erasure/erasure/theories/Typed/TypeAnnotations.v.html            │
│  0.220    0.0207  -0.1993  -90.57%   123  rocq-metarocq-erasure/erasure/theories/EDeps.v.html                            │
│  0.201   0.00221  -0.1987  -98.90%   349  rocq-metarocq-erasure/erasure/theories/Typed/OptimizeCorrectness.v.html        │
│  0.216    0.0181  -0.1981  -91.61%   101  rocq-metarocq-safechecker/safechecker/theories/PCUICTypeChecker.v.html         │
│  0.197  0.000550  -0.1969  -99.72%   136  rocq-metarocq-safechecker/safechecker/theories/PCUICSafeChecker.v.html         │
│  0.416     0.219  -0.1968  -47.31%   411  rocq-metarocq-erasure/erasure/theories/Typed/Erasure.v.html                    │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

ppedrot · 2025-09-11T16:23:16Z

There is some observable slowdown, but to some extent it's unavoidable since we now have to stuff in the environment. I don't think I have immediate plans to remove the canonical part of names but maybe it's something we have to consider if we want to pursue in this direction. What do people think about the severity of the slowdown?

ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 7, 2025

coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 7, 2025

ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 10, 2025

ppedrot added 2 commits September 10, 2025 09:48

Actually rely on the environment to compute canonical data.

e91c345

Small optimization of canonical equality check.

07afb68

We first check for label equality, which is fast, before trying to normalize then name. The kernel guarantees that aliased names have the same label, so this is sound.

ppedrot force-pushed the environ-implement-canord-quotient branch from 1ba74c7 to 07afb68 Compare September 10, 2025 07:48

coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 10, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Actually rely on the environment to compute canonical data. #21075

Actually rely on the environment to compute canonical data. #21075

Uh oh!

ppedrot commented Sep 7, 2025

Uh oh!

ppedrot commented Sep 7, 2025

Uh oh!

coqbot-app bot commented Sep 7, 2025

Uh oh!

ppedrot commented Sep 10, 2025

Uh oh!

ppedrot commented Sep 10, 2025

Uh oh!

coqbot-app bot commented Sep 10, 2025

Uh oh!

ppedrot commented Sep 11, 2025

Uh oh!

Uh oh!

Actually rely on the environment to compute canonical data. #21075

Are you sure you want to change the base?

Actually rely on the environment to compute canonical data. #21075

Uh oh!

Conversation

ppedrot commented Sep 7, 2025

Uh oh!

ppedrot commented Sep 7, 2025

Uh oh!

coqbot-app bot commented Sep 7, 2025

Uh oh!

ppedrot commented Sep 10, 2025

Uh oh!

ppedrot commented Sep 10, 2025

Uh oh!

coqbot-app bot commented Sep 10, 2025

Uh oh!

ppedrot commented Sep 11, 2025

Uh oh!

Uh oh!