Add a fast path in Mod_subst.reroot. - #22421
Open
ppedrot wants to merge 1 commit into
Open
Conversation
There is no point in rerooting if the root of the δ-resolver is already the path at which we want to reroot. While not a silver bullet, it really mitigates rocq-prover#22420, which goes from ~22 seconds to ~5 seconds on my machine.
ppedrot
added
kind: performance
coqbot-app
Bot
removed
the
request: full CI
Member
Author
|
@coqbot bench |
Member
Author
|
cc @ebmoon, I don't know if it helps for your practical examples. |
Contributor
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 62.4 63.9 1.4476 2.32% 857 rocq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v.html │ │ 127 128 0.7322 0.58% 659 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 90.9 91.5 0.5817 0.64% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 66.1 66.6 0.4914 0.74% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 53.2 53.7 0.4839 0.91% 567 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 18.5 19.0 0.4741 2.57% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 9.37 9.84 0.4725 5.04% 436 coq-mathcomp-odd-order/theories/PFsection12.v.html │ │ 43.0 43.4 0.4576 1.07% 539 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 11.8 12.3 0.4547 3.85% 1828 rocq-mathcomp-analysis/theories/ftc.v.html │ │ 65.9 66.3 0.4508 0.68% 794 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 68.0 68.5 0.4501 0.66% 596 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 90.9 91.3 0.4471 0.49% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 107 107 0.4430 0.41% 255 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 13.6 14.1 0.4423 3.24% 925 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html │ │ 53.8 54.2 0.4385 0.82% 776 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 27.3 27.7 0.4368 1.60% 13 coq-fourcolor/theories/proof/job611to617.v.html │ │ 26.3 26.7 0.3856 1.46% 62 coq-fiat-crypto-with-bedrock/src/Assembly/Parse/TestAsm.v.html │ │ 0.00970 0.379 0.3697 3813.75% 111 rocq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v.html │ │ 65.5 65.8 0.3470 0.53% 305 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 24.8 25.2 0.3417 1.38% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 43.5 43.9 0.3289 0.76% 221 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 50.9 51.3 0.3232 0.63% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 32.3 32.6 0.3149 0.98% 255 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html │ │ 18.7 19.0 0.3101 1.66% 77 coq-fiat-crypto-with-bedrock/src/Assembly/Parse/TestAsm.v.html │ │ 10.4 10.7 0.3057 2.94% 2852 coq-fiat-crypto-with-bedrock/src/Assembly/EquivalenceProofs.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 18.8 17.2 -1.5558 -8.28% 670 coq-performance-tests-lite/src/Nia.v.html │ │ 12.6 11.6 -1.0376 -8.24% 531 coq-performance-tests-lite/src/Nia.v.html │ │ 8.54 7.79 -0.7465 -8.74% 428 coq-performance-tests-lite/src/Nia.v.html │ │ 6.85 6.23 -0.6207 -9.07% 658 coq-performance-tests-lite/src/Nia.v.html │ │ 48.6 48.0 -0.5574 -1.15% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html │ │ 5.01 4.48 -0.5279 -10.55% 330 coq-performance-tests-lite/src/Nia.v.html │ │ 46.8 46.3 -0.4702 -1.00% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 0.386 0.00146 -0.3847 -99.62% 161 rocq-mathcomp-analysis/theories/derive.v.html │ │ 0.377 0.000687 -0.3766 -99.82% 183 rocq-mathcomp-analysis/theories/sequences.v.html │ │ 3.61 3.24 -0.3707 -10.25% 462 coq-performance-tests-lite/src/Nia.v.html │ │ 0.372 0.00347 -0.3690 -99.07% 112 rocq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v.html │ │ 20.8 20.5 -0.3686 -1.77% 560 coq-mathcomp-odd-order/theories/PFsection9.v.html │ │ 48.7 48.3 -0.3573 -0.73% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 31.5 31.1 -0.3523 -1.12% 656 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 22.2 21.8 -0.3487 -1.57% 13 coq-fourcolor/theories/proof/job542to545.v.html │ │ 7.27 6.95 -0.3193 -4.39% 594 coq-performance-tests-lite/src/Nia.v.html │ │ 1.32 1.01 -0.3039 -23.11% 127 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/Poly1305/Field1305.v.html │ │ 203 203 -0.3026 -0.15% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 2.80 2.50 -0.2998 -10.71% 108 coq-performance-tests-lite/src/Nia.v.html │ │ 4.53 4.24 -0.2964 -6.54% 814 coq-performance-tests-lite/src/Nia.v.html │ │ 4.52 4.23 -0.2962 -6.55% 815 coq-performance-tests-lite/src/Nia.v.html │ │ 23.5 23.2 -0.2957 -1.26% 743 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 0.295 0.00116 -0.2936 -99.61% 251 rocq-mathcomp-analysis/theories/measure_theory/measurable_structure.v.html │ │ 4.58 4.29 -0.2862 -6.25% 813 coq-performance-tests-lite/src/Nia.v.html │ │ 1.73 1.45 -0.2840 -16.37% 4 rocq-mathcomp-analysis/theories/pi_irrational.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
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
1 participant
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.
There is no point in rerooting if the root of the δ-resolver is already the path at which we want to reroot. While not a silver bullet, it really mitigates #22420, which goes from ~22 seconds to ~5 seconds on my machine.