Ncring_tac: avoid generating temporary pairs in main loop#19501
Merged
coqbot-app[bot] merged 5 commits intorocq-prover:masterfrom Sep 6, 2024
Merged
Ncring_tac: avoid generating temporary pairs in main loop#19501coqbot-app[bot] merged 5 commits intorocq-prover:masterfrom
coqbot-app[bot] merged 5 commits intorocq-prover:masterfrom
Conversation
coqbot-app
bot
added
the
needs: full CI
Contributor
Author
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
Contributor
Author
|
@coqbot bench |
Contributor
|
🏁 Bench results: INFO: failed to install coq-mathcomp-fingroup (dependency coq-mathcomp-ssreflect failed) 🐢 Top 25 slow downs┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 23.5470 27.0730 3.5260 14.97% 129 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 5.4800 7.1620 1.6820 30.69% 196 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 198.9230 200.1030 1.1800 0.59% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 16.3450 17.1740 0.8290 5.07% 32 coq-performance-tests-lite/src/pattern.v.html │ │ 120.6320 121.3010 0.6690 0.55% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 36.0910 36.5400 0.4490 1.24% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 62.6480 62.9890 0.3410 0.54% 609 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 1.9770 2.3050 0.3280 16.59% 227 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2/HeapletwiseAutoSplitMerge.v.html │ │ 61.3710 61.6580 0.2870 0.47% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 235.6160 235.8770 0.2610 0.11% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 22.5040 22.7550 0.2510 1.12% 296 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 2.5010 2.7410 0.2400 9.60% 1001 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 32.5620 32.7980 0.2360 0.72% 97 coq-vst/veric/binop_lemmas5.v.html │ │ 0.6700 0.8900 0.2200 32.84% 736 coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html │ │ 9.2580 9.4500 0.1920 2.07% 2094 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 6.9320 7.1170 0.1850 2.67% 145 coq-fiat-crypto-with-bedrock/src/Algebra/Field.v.html │ │ 9.6340 9.8170 0.1830 1.90% 87 coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html │ │ 3.3670 3.5430 0.1760 5.23% 32 coq-performance-tests-lite/src/n_polymorphic_universes.v.html │ │ 37.3650 37.5380 0.1730 0.46% 548 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 1.1490 1.3090 0.1600 13.93% 1252 coq-metacoq-erasure/erasure/theories/ErasureFunction.v.html │ │ 46.7210 46.8750 0.1540 0.33% 110 coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 22.4400 22.5930 0.1530 0.68% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 0.4290 0.5810 0.1520 35.43% 870 coq-stdlib/MSets/MSetRBT.v.html │ │ 0.2690 0.4110 0.1420 52.79% 586 coq-stdlib/Strings/Byte.v.html │ │ 32.9660 33.1070 0.1410 0.43% 147 coq-vst/veric/expr_lemmas4.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 41.2390 37.6010 -3.6380 -8.82% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 76.5280 74.9540 -1.5740 -2.06% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 97.2500 96.0750 -1.1750 -1.21% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 97.1460 96.0020 -1.1440 -1.18% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 15.6020 14.4890 -1.1130 -7.13% 828 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ │ 22.0600 21.1650 -0.8950 -4.06% 85 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html │ │ 3.5450 2.6620 -0.8830 -24.91% 490 coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 9.3410 8.6010 -0.7400 -7.92% 820 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ │ 180.9990 180.3460 -0.6530 -0.36% 233 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │ │ 39.4630 38.9090 -0.5540 -1.40% 236 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 9.1730 8.6220 -0.5510 -6.01% 819 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ │ 17.1480 16.7910 -0.3570 -2.08% 820 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ │ 8.5810 8.2340 -0.3470 -4.04% 599 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ │ 5.1900 4.8610 -0.3290 -6.34% 416 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ │ 6.8830 6.5980 -0.2850 -4.14% 261 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 38.0640 37.7790 -0.2850 -0.75% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v.html │ │ 9.5640 9.3200 -0.2440 -2.55% 212 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 24.2920 24.0500 -0.2420 -1.00% 79 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html │ │ 1.0220 0.7800 -0.2420 -23.68% 572 coq-stdlib/MSets/MSetAVL.v.html │ │ 4.9430 4.7060 -0.2370 -4.79% 227 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 27.2580 27.0210 -0.2370 -0.87% 68 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │ │ 1.6130 1.3810 -0.2320 -14.38% 313 coq-stdlib/Strings/Byte.v.html │ │ 4.1720 3.9500 -0.2220 -5.32% 201 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 15.2510 15.0510 -0.2000 -1.31% 417 coq-fiat-crypto-with-bedrock/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v.html │ │ 1.0600 0.8670 -0.1930 -18.21% 408 coq-stdlib/MSets/MSetAVL.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
Contributor
Author
|
Full CI was green at https://gitlab.inria.fr/coq/coq/-/pipelines/1028999 |
ppedrot
reviewed
Sep 4, 2024
| Ltac extra_reify term := open_constr:((false,tt)). | ||
| (* extensibility: override to add ways to reify a term. | ||
| Return [tt] for terms which aren't handled (tt doesn't have type PExpr so is unambiguous) *) | ||
| Ltac extra_reify term := open_constr:(tt). |
Member
There was a problem hiding this comment.
I'm not sure how often this is used and how documented it is, but I think this deserves a changelog.
Contributor
Author
silene
reviewed
Sep 4, 2024
SkySkimmer
force-pushed
the
ncring-tac-speed
branch
from
b809ebe to
fd03089
Compare
coqbot-app
bot
added
the
needs: full CI
SkySkimmer
removed
the
needs: full CI
SkySkimmer
force-pushed
the
ncring-tac-speed
branch
from
fd03089 to
1ca1831
Compare
coqbot-app
bot
added
the
needs: full CI
SkySkimmer
added a commit
to ppedrot/coq
that referenced
this pull request
Sep 5, 2024
SkySkimmer
force-pushed
the
ncring-tac-speed
branch
from
9705b09 to
82a2e20
Compare
Contributor
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 2.7320 3.4660 0.7340 26.87% 490 coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 65.6030 66.2930 0.6900 1.05% 609 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 60.3970 60.8700 0.4730 0.78% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 181.3870 181.8340 0.4470 0.25% 233 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │ │ 0.6580 0.9410 0.2830 43.01% 813 coq-stdlib/MSets/MSetRBT.v.html │ │ 39.3890 39.6360 0.2470 0.63% 835 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 93.7670 93.9760 0.2090 0.22% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 7.0580 7.2560 0.1980 2.81% 196 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 35.3640 35.5340 0.1700 0.48% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 37.4780 37.6410 0.1630 0.43% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v.html │ │ 0.5520 0.7140 0.1620 29.35% 422 coq-stdlib/MSets/MSetList.v.html │ │ 22.0470 22.1980 0.1510 0.68% 6 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.v.html │ │ 37.6490 37.7990 0.1500 0.40% 548 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 6.3930 6.5330 0.1400 2.19% 3024 coq-fiat-crypto-with-bedrock/src/Assembly/EquivalenceProofs.v.html │ │ 0.4050 0.5430 0.1380 34.07% 705 coq-stdlib/Numbers/HexadecimalFacts.v.html │ │ 11.3850 11.5220 0.1370 1.20% 527 coq-fiat-crypto-with-bedrock/src/AbstractInterpretation/Wf.v.html │ │ 16.5390 16.6700 0.1310 0.79% 81 coq-fiat-crypto-with-bedrock/rupicola/src/Rupicola/Examples/Utf8/Utf8.v.html │ │ 1.3130 1.4390 0.1260 9.60% 98 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Translation/Proofs/UsedVarnames.v.html │ │ 3.6020 3.7250 0.1230 3.41% 195 coq-fiat-crypto-with-bedrock/src/Demo.v.html │ │ 0.2450 0.3680 0.1230 50.20% 778 coq-stdlib/setoid_ring/Ring_polynom.v.html │ │ 1.6800 1.8020 0.1220 7.26% 849 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ │ 1.6860 1.8080 0.1220 7.24% 105 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Translation/Proofs/UsedVarnames.v.html │ │ 5.6140 5.7350 0.1210 2.16% 209 coq-fiat-crypto-with-bedrock/src/Demo.v.html │ │ 21.4120 21.5310 0.1190 0.56% 23 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/Arith.v.html │ │ 0.3910 0.5070 0.1160 29.67% 870 coq-stdlib/MSets/MSetRBT.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 76.3450 74.4960 -1.8490 -2.42% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 236.2940 235.3780 -0.9160 -0.39% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 9.6660 8.7640 -0.9020 -9.33% 849 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ │ 21.8600 20.9730 -0.8870 -4.06% 85 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html │ │ 24.7790 24.0680 -0.7110 -2.87% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 133.3530 132.8160 -0.5370 -0.40% 155 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 20.0980 19.6430 -0.4550 -2.26% 213 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 27.5920 27.2160 -0.3760 -1.36% 129 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 5.9660 5.6070 -0.3590 -6.02% 840 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ │ 38.5000 38.1450 -0.3550 -0.92% 1350 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 6.9170 6.5670 -0.3500 -5.06% 261 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 4.9930 4.6500 -0.3430 -6.87% 227 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 9.5250 9.1950 -0.3300 -3.46% 212 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 5.9690 5.6540 -0.3150 -5.28% 841 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ │ 0.9440 0.6520 -0.2920 -30.93% 736 coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html │ │ 4.1840 3.9560 -0.2280 -5.45% 201 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 3.3580 3.1350 -0.2230 -6.64% 256 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 14.9910 14.7930 -0.1980 -1.32% 617 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html │ │ 46.7540 46.5720 -0.1820 -0.39% 110 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 14.6750 14.4950 -0.1800 -1.23% 615 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html │ │ 6.5080 6.3350 -0.1730 -2.66% 488 coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html │ │ 24.8380 24.6670 -0.1710 -0.69% 345 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 0.2530 0.0940 -0.1590 -62.85% 853 coq-stdlib/MSets/MSetRBT.v.html │ │ 8.5270 8.3680 -0.1590 -1.86% 566 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/Jacobian.v.html │ │ 20.9430 20.7900 -0.1530 -0.73% 40 coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/SolinasReductionReificationCache.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
Contributor
Author
New version doesn't have an issue there |
ppedrot
approved these changes
Sep 6, 2024
Member
|
To please the label master, @coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
Member
|
@coqbot merge now |
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 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.
Should be more efficient especially with #19228