Inline redflags logic in CClosure. #21353

rlepigre · 2025-11-22T20:44:07Z

This is another experiment that @Janno and I ran in #17839, which improved performance quite a bit. This is orthogonal to #21352, and makes it so that reduction flag queries on the hot paths of CClosure are inlined.

SkySkimmer · 2025-11-22T20:53:30Z

@coqbot run full ci

SkySkimmer · 2025-11-22T20:53:57Z

@coqbot bench

rlepigre · 2025-11-23T18:59:53Z

The initial version is a performance regression, probably due to the costly translation function. Rebasing on #21352, to see what happens if we just expose the implementation details of the bitfield-represented flags.

rlepigre · 2025-11-23T19:00:03Z

@coqbot bench

coqbot-app · 2025-11-23T19:29:43Z

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│ coq-neural-net-interp-computed-lite │  236.26   240.47  -1.75 │  2266529999062   2266182558074   0.02 │  846936   846912   0.00 │
│                           rocq-elpi │   15.75    15.92  -1.07 │   111917979757    111883915508   0.03 │  572800   572584   0.04 │
│                        rocq-bignums │   24.73    24.88  -0.60 │   158072579614    157137533111   0.60 │  460168   457988   0.48 │
│                        rocq-runtime │   74.11    74.42  -0.42 │   538101564631    538004271428   0.02 │  510356   513848  -0.68 │
│          rocq-metarocq-translations │   15.48    15.53  -0.32 │   109370119318    109416228780  -0.04 │  779924   774528   0.70 │
│              rocq-metarocq-template │   81.36    81.60  -0.29 │   561008027887    560172450471   0.15 │ 1027060  1026392   0.07 │
│               coq-engine-bench-lite │  127.21   127.51  -0.24 │   948967387137    949552043141  -0.06 │ 1175876  1085036   8.37 │
│                         rocq-stdlib │  445.49   446.34  -0.19 │  1539607525584   1535260844323   0.28 │  635156   628452   1.07 │
│          coq-performance-tests-lite │  900.17   901.07  -0.10 │  7265878564526   7257592866744   0.11 │ 2203296  2203592  -0.01 │
│                       coq-fourcolor │ 1362.64  1362.91  -0.02 │ 12558332212043  12553761511378   0.04 │ 1401744  1401680   0.00 │
│         coq-rewriter-perf-SuperFast │  478.25   477.65   0.13 │  3746719168464   3729775799139   0.45 │ 1247972  1238916   0.73 │
│                    coq-fiat-parsers │  276.00   275.63   0.13 │  2117617622842   2112206632179   0.26 │ 2041052  2034516   0.32 │
│                        coq-compcert │  299.42   298.85   0.19 │  1961581685617   1953673154135   0.40 │ 1194004  1291620  -7.56 │
│                 rocq-metarocq-pcuic │  625.39   624.09   0.21 │  4000067080541   3983473831932   0.42 │ 1940756  1892844   2.53 │
│        coq-fiat-crypto-with-bedrock │ 7202.63  7181.55   0.29 │ 59692069354570  59521917887757   0.29 │ 3273524  3148356   3.98 │
│                 coq-category-theory │  582.07   579.80   0.39 │  4307359521268   4294293185530   0.30 │  992560   921256   7.74 │
│                  rocq-mathcomp-boot │   39.07    38.91   0.41 │   230885689618    230366125378   0.23 │  744596   746680  -0.28 │
│                           coq-color │  230.40   229.41   0.43 │  1456365567124   1452000909774   0.30 │ 1157656  1136404   1.87 │
│               rocq-metarocq-erasure │  473.25   471.16   0.44 │  3246042325373   3236118699911   0.31 │ 1901524  1918972  -0.91 │
│                            coq-hott │  159.29   158.55   0.47 │  1095222044564   1091582018075   0.33 │  491740   471300   4.34 │
│                    coq-math-classes │   82.81    82.40   0.50 │   503474024604    502368901463   0.22 │  515124   515044   0.02 │
│                        coq-rewriter │  332.94   331.23   0.52 │  2486603908127   2478097495159   0.34 │ 1499012  1509480  -0.69 │
│                rocq-metarocq-common │   40.59    40.33   0.64 │   261153239677    260017091775   0.44 │  912628   896000   1.86 │
│                            coq-corn │  650.70   646.51   0.65 │  4389698490723   4375003717724   0.34 │  761000   734900   3.55 │
│                      coq-coquelicot │   46.38    46.08   0.65 │   272439880700    271942507732   0.18 │  843708   843800  -0.01 │
│                   coq-iris-examples │  365.50   362.98   0.69 │  2412204869587   2404120582250   0.34 │ 1124724  1125236  -0.05 │
│                        coq-coqprime │   52.92    52.39   1.01 │   360236449041    358973446303   0.35 │  822804   822476   0.04 │
│                           coq-verdi │   43.05    42.61   1.03 │   287127122657    285144530282   0.70 │  525120   527408  -0.43 │
│                         coq-coqutil │   46.67    46.17   1.08 │   290117693452    289051086028   0.37 │  562992   560380   0.47 │
│              rocq-mathcomp-fingroup │   26.69    26.40   1.10 │   174267511644    172272549934   1.16 │  600744   602980  -0.37 │
│              rocq-mathcomp-solvable │  103.97   102.79   1.15 │   722184665982    716219377763   0.83 │ 1529368  1527164   0.14 │
│                      coq-verdi-raft │  499.08   493.20   1.19 │  3455113112953   3420529327891   1.01 │  818164   817312   0.10 │
│               coq-mathcomp-analysis │ 1058.61  1045.94   1.21 │  7950486832503   7898622037459   0.66 │ 2588888  2586928   0.08 │
│                       coq-fiat-core │   55.32    54.64   1.24 │   335898198512    335491981229   0.12 │  481896   480752   0.24 │
│               rocq-mathcomp-algebra │  330.08   325.93   1.27 │  2440196579480   2432219813907   0.33 │ 2053632  2049220   0.22 │
│                      rocq-equations │    8.74     8.63   1.27 │    59904847616     59871521236   0.06 │  398328   396892   0.36 │
│           rocq-metarocq-safechecker │  312.47   308.30   1.35 │  2324114667647   2318437314542   0.24 │ 1871816  1874260  -0.13 │
│                 rocq-metarocq-utils │   23.86    23.54   1.36 │   154051984900    153679859862   0.24 │  588664   592840  -0.70 │
│                 rocq-mathcomp-order │   81.97    80.83   1.41 │   602995807105    601990841011   0.17 │ 2062080  2060208   0.09 │
│              coq-mathcomp-odd-order │  608.95   600.30   1.44 │  4391259451370   4345006988977   1.06 │ 3318324  3401168  -2.44 │
│             rocq-mathcomp-character │  101.46    99.90   1.56 │   717215685983    712411980299   0.67 │ 2128780  2130644  -0.09 │
│                        coq-bedrock2 │  355.33   349.41   1.69 │  2958779839115   2911423968829   1.63 │  830708   851064  -2.39 │
│                         coq-unimath │ 1816.76  1780.00   2.07 │ 15087384120873  14816205446111   1.83 │ 1150680  1094620   5.12 │
│                 rocq-mathcomp-field │  191.22   186.84   2.34 │  1434907826213   1427276270262   0.53 │ 2781360  2792812  -0.41 │
│                             coq-vst │  847.08   827.03   2.42 │  6430266556195   6281909622084   2.36 │ 2102360  2163744  -2.84 │
│                           rocq-core │    6.66     6.50   2.46 │    41103256140     41044129796   0.14 │  456900   454984   0.42 │
│             rocq-mathcomp-ssreflect │    1.18     1.15   2.61 │     8313508009      8314050486  -0.01 │  862856   862868  -0.00 │
│                            coq-core │    2.96     2.88   2.78 │    19720215691     19685521333   0.18 │  106320   106100   0.21 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                               TOP 25 SLOW DOWNS                                                               │
│                                                                                                                                               │
│  OLD     NEW     DIFF   %DIFF    Ln                      FILE                                                                                 │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│    173     178  4.6918   2.71%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│   49.2    52.0  2.8083   5.71%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                             │
│   24.1    26.6  2.5689  10.68%   550  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                         │
│   24.1    26.7  2.5635  10.63%   550  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html       │
│   63.3    65.4  2.1090   3.33%   608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                             │
│ 34.775  36.761  1.9860   5.71%   147  coq-vst/veric/expr_lemmas4.v.html                                                                       │
│ 33.942  35.751  1.8090   5.33%   194  coq-vst/veric/expr_lemmas4.v.html                                                                       │
│   26.6    28.3  1.7431   6.55%   374  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                             │
│   26.6    28.3  1.6961   6.36%   375  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                             │
│   64.0    65.7  1.6947   2.65%   608  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html           │
│   21.1    22.3  1.2649   6.01%   338  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                             │
│   1.34    2.57  1.2319  92.02%   549  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                           │
│ 15.358  16.578  1.2200   7.94%  1223  coq-vst/floyd/Component.v.html                                                                          │
│ 15.363  16.531  1.1680   7.60%  1209  coq-vst/floyd/Component.v.html                                                                          │
│   16.5    17.7  1.1143   6.74%   905  coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html                                    │
│   12.1    13.1  1.0101   8.33%    97  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/HValuedSets.v.html                                    │
│ 15.392  16.398  1.0060   6.54%  1515  coq-vst/floyd/VSU.v.html                                                                                │
│   82.2    83.1  0.8496   1.03%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 │
│   2.47    3.27  0.7972  32.29%    34  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│ 10.602  11.389  0.7870   7.42%   985  coq-vst/floyd/closed_lemmas.v.html                                                                      │
│   21.8    22.6  0.7862   3.61%    49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 │
│  7.444   8.086  0.6420   8.62%  1206  coq-vst/floyd/Component.v.html                                                                          │
│  7.497   8.108  0.6110   8.15%  1506  coq-vst/floyd/Component.v.html                                                                          │
│  7.481   8.083  0.6020   8.05%  1208  coq-vst/floyd/Component.v.html                                                                          │
│  7.477   8.074  0.5970   7.98%  1221  coq-vst/floyd/Component.v.html                                                                          │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                               TOP 25 SPEED UPS                                                                │
│                                                                                                                                               │
│  OLD     NEW      DIFF     %DIFF   Ln                      FILE                                                                               │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   205       201  -4.3093   -2.10%    8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html         │
│  6.69      5.20  -1.4834  -22.18%  130  coq-category-theory/Functor/Strong/Product.v.html                                                     │
│  30.9      29.8  -1.0432   -3.38%  148  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                  │
│  18.9      17.9  -0.9560   -5.07%   32  coq-performance-tests-lite/src/pattern.v.html                                                         │
│  33.8      32.9  -0.9022   -2.67%  960  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                                  │
│  30.5      29.6  -0.8971   -2.94%  166  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                  │
│  30.6      29.7  -0.8475   -2.77%  139  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                  │
│  31.7      30.9  -0.8448   -2.66%  121  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                  │
│  30.6      29.8  -0.8412   -2.75%  157  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                  │
│  30.4      29.6  -0.8168   -2.69%  198  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                  │
│  30.6      29.8  -0.7625   -2.49%  214  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                  │
│  30.5      29.8  -0.7202   -2.36%  960  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                                  │
│  30.6      29.9  -0.6717   -2.20%  180  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                  │
│  1.64     0.973  -0.6672  -40.68%  813  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                             │
│  3.96      3.29  -0.6642  -16.78%  557  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                         │
│  18.7      18.1  -0.6565   -3.51%   31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                             │
│ 0.580   0.00717  -0.5730  -98.76%  145  coq-mathcomp-analysis/theories/ftc.v.html                                                             │
│ 0.528   0.00993  -0.5181  -98.12%  219  coq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v.html │
│ 0.520   0.00748  -0.5125  -98.56%  217  coq-mathcomp-analysis/theories/derive.v.html                                                          │
│ 0.511  0.000103  -0.5105  -99.98%  221  coq-mathcomp-analysis/theories/ess_sup_inf.v.html                                                     │
│ 0.514   0.00578  -0.5082  -98.88%  159  coq-mathcomp-analysis/theories/lebesgue_integral_theory/measurable_fun_approximation.v.html           │
│ 0.538    0.0316  -0.5060  -94.13%  188  coq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_under.v.html                │
│  30.1      29.6  -0.5031   -1.67%  671  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                                  │
│ 0.495   0.00176  -0.4932  -99.64%  271  coq-mathcomp-analysis/theories/sequences.v.html                                                       │
│ 0.492  0.000732  -0.4912  -99.85%   89  coq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_Rintegral.v.html                     │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

