First-order approximation for polymorphic hints. #21164
Open
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
ppedrot
added
request: full CI
coqbot-app
bot
removed
the
request: full CI
Member
Author
|
@coqbot bench |
Contributor
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 200 202 1.7598 0.88% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 0.924 1.77 0.8474 91.74% 813 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 0.189 0.682 0.4935 261.55% 374 rocq-stdlib/theories/Sorting/SetoidList.v.html │ │ 0.643 1.11 0.4711 73.22% 736 rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyReals.v.html │ │ 1.08 1.46 0.3819 35.45% 1142 rocq-stdlib/theories/FSets/FMapAVL.v.html │ │ 1.22 1.53 0.3153 25.94% 408 rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 26.3 26.6 0.3004 1.14% 12 coq-fourcolor/theories/proof/job190to206.v.html │ │ 0.678 0.947 0.2689 39.63% 1290 rocq-stdlib/theories/Logic/ChoiceFacts.v.html │ │ 0.0759 0.333 0.2575 339.38% 585 rocq-stdlib/theories/Strings/Byte.v.html │ │ 23.0 23.2 0.2402 1.05% 79 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html │ │ 0.354 0.591 0.2369 66.90% 11 rocq-stdlib/theories/Numbers/DecimalString.v.html │ │ 26.5 26.7 0.2237 0.85% 12 coq-fourcolor/theories/proof/job399to438.v.html │ │ 0.449 0.663 0.2135 47.53% 624 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 1.45 1.66 0.2118 14.63% 75 rocq-stdlib/theories/Numbers/HexadecimalString.v.html │ │ 0.000110 0.211 0.2109 191686.36% 8 rocq-metarocq-erasure/erasure/theories/Typed/ExtractionCorrectness.v.html │ │ 0.176 0.386 0.2098 118.92% 586 rocq-stdlib/theories/Strings/Byte.v.html │ │ 0.452 0.660 0.2083 46.12% 518 rocq-metarocq-pcuic/pcuic/theories/PCUICCumulProp.v.html │ │ 0.0873 0.294 0.2064 236.31% 260 rocq-stdlib/theories/Reals/Abstract/ConstructiveAbs.v.html │ │ 0.834 1.04 0.2045 24.53% 816 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 0.0125 0.217 0.2045 1631.76% 32 rocq-metarocq-erasure/erasure/theories/Typed/Erasure.v.html │ │ 32.7 32.9 0.1996 0.61% 12 coq-fourcolor/theories/proof/job439to465.v.html │ │ 0.000894 0.193 0.1917 21444.07% 280 rocq-metarocq-erasure/erasure/theories/ErasureCorrectness.v.html │ │ 0.0316 0.221 0.1897 599.56% 355 rocq-metarocq-pcuic/pcuic/theories/PCUICSpine.v.html │ │ 0.444 0.632 0.1886 42.49% 13 rocq-stdlib/theories/FSets/FMapPositive.v.html │ │ 0.0120 0.200 0.1877 1567.47% 395 rocq-metarocq-erasure/erasure/theories/EGenericGlobalMap.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 97.1 95.6 -1.5692 -1.62% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 7.97 6.90 -1.0720 -13.45% 149 coq-category-theory/Structure/Monoid.v.html │ │ 97.0 96.2 -0.8232 -0.85% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 4.15 3.44 -0.7110 -17.13% 250 rocq-metarocq-erasure/erasure/theories/EWellformed.v.html │ │ 22.0 21.5 -0.5503 -2.50% 651 rocq-stdlib/theories/Zmod/ZmodBase.v.html │ │ 1.45 1.02 -0.4371 -30.05% 572 rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 7.89 7.48 -0.4077 -5.17% 602 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 2.77 2.40 -0.3671 -13.25% 240 coq-category-theory/Construction/Comma/Adjunction.v.html │ │ 25.4 25.0 -0.3240 -1.28% 12 coq-fourcolor/theories/proof/job299to302.v.html │ │ 3.72 3.40 -0.3209 -8.63% 196 rocq-stdlib/theories/ZArith/ZModOffset.v.html │ │ 21.2 20.9 -0.3112 -1.47% 479 rocq-metarocq-erasure/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v.html │ │ 0.709 0.399 -0.3105 -43.78% 615 rocq-stdlib/theories/setoid_ring/Field_theory.v.html │ │ 29.5 29.2 -0.2913 -0.99% 12 coq-fourcolor/theories/proof/job323to383.v.html │ │ 0.550 0.265 -0.2845 -51.74% 13 rocq-stdlib/theories/QArith/Qreduction.v.html │ │ 2.35 2.07 -0.2799 -11.90% 1351 rocq-metarocq-erasure/erasure/theories/ErasureCorrectness.v.html │ │ 3.01 2.73 -0.2771 -9.21% 120 coq-category-theory/Functor/Strong/Product.v.html │ │ 0.469 0.210 -0.2584 -55.15% 246 rocq-stdlib/theories/Structures/OrdersEx.v.html │ │ 9.72 9.47 -0.2537 -2.61% 978 coq-verdi-raft/theories/Raft/Linearizability.v.html │ │ 3.89 3.64 -0.2536 -6.52% 128 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 0.363 0.112 -0.2503 -69.04% 12 rocq-stdlib/theories/Reals/Abstract/ConstructiveAbs.v.html │ │ 0.662 0.417 -0.2447 -36.99% 260 rocq-metarocq-pcuic/pcuic/theories/PCUICCumulProp.v.html │ │ 1.44 1.19 -0.2418 -16.83% 2273 rocq-metarocq-erasure/erasure/theories/Typed/OptimizeCorrectness.v.html │ │ 0.232 0.000678 -0.2311 -99.71% 715 rocq-metarocq-erasure/erasure/theories/EReorderCstrs.v.html │ │ 31.4 31.2 -0.2308 -0.74% 12 coq-fourcolor/theories/proof/job254to270.v.html │ │ 0.575 0.348 -0.2275 -39.56% 719 rocq-stdlib/theories/MSets/MSetRBT.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
Member
Author
|
There is a clearly observable effect but I'm not sure it's worth the tweak. The new code is less complete as it commits early to universe instances. Anyway I'm closing this. |
coqbot-app
bot
added
the
needs: full CI
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
hint-refresh-firstorder-approx
branch
from
660eb8c to
0c52442
Compare
coqbot-app
bot
removed
request: full CI
Member
Author
|
Reopening this with the goal to actually merge it. |
ppedrot
added
kind: performance
coqbot-app
bot
added
needs: full CI
Contributor
|
@coqbot run full ci |
Contributor
|
The Is most of the speedup from aborting hints early or is from guiding unification to an easy and correct solution? |
tabareau
force-pushed
the
hint-refresh-firstorder-approx
branch
from
f6029c7 to
43e2c06
Compare
coqbot-app
bot
added
the
needs: full CI
Contributor
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
Contributor
|
The Hint Extern issue minimized looks like Set Universe Polymorphism.
Cumulative Class C@{u} (T:Type@{u}) : Type@{u} := {}.
Set Primitive Projections.
Record R@{u} := Build_R { T:>Type@{u}; R_C :: C@{u} T }.
Definition foo@{i j | i < j} (x:R@{i}) : C@{j} (T x) := _.
(* succeeds in master, fails in PR *)Note that |
|
In HoTT/Coq-HoTT#2318 (now merged) I found a way to avoid needing the |
Contributor
|
@coqbot bench |
Contributor
|
@jdchristensen the gain on coq-hott is not huge, but significant enough
|
Contributor
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 200 202 1.5856 0.79% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 38.7 39.7 0.9788 2.53% 236 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 38.1 39.0 0.8700 2.28% 224 coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html │ │ 3.94 4.38 0.4415 11.22% 492 rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 0.382 0.788 0.4059 106.37% 21 rocq-stdlib/theories/FSets/FMapAVL.v.html │ │ 0.367 0.770 0.4035 110.01% 1 rocq-stdlib/theories/Reals/Cauchy/ConstructiveExtra.v.html │ │ 21.2 21.6 0.3350 1.58% 651 rocq-stdlib/theories/Zmod/ZmodBase.v.html │ │ 3.23 3.55 0.3215 9.94% 213 rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html │ │ 0.933 1.24 0.3093 33.15% 408 rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 9.03 9.34 0.3064 3.39% 434 coq-mathcomp-odd-order/theories/PFsection12.v.html │ │ 0.372 0.641 0.2695 72.47% 14 rocq-stdlib/theories/extraction/ExtrOcamlZBigInt.v.html │ │ 0.0726 0.341 0.2686 369.99% 585 rocq-stdlib/theories/Strings/Byte.v.html │ │ 0.255 0.515 0.2603 102.20% 11 rocq-stdlib/theories/Strings/BinaryString.v.html │ │ 0.213 0.465 0.2517 118.18% 1166 rocq-stdlib/theories/Strings/Byte.v.html │ │ 48.5 48.7 0.2511 0.52% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 0.826 1.07 0.2484 30.06% 215 rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html │ │ 0.0751 0.283 0.2078 276.66% 215 rocq-stdlib/theories/Logic/Decidable.v.html │ │ 0.316 0.522 0.2055 64.96% 19 rocq-stdlib/theories/Sorting/Heap.v.html │ │ 0.00110 0.198 0.1972 17931.73% 189 rocq-metarocq-erasure/erasure/theories/ErasureFunctionProperties.v.html │ │ 0.210 0.405 0.1957 93.39% 11 rocq-stdlib/theories/setoid_ring/Field_tac.v.html │ │ 0.202 0.393 0.1910 94.74% 14 rocq-stdlib/theories/Numbers/Cyclic/Int63/Uint63.v.html │ │ 0.00155 0.192 0.1909 12303.16% 155 rocq-metarocq-erasure/erasure/theories/EEtaExpandedFix.v.html │ │ 0.000519 0.189 0.1884 36303.28% 236 rocq-metarocq-pcuic/pcuic/theories/PCUICCasesHelper.v.html │ │ 0.346 0.533 0.1865 53.88% 14 rocq-stdlib/theories/extraction/ExtrOcamlChar.v.html │ │ 0.298 0.483 0.1856 62.39% 128 rocq-metarocq-erasure/erasure/theories/ECoInductiveToInductive.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 97.3 96.5 -0.7980 -0.82% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 97.3 96.5 -0.7662 -0.79% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 19.8 19.2 -0.6600 -3.33% 481 coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html │ │ 3.79 3.19 -0.5963 -15.75% 250 rocq-metarocq-erasure/erasure/theories/EWellformed.v.html │ │ 29.8 29.2 -0.5848 -1.96% 12 coq-fourcolor/theories/proof/job589to610.v.html │ │ 21.4 21.0 -0.4334 -2.02% 12 coq-fourcolor/theories/proof/job219to222.v.html │ │ 1.40 1.01 -0.3811 -27.31% 207 rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html │ │ 17.8 17.5 -0.3589 -2.01% 12 coq-fourcolor/theories/proof/job550to553.v.html │ │ 0.514 0.191 -0.3230 -62.86% 11 rocq-stdlib/theories/QArith/Qpower.v.html │ │ 6.80 6.49 -0.3131 -4.60% 149 coq-category-theory/Structure/Monoid.v.html │ │ 1.54 1.23 -0.3122 -20.28% 813 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 31.3 30.9 -0.3076 -0.98% 12 coq-fourcolor/theories/proof/job254to270.v.html │ │ 0.531 0.232 -0.2989 -56.30% 11 rocq-stdlib/theories/omega/OmegaLemmas.v.html │ │ 0.554 0.255 -0.2988 -53.91% 19 rocq-stdlib/theories/MSets/MSetFacts.v.html │ │ 12.4 12.1 -0.2831 -2.28% 930 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html │ │ 0.497 0.256 -0.2409 -48.50% 12 rocq-stdlib/theories/ZArith/Znumtheory.v.html │ │ 0.765 0.529 -0.2357 -30.83% 13 rocq-stdlib/theories/FSets/FMapPositive.v.html │ │ 0.296 0.0738 -0.2219 -75.05% 561 coq-category-theory/Construction/Comma/Adjunction.v.html │ │ 21.7 21.5 -0.2213 -1.02% 12 coq-fourcolor/theories/proof/job542to545.v.html │ │ 0.662 0.442 -0.2199 -33.23% 736 rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyReals.v.html │ │ 1.25 1.04 -0.2053 -16.47% 27 coq-category-theory/Instance/Cones/Comma.v.html │ │ 0.208 0.00785 -0.2000 -96.22% 180 rocq-metarocq-erasure/erasure/theories/ErasureFunctionProperties.v.html │ │ 0.430 0.241 -0.1885 -43.87% 759 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 0.188 0.000109 -0.1876 -99.94% 235 rocq-metarocq-pcuic/pcuic/theories/PCUICCasesHelper.v.html │ │ 0.225 0.0425 -0.1821 -81.09% 126 rocq-metarocq-erasure/erasure/theories/ECoInductiveToInductive.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
Contributor
|
@coqbot bench |
coqbot-app
bot
added
the
needs: full CI
tabareau
force-pushed
the
hint-refresh-firstorder-approx
branch
from
7631376 to
d8f157a
Compare
Contributor
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 2.35 3.12 0.7647 32.49% 607 rocq-stdlib/theories/Zmod/ZmodBase.v.html │ │ 1.49 2.01 0.5165 34.67% 313 rocq-stdlib/theories/Strings/Byte.v.html │ │ 3.10 3.61 0.5051 16.28% 196 rocq-stdlib/theories/ZArith/ZModOffset.v.html │ │ 96.3 96.7 0.4484 0.47% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 96.3 96.7 0.4392 0.46% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 3.15 3.47 0.3216 10.21% 213 rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html │ │ 0.682 0.991 0.3088 45.25% 816 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 9.94 10.2 0.2965 2.98% 496 coq-rewriter/src/Rewriter/Rewriter/Wf.v.html │ │ 11.4 11.7 0.2954 2.60% 410 coq-verdi-raft/theories/RaftProofs/LeaderLogsLogMatchingProof.v.html │ │ 0.256 0.543 0.2866 111.86% 36 rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 13.6 13.8 0.2722 2.01% 571 coq-mathcomp-odd-order/theories/PFsection9.v.html │ │ 14.9 15.2 0.2682 1.80% 559 coq-mathcomp-odd-order/theories/PFsection9.v.html │ │ 6.91 7.14 0.2335 3.38% 604 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 9.65 9.88 0.2300 2.38% 978 coq-verdi-raft/theories/Raft/Linearizability.v.html │ │ 31.864 32.09 0.2260 0.71% 97 coq-vst/veric/binop_lemmas5.v.html │ │ 2.46 2.68 0.2203 8.97% 761 coq-category-theory/Construction/Comma/Adjunction.v.html │ │ 1.10 1.32 0.2154 19.57% 1142 rocq-stdlib/theories/FSets/FMapAVL.v.html │ │ 0.0176 0.229 0.2112 1200.93% 124 rocq-metarocq-safechecker/safechecker/theories/PCUICTypeChecker.v.html │ │ 0.348 0.550 0.2021 58.16% 11 rocq-stdlib/theories/Strings/BinaryString.v.html │ │ 0.00111 0.199 0.1982 17918.99% 189 rocq-metarocq-erasure/erasure/theories/ErasureFunctionProperties.v.html │ │ 0.256 0.451 0.1947 75.92% 1 rocq-stdlib/theories/micromega/ZifyPow.v.html │ │ 0.235 0.430 0.1947 82.87% 11 rocq-stdlib/theories/micromega/Zify.v.html │ │ 0.00152 0.193 0.1919 12622.50% 155 rocq-metarocq-erasure/erasure/theories/EEtaExpandedFix.v.html │ │ 1.22 1.40 0.1880 15.48% 572 rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 0.331 0.518 0.1873 56.58% 11 rocq-stdlib/theories/ZArith/Zquot.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 202 201 -1.1086 -0.55% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 3.82 3.22 -0.6001 -15.70% 250 rocq-metarocq-erasure/erasure/theories/EWellformed.v.html │ │ 25.2 24.7 -0.5431 -2.15% 12 coq-fourcolor/theories/proof/job319to322.v.html │ │ 17.7 17.4 -0.3062 -1.73% 12 coq-fourcolor/theories/proof/job550to553.v.html │ │ 1.39 1.13 -0.2581 -18.61% 733 coq-category-theory/Construction/Comma/Adjunction.v.html │ │ 0.904 0.649 -0.2549 -28.20% 41 rocq-stdlib/theories/ZArith/Zdiv_facts.v.html │ │ 0.578 0.324 -0.2539 -43.95% 18 rocq-stdlib/theories/FSets/FMapFacts.v.html │ │ 6.78 6.53 -0.2489 -3.67% 149 coq-category-theory/Structure/Monoid.v.html │ │ 10.3 10.0 -0.2340 -2.28% 214 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 0.443 0.213 -0.2306 -52.02% 14 rocq-stdlib/theories/Numbers/Cyclic/Int63/Uint63.v.html │ │ 0.715 0.492 -0.2230 -31.20% 719 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 26.3 26.1 -0.2220 -0.84% 374 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 0.533 0.316 -0.2170 -40.73% 1 rocq-stdlib/theories/ZArith/ZModOffset.v.html │ │ 2.11 1.91 -0.2053 -9.73% 102 coq-fiat-parsers/src/Parsers/ParserImplementation.v.html │ │ 0.217 0.0139 -0.2032 -93.61% 573 coq-category-theory/Construction/Comma/Adjunction.v.html │ │ 0.206 0.00798 -0.1985 -96.13% 180 rocq-metarocq-erasure/erasure/theories/ErasureFunctionProperties.v.html │ │ 0.502 0.310 -0.1922 -38.25% 14 rocq-stdlib/theories/Numbers/Integer/Binary/ZBinary.v.html │ │ 26.7 26.5 -0.1902 -0.71% 12 coq-fourcolor/theories/proof/job399to438.v.html │ │ 33.974 33.785 -0.1890 -0.56% 194 coq-vst/veric/expr_lemmas4.v.html │ │ 0.285 0.0979 -0.1872 -65.66% 18 rocq-stdlib/theories/Sorting/Permutation.v.html │ │ 0.187 0.000109 -0.1866 -99.94% 235 rocq-metarocq-pcuic/pcuic/theories/PCUICCasesHelper.v.html │ │ 0.185 0.000372 -0.1846 -99.80% 38 rocq-metarocq-pcuic/pcuic/theories/Typing/PCUICContextConversionTyp.v.html │ │ 48.7 48.5 -0.1836 -0.38% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 0.277 0.0937 -0.1836 -66.21% 22 rocq-stdlib/theories/Vectors/VectorEq.v.html │ │ 0.223 0.0425 -0.1809 -80.96% 126 rocq-metarocq-erasure/erasure/theories/ECoInductiveToInductive.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
github-actions
bot
added
the
needs: rebase
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
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.