Update opam version used in bench (2.1.3 -> 2.3.0) + cleanup script parts about job count #20687
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
we don't run the test suite anymore
hopefully those comments about opam ignoring -j are obsolete with opam 2.3
|
🏁 Bench results: 🐢 Top 25 slow downs┌────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 0.455 0.483 0.0280 6.16% 73 rocq-stdlib/theories/Numbers/HexadecimalString.v.html │ │ 0.681 0.703 0.0218 3.19% 1142 rocq-stdlib/theories/FSets/FMapAVL.v.html │ │ 0.757 0.772 0.0147 1.94% 530 rocq-stdlib/theories/Strings/PString.v.html │ │ 0.284 0.298 0.0132 4.65% 2109 rocq-stdlib/theories/FSets/FMapFacts.v.html │ │ 0.128 0.140 0.0119 9.30% 16 rocq-stdlib/theories/Numbers/DecimalPos.v.html │ │ 0.0789 0.0904 0.0115 14.64% 11 rocq-stdlib/theories/QArith/QArith_base.v.html │ │ 0.261 0.271 0.0105 4.02% 75 rocq-stdlib/theories/Numbers/HexadecimalString.v.html │ │ 0.374 0.384 0.0105 2.80% 736 rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyReals.v.html │ │ 0.0130 0.0222 0.0092 70.32% 17 rocq-stdlib/theories/setoid_ring/Ncring_polynom.v.html │ │ 0.109 0.118 0.0092 8.48% 26 rocq-stdlib/theories/Numbers/Integer/Abstract/ZProperties.v.html │ │ 0.473 0.482 0.0089 1.89% 572 rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 0.118 0.126 0.0082 6.99% 110 rocq-stdlib/theories/Numbers/HexadecimalPos.v.html │ │ 0.0541 0.0616 0.0076 14.03% 717 rocq-stdlib/theories/micromega/EnvRing.v.html │ │ 0.137 0.143 0.0068 5.00% 11 rocq-stdlib/theories/Reals/SeqSeries.v.html │ │ 0.0724 0.0791 0.0067 9.20% 75 rocq-stdlib/theories/FSets/FMapFullAVL.v.html │ │ 0.178 0.184 0.0066 3.72% 555 rocq-stdlib/theories/Reals/Rfunctions.v.html │ │ 0.137 0.144 0.0065 4.77% 11 rocq-stdlib/theories/Reals/Rsigma.v.html │ │ 0.137 0.144 0.0064 4.63% 11 rocq-stdlib/theories/Reals/Cauchy_prod.v.html │ │ 0.0409 0.0471 0.0063 15.34% 159 rocq-stdlib/theories/setoid_ring/RealField.v.html │ │ 0.134 0.140 0.0063 4.68% 1 rocq-stdlib/theories/micromega/Fourier.v.html │ │ 0.0737 0.0800 0.0062 8.46% 28 rocq-stdlib/theories/Structures/OrdersEx.v.html │ │ 0.144 0.150 0.0062 4.28% 16 rocq-stdlib/theories/Reals/R_Ifp.v.html │ │ 0.0799 0.0859 0.0060 7.56% 766 rocq-stdlib/theories/micromega/EnvRing.v.html │ │ 0.0428 0.0487 0.0059 13.72% 66 rocq-stdlib/theories/Reals/Cauchy_prod.v.html │ │ 0.0384 0.0442 0.0058 15.12% 101 rocq-stdlib/theories/Reals/SeqSeries.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌─────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 0.0533 0.000123 -0.0532 -99.77% 1477 rocq-stdlib/theories/Reals/RIneq.v.html │ │ 0.0183 0.000330 -0.0180 -98.20% 1034 rocq-stdlib/theories/Numbers/Natural/Abstract/NBits.v.html │ │ 0.263 0.249 -0.0143 -5.43% 21 rocq-stdlib/theories/MSets/MSetPositive.v.html │ │ 0.250 0.236 -0.0139 -5.55% 58 rocq-stdlib/theories/Numbers/DecimalString.v.html │ │ 0.229 0.215 -0.0136 -5.94% 637 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 0.242 0.229 -0.0128 -5.31% 12 rocq-stdlib/theories/MSets/MSets.v.html │ │ 0.0216 0.00878 -0.0128 -59.31% 134 rocq-stdlib/theories/ZArith/ZModOffset.v.html │ │ 0.0108 0.000053 -0.0107 -99.51% 1112 rocq-stdlib/theories/NArith/BinNat.v.html │ │ 0.220 0.209 -0.0107 -4.88% 707 rocq-stdlib/theories/MSets/MSetList.v.html │ │ 0.0360 0.0256 -0.0104 -28.99% 133 rocq-stdlib/theories/ZArith/ZModOffset.v.html │ │ 0.351 0.341 -0.0097 -2.77% 829 rocq-stdlib/theories/setoid_ring/Ring_polynom.v.html │ │ 0.288 0.278 -0.0096 -3.35% 487 rocq-stdlib/theories/MSets/MSetWeakList.v.html │ │ 0.00968 0.000563 -0.0091 -94.19% 165 rocq-stdlib/theories/Numbers/NatInt/NZGcd.v.html │ │ 0.314 0.305 -0.0081 -2.57% 83 rocq-stdlib/theories/Numbers/Cyclic/Int63/Sint63.v.html │ │ 0.0910 0.0834 -0.0076 -8.38% 91 rocq-stdlib/theories/Numbers/DecimalPos.v.html │ │ 0.143 0.136 -0.0075 -5.22% 11 rocq-stdlib/theories/Reals/Rregisternames.v.html │ │ 0.0699 0.0628 -0.0071 -10.13% 49 rocq-stdlib/theories/micromega/RMicromega.v.html │ │ 0.148 0.141 -0.0067 -4.55% 11 rocq-stdlib/theories/Reals/Rtrigo_def.v.html │ │ 0.102 0.0956 -0.0066 -6.48% 206 rocq-stdlib/theories/Reals/ClassicalConstructiveReals.v.html │ │ 0.215 0.209 -0.0066 -3.05% 60 rocq-stdlib/theories/Numbers/DecimalString.v.html │ │ 0.0993 0.0928 -0.0064 -6.47% 212 rocq-stdlib/theories/Reals/ClassicalConstructiveReals.v.html │ │ 0.0519 0.0455 -0.0063 -12.22% 14 rocq-stdlib/theories/ZArith/ZArith.v.html │ │ 0.362 0.356 -0.0062 -1.72% 422 rocq-stdlib/theories/MSets/MSetList.v.html │ │ 0.0421 0.0360 -0.0061 -14.41% 53 rocq-stdlib/theories/Reals/Qreals.v.html │ │ 0.111 0.105 -0.0061 -5.49% 185 rocq-stdlib/theories/Reals/ClassicalConstructiveReals.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
|
🏁 Bench results: 🐢 Top 25 slow downs┌───────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 0.000132 0.0540 0.0539 40796.97% 1477 rocq-stdlib/theories/Reals/RIneq.v.html │ │ 0.000089 0.0392 0.0391 43974.16% 120 rocq-stdlib/theories/Reals/Runcountable.v.html │ │ 0.000544 0.0249 0.0243 4472.06% 688 rocq-stdlib/theories/FSets/FMapWeakList.v.html │ │ 0.274 0.290 0.0161 5.88% 474 rocq-stdlib/theories/MSets/MSetWeakList.v.html │ │ 0.833 0.847 0.0142 1.71% 313 rocq-stdlib/theories/Strings/Byte.v.html │ │ 0.00266 0.0143 0.0117 438.27% 234 rocq-stdlib/theories/Numbers/NatInt/NZPow.v.html │ │ 0.286 0.298 0.0115 4.02% 2109 rocq-stdlib/theories/FSets/FMapFacts.v.html │ │ 0.00187 0.0128 0.0109 581.89% 500 rocq-stdlib/theories/Numbers/NatInt/NZDiv.v.html │ │ 0.121 0.131 0.0105 8.70% 54 rocq-stdlib/theories/Strings/Byte.v.html │ │ 0.273 0.283 0.0098 3.59% 487 rocq-stdlib/theories/MSets/MSetWeakList.v.html │ │ 0.0407 0.0504 0.0096 23.63% 202 rocq-stdlib/theories/Numbers/NatInt/NZParity.v.html │ │ 0.464 0.473 0.0094 2.04% 73 rocq-stdlib/theories/Numbers/HexadecimalString.v.html │ │ 0.00682 0.0149 0.0081 119.07% 81 rocq-stdlib/theories/Reals/Cauchy_prod.v.html │ │ 0.00566 0.0136 0.0079 140.51% 410 rocq-stdlib/theories/Numbers/NatInt/NZSqrt.v.html │ │ 0.107 0.114 0.0065 6.04% 386 rocq-stdlib/theories/Strings/PString.v.html │ │ 0.0730 0.0792 0.0062 8.51% 28 rocq-stdlib/theories/Structures/OrdersEx.v.html │ │ 0.0442 0.0504 0.0061 13.86% 49 rocq-stdlib/theories/Reals/Rprod.v.html │ │ 0.0409 0.0470 0.0061 14.89% 94 rocq-stdlib/theories/Reals/Rtrigo_def.v.html │ │ 0.218 0.224 0.0061 2.80% 705 rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html │ │ 0.210 0.216 0.0057 2.71% 707 rocq-stdlib/theories/MSets/MSetList.v.html │ │ 0.0409 0.0463 0.0054 13.32% 60 rocq-stdlib/theories/Reals/PSeries_reg.v.html │ │ 0.0932 0.0986 0.0054 5.74% 262 rocq-stdlib/theories/MSets/MSetProperties.v.html │ │ 0.133 0.139 0.0054 4.06% 146 rocq-stdlib/theories/FSets/FMapFullAVL.v.html │ │ 0.160 0.165 0.0054 3.40% 313 rocq-stdlib/theories/Reals/Abstract/ConstructiveLUB.v.html │ │ 0.0343 0.0395 0.0052 15.09% 208 rocq-stdlib/theories/Reals/RIneq.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 2.26 2.16 -0.0926 -4.10% 492 rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 1.06 1.02 -0.0389 -3.67% 204 rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html │ │ 0.467 0.447 -0.0204 -4.36% 408 < 8E5A a href="https://coq.gitlabpages.inria.fr/-/coq/-/jobs/5807904/artifacts/_bench/html/rocq-stdlib/theories/MSets/MSetAVL.v.html#L408" rel="nofollow">rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 0.0180 0.000329 -0.0177 -98.18% 1034 rocq-stdlib/theories/Numbers/Natural/Abstract/NBits.v.html │ │ 0.493 0.476 -0.0168 -3.40% 572 rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 0.240 0.224 -0.0158 -6.61% 12 rocq-stdlib/theories/MSets/MSets.v.html │ │ 0.393 0.380 -0.0129 -3.29% 206 rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html │ │ 0.365 0.353 -0.0122 -3.34% 198 rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html │ │ 0.0591 0.0484 -0.0107 -18.13% 356 rocq-stdlib/theories/Numbers/NatInt/NZSqrt.v.html │ │ 0.442 0.432 -0.0100 -2.27% 387 rocq-stdlib/theories/Reals/Raxioms.v.html │ │ 0.00957 0.000533 -0.0090 -94.43% 165 rocq-stdlib/theories/Numbers/NatInt/NZGcd.v.html │ │ 0.102 0.0942 -0.0078 -7.63% 99 rocq-stdlib/theories/ZArith/Zbitwise.v.html │ │ 0.312 0.304 -0.0077 -2.47% 83 rocq-stdlib/theories/Numbers/Cyclic/Int63/Sint63.v.html │ │ 0.0850 0.0779 -0.0072 -8.43% 78 rocq-stdlib/theories/Reals/Raxioms.v.html │ │ 0.0723 0.0660 -0.0063 -8.69% 76 rocq-stdlib/theories/Reals/Cauchy/ConstructiveRcomplete.v.html │ │ 0.114 0.108 -0.0062 -5.47% 26 rocq-stdlib/theories/Numbers/Integer/Abstract/ZProperties.v.html │ │ 0.0684 0.0623 -0.0062 -8.99% 49 rocq-stdlib/theories/micromega/RMicromega.v.html │ │ 0.0110 0.00490 -0.0061 -55.53% 257 rocq-stdlib/theories/Numbers/NatInt/NZParity.v.html │ │ 0.183 0.177 -0.0060 -3.28% 555 rocq-stdlib/theories/Reals/Rfunctions.v.html │ │ 0.0458 0.0400 -0.0059 -12.81% 794 rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 0.129 0.123 -0.0059 -4.56% 199 rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html │ │ 0.141 0.135 -0.0059 -4.16% 11 rocq-stdlib/theories/Reals/Rtrigo.v.html │ │ 0.00615 0.000328 -0.0058 -94.66% 2205 rocq-stdlib/theories/Lists/List.v.html │ │ 0.0827 0.0769 -0.0058 -7.02% 676 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 0.0968 0.0912 -0.0057 -5.84% 115 rocq-stdlib/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.