coqbot-app · 2025-11-24T08:50:58Z

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                      rocq-equations │    8.62     8.85  -2.60 │    59869804068     59878500624  -0.01 │  401984   397372   1.16 │
│                            coq-core │    2.92     2.99  -2.34 │    19687077623     19681601219   0.03 │  106076   106348  -0.26 │
│              rocq-mathcomp-fingroup │   26.25    26.55  -1.13 │   171978798765    172262181223  -0.16 │  598624   604520  -0.98 │
│                      coq-coquelicot │   45.93    46.36  -0.93 │   271744158155    271934128857  -0.07 │  845388   846408  -0.12 │
│                         rocq-stdlib │  444.17   447.96  -0.85 │  1534858919851   1535245339342  -0.03 │  629116   631144  -0.32 │
│                           rocq-elpi │   15.88    16.01  -0.81 │   111893880500    111884999704   0.01 │  572920   572852   0.01 │
│                  rocq-mathcomp-boot │   38.82    39.10  -0.72 │   230245248645    230335932373  -0.04 │  744644   746640  -0.27 │
│              rocq-metarocq-template │   81.08    81.64  -0.69 │   560163988316    560191739013  -0.00 │ 1026264  1027560  -0.13 │
│               coq-engine-bench-lite │  126.66   127.53  -0.68 │   945488625426    948450708811  -0.31 │ 1174244  1084900   8.24 │
│ coq-neural-net-interp-computed-lite │  237.20   238.79  -0.67 │  2265922189662   2266179435740  -0.01 │  845876   848228  -0.28 │
│                rocq-metarocq-common │   40.09    40.33  -0.60 │   259910126401    260037480083  -0.05 │  896352   894036   0.26 │
│                 rocq-metarocq-utils │   23.63    23.74  -0.46 │   153575934364    153715777441  -0.09 │  592360   593060  -0.12 │
│                 rocq-mathcomp-order │   81.17    81.50  -0.40 │   601914938238    601991469895  -0.01 │ 2060560  2059284   0.06 │
│                         coq-coqutil │   46.23    46.40  -0.37 │   288914564595    289025594382  -0.04 │  560672   560400   0.05 │
│        coq-fiat-crypto-with-bedrock │ 7156.73  7182.12  -0.35 │ 59344224489087  59520327137087  -0.30 │ 3142556  3125952   0.53 │
│                      coq-verdi-raft │  492.68   494.36  -0.34 │  3414269255317   3420432047454  -0.18 │  820232   821056  -0.10 │
│                        coq-rewriter │  329.96   331.03  -0.32 │  2476763503286   2478042800529  -0.05 │ 1496848  1509544  -0.84 │
│                 rocq-mathcomp-field │  187.56   188.15  -0.31 │  1426342813831   1427326642693  -0.07 │ 2768240  2789256  -0.75 │
│                   coq-iris-examples │  363.49   364.17  -0.19 │  2401423306456   2404081468933  -0.11 │ 1125436  1126196  -0.07 │
│                        coq-coqprime │   52.52    52.61  -0.17 │   359013316402    358983553131   0.01 │  822708   822736  -0.00 │
│               rocq-metarocq-erasure │  470.49   471.16  -0.14 │  3231367079463   3236115975763  -0.15 │ 1919896  1921892  -0.10 │
│                    coq-fiat-parsers │  275.40   275.70  -0.11 │  2110738733173   2112184143234  -0.07 │ 2041160  2034432   0.33 │
│               coq-mathcomp-analysis │ 1047.03  1047.87  -0.08 │  7898112565872   7899359814084  -0.02 │ 2590824  2586260   0.18 │
│                        rocq-runtime │   74.31    74.32  -0.01 │   537903067841    537969879176  -0.01 │  513360   513868  -0.10 │
│                           coq-color │  229.17   229.14   0.01 │  1451107628507   1452121837280  -0.07 │ 1135312  1137776  -0.22 │
│                            coq-corn │  647.00   646.91   0.01 │  4370015685336   4374908854475  -0.11 │  731828   735244  -0.46 │
│                       coq-fiat-core │   54.79    54.77   0.04 │   335322071968    335454016285  -0.04 │  481636   481788  -0.03 │
│             rocq-mathcomp-character │  100.51   100.47   0.04 │   711821224274    712345587175  -0.07 │ 2129112  2130444  -0.06 │
│                        rocq-bignums │   24.80    24.78   0.08 │   157156097601    157153145357   0.00 │  459192   457420   0.39 │
│                        coq-compcert │  298.74   298.46   0.09 │  1953083733127   1953762886341  -0.03 │ 1261800  1291844  -2.33 │
│         coq-rewriter-perf-SuperFast │  478.39   477.92   0.10 │  3726464641184   3729024693981  -0.07 │ 1268528  1273992  -0.43 │
│                       coq-fourcolor │ 1363.04  1361.69   0.10 │ 12551794730780  12553894509758  -0.02 │ 1401628  1401708  -0.01 │
│               rocq-mathcomp-algebra │  326.26   325.92   0.10 │  2431761381019   2432175170599  -0.02 │ 2054344  2046104   0.40 │
│                    coq-math-classes │   82.67    82.58   0.11 │   501850744028    502455806990  -0.12 │  514144   514352  -0.04 │
│                        coq-bedrock2 │  350.19   349.46   0.21 │  2906534015522   2911516137537  -0.17 │  833156   851220  -2.12 │
│                           coq-verdi │   42.86    42.76   0.23 │   284861418273    285138722191  -0.10 │  528660   524028   0.88 │
│              rocq-mathcomp-solvable │  103.04   102.79   0.24 │   715474004377    716140292318  -0.09 │ 1519240  1529040  -0.64 │
│                 rocq-metarocq-pcuic │  625.60   623.68   0.31 │  3978711666113   3983362751486  -0.12 │ 1903124  1895924   0.38 │
│                             coq-vst │  828.96   826.25   0.33 │  6282729834547   6282034270652   0.01 │ 2155596  2163832  -0.38 │
│                            coq-hott │  158.76   158.20   0.35 │  1090731656652   1091377105000  -0.06 │  490824   468352   4.80 │
│              coq-mathcomp-odd-order │  602.24   599.99   0.38 │  4336529085693   4345070460690  -0.20 │ 3343532  3400460  -1.67 │
│          coq-performance-tests-lite │  901.71   898.15   0.40 │  7255581039891   7257573388984  -0.03 │ 2202392  2203356  -0.04 │
│                 coq-category-theory │  581.29   578.99   0.40 │  4285097192695   4294880620229  -0.23 │  970788   917648   5.79 │
│           rocq-metarocq-safechecker │  310.54   309.02   0.49 │  2316639931431   2318413941606  -0.08 │ 1870632  1874564  -0.21 │
│                           rocq-core │    6.66     6.62   0.60 │    41034528382     41055967615  -0.05 │  454644   454624   0.00 │
│                         coq-unimath │ 1792.29  1779.93   0.69 │ 14801460105097  14815545036727  -0.10 │ 1109684  1096240   1.23 │
│             rocq-mathcomp-ssreflect │    1.19     1.18   0.85 │     8317454256      8314137882   0.04 │  863284   861616   0.19 │
│          rocq-metarocq-translations │   15.54    15.37   1.11 │   109261271899    109439677865  -0.16 │  775648   775460   0.02 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                TOP 25 SLOW DOWNS                                                                 │
│                                                                                                                                                  │
│   OLD      NEW     DIFF     %DIFF     Ln                      FILE                                                                               │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│     93.5    95.5  1.9480      2.08%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                       │
│     94.0    95.3  1.2218      1.30%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                       │
│     63.6    64.7  1.0902      1.71%   608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                           │
│     26.6    27.6  1.0042      3.78%   374  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                           │
│     26.7    27.6  0.9642      3.61%   375  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                           │
│     21.5    22.4  0.8873      4.12%   651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                             │
│     40.4    41.2  0.8491      2.10%  1423  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html      │
│     1.00    1.69  0.6924     69.17%   813  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                             │
│     64.0    64.6  0.6181      0.97%   716  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                                 │
│  0.00357   0.577  0.5739  16093.41%   142  coq-mathcomp-analysis/theories/ftc.v.html                                                             │
│     1.91    2.48  0.5718     29.91%    32  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                           │
│     24.0    24.5  0.5317      2.21%   550  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                       │
│  0.00423   0.517  0.5129  12133.55%   152  coq-mathcomp-analysis/theories/lebesgue_integral_theory/measurable_fun_approximation.v.html           │
│  0.00910   0.522  0.5125   5633.57%   215  coq-mathcomp-analysis/theories/derive.v.html                                                          │
│  0.00314   0.515  0.5116  16267.98%   218  coq-mathcomp-analysis/theories/ess_sup_inf.v.html                                                     │
│   0.0108   0.502  0.4911   4555.12%   187  coq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_under.v.html                │
│  0.00535   0.496  0.4907   9166.22%   113  coq-mathcomp-analysis/theories/derive.v.html                                                          │
│  0.00443   0.493  0.4885  11024.01%    54  coq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v.html │
│ 0.000876   0.488  0.4874  55636.99%    89  coq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_Rintegral.v.html                     │
│  0.00391   0.489  0.4852  12425.45%   175  coq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_definition.v.html           │
│ 0.000670   0.454  0.4538  67728.81%   660  rocq-mathcomp-character/character/mxrepresentation.v.html                                             │
│  0.00195   0.437  0.4353  22358.40%   146  rocq-mathcomp-algebra/algebra/spectral.v.html                                                         │
│     3.65    4.08  0.4331     11.87%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                         │
│   10.514  10.916  0.4020      3.82%   985  coq-vst/floyd/closed_lemmas.v.html                                                                    │
│  0.00925   0.393  0.3834   4143.40%   248  rocq-mathcomp-field/field/algebraics_fundamentals.v.html                                              │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                TOP 25 SPEED UPS                                                                 │
│                                                                                                                                                 │
│  OLD     NEW      DIFF     %DIFF   Ln                      FILE                                                                                 │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  65.2      62.4  -2.7026   -4.15%  608  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html           │
│   174       172  -2.3136   -1.33%  233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  6.86      5.19  -1.6717  -24.35%  130  coq-category-theory/Functor/Strong/Product.v.html                                                       │
│   203       202  -1.3862   -0.68%    8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html           │
│  82.8      81.8  -1.0400   -1.26%   48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 │
│  33.6      32.6  -1.0103   -3.01%  960  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                                    │
│  30.4      29.4  -0.9325   -3.07%  960  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                                    │
│  18.6      17.7  -0.9294   -4.99%   31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                               │
│  93.4      92.6  -0.8494   -0.91%   20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                             │
│  3.02      2.27  -0.7484  -24.76%  607  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                               │
│  42.7      41.9  -0.7212   -1.69%   50  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│  43.3      42.6  -0.6755   -1.56%   50  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│  30.7      30.0  -0.6630   -2.16%  198  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│  18.7      18.1  -0.6228   -3.33%   32  coq-performance-tests-lite/src/pattern.v.html                                                           │
│  48.1      47.5  -0.6071   -1.26%  260  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                           │
│  30.8      30.2  -0.5904   -1.92%  166  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│  30.8      30.2  -0.5893   -1.91%  214  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│ 0.582   0.00728  -0.5749  -98.75%  145  coq-mathcomp-analysis/theories/ftc.v.html                                                               │
│  30.9      30.4  -0.5621   -1.82%  148  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│  30.8      30.2  -0.5263   -1.71%  157  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│ 0.516  0.000100  -0.5159  -99.98%  221  coq-mathcomp-analysis/theories/ess_sup_inf.v.html                                                       │
│ 0.521   0.00727  -0.5137  -98.60%  217  coq-mathcomp-analysis/theories/derive.v.html                                                            │
│ 0.513   0.00586  -0.5076  -98.86%  159  coq-mathcomp-analysis/theories/lebesgue_integral_theory/measurable_fun_approximation.v.html             │
│ 0.534    0.0305  -0.5038  -94.28%  188  coq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_under.v.html                  │
│  31.8      31.3  -0.5024   -1.58%  121  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

kernel/redFlags.mli

ppedrot · 2025-11-26T12:55:41Z

@coqbot run full ci

rlepigre requested a review from a team as a code owner November 22, 2025 20:44

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Nov 22, 2025

coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Nov 22, 2025

rlepigre force-pushed the cclosure-redflags branch from 90c541c to e79aeb4 Compare November 23, 2025 18:57

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Nov 23, 2025

rlepigre force-pushed the cclosure-redflags branch from e79aeb4 to 2ad8607 Compare November 26, 2025 12:53

rlepigre commented Nov 26, 2025

View reviewed changes

kernel/redFlags.mli Outdated Show resolved Hide resolved

ppedrot self-assigned this Nov 26, 2025

coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Nov 26, 2025

Inline redflags logic in CClosure.

49c37f4

rlepigre force-pushed the cclosure-redflags branch from 2ad8607 to 49c37f4 Compare November 29, 2025 08:56

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Nov 29, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Inline redflags logic in CClosure. #21353

Inline redflags logic in CClosure. #21353

rlepigre commented Nov 22, 2025

Uh oh!

SkySkimmer commented Nov 22, 2025

Uh oh!

SkySkimmer commented Nov 22, 2025

Uh oh!

rlepigre commented Nov 23, 2025

Uh oh!

rlepigre commented Nov 23, 2025

Uh oh!

coqbot-app bot commented Nov 23, 2025

Uh oh!

coqbot-app bot commented Nov 24, 2025

Uh oh!

Uh oh!

ppedrot commented Nov 26, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Inline redflags logic in CClosure. #21353

Are you sure you want to change the base?

Inline redflags logic in CClosure. #21353

Conversation

rlepigre commented Nov 22, 2025

Uh oh!

SkySkimmer commented Nov 22, 2025

Uh oh!

SkySkimmer commented Nov 22, 2025

Uh oh!

rlepigre commented Nov 23, 2025

Uh oh!

rlepigre commented Nov 23, 2025

Uh oh!

coqbot-app bot commented Nov 23, 2025

Uh oh!

coqbot-app bot commented Nov 24, 2025

Uh oh!

Uh oh!

ppedrot commented Nov 26, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants