[Quotation] Swap ordering in quotation for performance #942
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 now check whether or not we're going to be using a constant based on its name before trying to check its universes and relevance, on the presumption that getting all the data about a constant / inductive is more expensive than some bytestring manipulation, and additionally that it's more rare to fail on relevance issues than on name checking. We'll pay a small performance hit on quoting modules with many constants in `SProp` so that we can get a large performance boost when separating out submodules manually. We also expose code to skip PCUIC translation when all we care about is the universes / relevance. <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 6m12.90s | 1264632 ko | Total Time / Peak Mem | 8m09.01s | 1781868 ko || -1m56.10s || -517236 ko | -23.74% | -29.02% --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 0m25.58s | 955620 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.vo | 1m04.69s | 1563988 ko || -0m39.10s || -608368 ko | -60.45% | -38.89% 0m30.62s | 1234976 ko | ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.vo | 1m02.19s | 1781868 ko || -0m31.56s || -546892 ko | -50.76% | -30.69% 0m11.57s | 1102628 ko | ToTemplate/QuotationOf/Common/EnvironmentTyping/Sig.vo | 0m16.77s | 1184292 ko || -0m05.19s || -81664 ko | -31.00% | -6.89% 0m05.68s | 854452 ko | ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.vo | 0m09.98s | 938440 ko || -0m04.30s || -83988 ko | -43.08% | -8.94% 0m11.77s | 998824 ko | ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.vo | 0m14.25s | 1064652 ko || -0m02.48s || -65828 ko | -17.40% | -6.18% 0m09.66s | 899064 ko | ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.vo | 0m12.07s | 913896 ko || -0m02.41s || -14832 ko | -19.96% | -1.62% 0m08.57s | 840392 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.vo | 0m11.41s | 893804 ko || -0m02.83s || -53412 ko | -24.89% | -5.97% 0m08.17s | 829724 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.vo | 0m10.40s | 870632 ko || -0m02.23s || -40908 ko | -21.44% | -4.69% 0m07.95s | 830208 ko | ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.vo | 0m10.15s | 877360 ko || -0m02.20s || -47152 ko | -21.67% | -5.37% 0m06.69s | 865048 ko | ToTemplate/QuotationOf/Common/Environment/Sig.vo | 0m09.02s | 920404 ko || -0m02.32s || -55356 ko | -25.83% | -6.01% 0m03.15s | 858276 ko | ToTemplate/QuotationOf/Template/Typing/TemplateEnvTyping/Instances.vo | 0m05.31s | 891164 ko || -0m02.15s || -32888 ko | -40.67% | -3.69% 0m11.40s | 837668 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.vo | 0m12.79s | 845984 ko || -0m01.38s || -8316 ko | -10.86% | -0.98% 0m11.20s | 865068 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.vo | 0m12.93s | 861012 ko || -0m01.73s || 4056 ko | -13.37% | +0.47% 0m11.10s | 848664 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.vo | 0m12.68s | 858968 ko || -0m01.58s || -10304 ko | -12.46% | -1.19% 0m04.33s | 806916 ko | ToTemplate/QuotationOf/Template/Ast/Env/Instances.vo | 0m06.06s | 847376 ko || -0m01.72s || -40460 ko | -28.54% | -4.77% 0m02.34s | 827000 ko | ToTemplate/QuotationOf/Utils/MCMSets/Sig.vo | 0m03.43s | 825052 ko || -0m01.09s || 1948 ko | -31.77% | +0.23% 0m01.87s | 862328 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversion/Instances.vo | 0m03.27s | 864456 ko || -0m01.39s || -2128 ko | -42.81% | -0.24% 0m18.82s | 1264632 ko | ToTemplate/Common/EnvironmentTyping.vo | 0m18.76s | 1264616 ko || +0m00.05s || 16 ko | +0.31% | +0.00% 0m15.08s | 1131500 ko | ToTemplate/Template/Typing.vo | 0m15.04s | 1128072 ko || +0m00.04s || 3428 ko | +0.26% | +0.30% 0m11.86s | 846532 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.vo | 0m12.65s | 856768 ko || -0m00.79s || -10236 ko | -6.24% | -1.19% 0m08.95s | 968096 ko | ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.vo | 0m09.01s | 973932 ko || -0m00.06s || -5836 ko | -0.66% | -0.59% 0m06.64s | 828236 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.vo | 0m07.21s | 818100 ko || -0m00.57s || 10136 ko | -7.90% | +1.23% 0m06.44s | 1074952 ko | ToTemplate/Coq/MSets.vo | 0m06.50s | 1074944 ko || -0m00.05s || 8 ko | -0.92% | +0.00% 0m05.55s | 1050848 ko | ToTemplate/Template/TermEquality.vo | 0m05.52s | 1050992 ko || +0m00.03s || -144 ko | +0.54% | -0.01% 0m05.15s | 1046632 ko | ToTemplate/Template/WfAst.vo | 0m05.17s | 1046748 ko || -0m00.01s || -116 ko | -0.38% | -0.01% 0m05.00s | 828160 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.vo | 0m05.41s | 823872 ko || -0m00.41s || 4288 ko | -7.57% | +0.52% 0m04.60s | 809544 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.vo | 0m04.94s | 819880 ko || -0m00.34s || -10336 ko | -6.88% | -1.26% 0m04.06s | 823204 ko | ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.vo | 0m04.27s | 821056 ko || -0m00.20s || 2148 ko | -4.91% | +0.26% 0m04.00s | 993452 ko | ToTemplate/Common/Environment.vo | 0m04.25s | 998812 ko || -0m00.25s || -5360 ko | -5.88% | -0.53% 0m03.97s | 858268 ko | ToTemplate/QuotationOf/Template/Typing/TemplateGlobalMaps/Instances.vo | 0m04.56s | 864384 ko || -0m00.58s || -6116 ko | -12.93% | -0.70% 0m03.51s | 814284 ko | ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.vo | 0m03.69s | 816344 ko || -0m00.18s || -2060 ko | -4.87% | -0.25% 0m03.31s | 806392 ko | ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.vo | 0m03.48s | 810496 ko || -0m00.16s || -4104 ko | -4.88% | -0.50% 0m03.29s | 963832 ko | ToTemplate/Common/Universes.vo | 0m03.36s | 963756 ko || -0m00.06s || 76 ko | -2.08% | +0.00% 0m03.07s | 902620 ko | ToTemplate/Coq/FSets.vo | 0m03.06s | 902704 ko || +0m00.00s || -84 ko | +0.32% | -0.00% 0m03.02s | 800788 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.vo | 0m03.18s | 796696 ko || -0m00.16s || 4092 ko | -5.03% | +0.51% 0m02.44s | 805928 ko | ToTemplate/Coq/Init.vo | 0m02.44s | 806312 ko || +0m00.00s || -384 ko | +0.00% | -0.04% 0m02.40s | 803688 ko | ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.vo | 0m02.43s | 801856 ko || -0m00.03s || 1832 ko | -1.23% | +0.22% 0m02.21s | 804668 ko | ToTemplate/QuotationOf/Coq/FSets/FMapInterface/Sig.vo | 0m02.43s | 801424 ko || -0m00.22s || 3244 ko | -9.05% | +0.40% 0m02.18s | 1044768 ko | ToTemplate/Template/Ast.vo | 0m02.21s | 1044940 ko || -0m00.02s || -172 ko | -1.35% | -0.01% 0m02.12s | 797412 ko | ToTemplate/QuotationOf/Coq/Structures/Equalities/Sig.vo | 0m02.11s | 797408 ko || +0m00.01s || 4 ko | +0.47% | +0.00% 0m02.09s | 847416 ko | ToTemplate/QuotationOf/Template/Ast/TemplateLookup/Instances.vo | 0m02.59s | 849644 ko || -0m00.50s || -2228 ko | -19.30% | -0.26% 0m01.98s | 921752 ko | ToTemplate/Common/Kernames.vo | 0m01.95s | 921784 ko || +0m00.03s || -32 ko | +1.53% | -0.00% 0m01.87s | 860332 ko | ToTemplate/QuotationOf/Template/Typing/TemplateDeclarationTyping/Instances.vo | 0m01.93s | 860336 ko || -0m00.05s || -4 ko | -3.10% | -0.00% 0m01.85s | 820192 ko | ToTemplate/QuotationOf/Utils/MCFSets/Sig.vo | 0m02.67s | 832016 ko || -0m00.81s || -11824 ko | -30.71% | -1.42% 0m01.66s | 797372 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.vo | 0m01.72s | 799280 ko || -0m00.06s || -1908 ko | -3.48% | -0.23% 0m01.66s | 1053108 ko | ToTemplate/Template/TypingWf.vo | 0m01.68s | 1053136 ko || -0m00.02s || -28 ko | -1.19% | -0.00% 0m01.65s | 816100 ko | ToTemplate/Init.vo | 0m01.62s | 816100 ko || +0m00.02s || 0 ko | +1.85% | +0.00% 0m01.64s | 801580 ko | ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.vo | 0m01.67s | 797348 ko || -0m00.03s || 4232 ko | -1.79% | +0.53% 0m01.64s | 972156 ko | ToTemplate/QuotationOf/Template/Ast/EnvHelper/Instances.vo | 0m01.95s | 972276 ko || -0m00.31s || -120 ko | -15.89% | -0.01% 0m01.63s | 800052 ko | ToTemplate/Utils/All_Forall.vo | 0m01.60s | 799924 ko || +0m00.02s || 128 ko | +1.87% | +0.01% 0m01.60s | 804960 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapDecide/Instances.vo | 0m02.22s | 821332 ko || -0m00.62s || -16372 ko | -27.92% | -1.99% 0m01.57s | 805496 ko | ToTemplate/QuotationOf/Common/Universes/Level/Instances.vo | 0m01.86s | 805712 ko || -0m00.29s || -216 ko | -15.59% | -0.02% 0m01.56s | 800756 ko | ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.vo | 0m01.87s | 800788 ko || -0m00.31s || -32 ko | -16.57% | -0.00% 0m01.55s | 805612 ko | ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.vo | 0m01.57s | 805700 ko || -0m00.02s || -88 ko | -1.27% | -0.01% 0m01.53s | 856368 ko | ToTemplate/QuotationOf/Template/Typing/TemplateTyping/Instances.vo | 0m01.55s | 858412 ko || -0m00.02s || -2044 ko | -1.29% | -0.23% 0m01.51s | 806736 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTerm/Instances.vo | 0m01.49s | 806320 ko || +0m00.02s || 416 ko | +1.34% | +0.05% 0m01.48s | 798032 ko | ToTemplate/Utils/MCOption.vo | 0m01.49s | 798024 ko || -0m00.01s || 8 ko | -0.67% | +0.00% 0m01.38s | 804980 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetExtraDecide/Instances.vo | 0m02.06s | 813080 ko || -0m00.68s || -8100 ko | -33.00% | -0.99% 0m01.35s | 1066252 ko | ToTemplate/All.vo | 0m01.38s | 1065564 ko || -0m00.02s || 688 ko | -2.17% | +0.06% 0m01.35s | 805064 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetExtraOrdProp/Instances.vo | 0m01.40s | 804920 ko || -0m00.04s || 144 ko | -3.57% | +0.01% 0m01.33s | 811700 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetExtraOrdProp/Instances.vo | 0m01.52s | 811632 ko || -0m00.18s || 68 ko | -12.49% | +0.00% 0m01.33s | 811736 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSetExtraOrdProp/Instances.vo | 0m01.52s | 811780 ko || -0m00.18s || -44 ko | -12.49% | -0.00% 0m01.30s | 856212 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversionPar/Instances.vo | 0m01.29s | 856196 ko || +0m00.01s || 16 ko | +0.77% | +0.00% 0m01.29s | 800100 ko | ToTemplate/Coq/Numbers.vo | 0m01.31s | 800076 ko || -0m00.02s || 24 ko | -1.52% | +0.00% 0m01.29s | 813764 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetExtraOrdProp/Instances.vo | 0m01.32s | 811848 ko || -0m00.03s || 1916 ko | -2.27% | +0.23% 0m01.29s | 812504 ko | ToTemplate/QuotationOf/Template/ReflectAst/EnvDecide/Instances.vo | 0m01.52s | 814584 ko || -0m00.23s || -2080 ko | -15.13% | -0.25% 0m01.28s | 811820 ko | CommonUtils.vo | 0m01.29s | 811804 ko || -0m00.01s || 16 ko | -0.77% | +0.00% 0m01.28s | 811768 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetExtraDecide/Instances.vo | 0m02.17s | 821904 ko || -0m00.88s || -10136 ko | -41.01% | -1.23% 0m01.28s | 811728 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetExtraDecide/Instances.vo | 0m02.02s | 819924 ko || -0m00.74s || -8196 ko | -36.63% | -0.99% 0m01.26s | 803572 ko | ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.vo | 0m01.49s | 807584 ko || -0m00.23s || -4012 ko | -15.43% | -0.49% 0m01.25s | 802256 ko | ToTemplate/Coq/Lists.vo | 0m01.24s | 802448 ko || +0m00.01s || -192 ko | +0.80% | -0.02% 0m01.23s | 935152 ko | ToTemplate/Common/BasicAst.vo | 0m01.22s | 935020 ko || +0m00.01s || 132 ko | +0.81% | +0.01% 0m01.23s | 806348 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTermUtils/Instances.vo | 0m01.22s | 806232 ko || +0m00.01s || 116 ko | +0.81% | +0.01% 0m01.21s | 1016248 ko | ToTemplate/QuotationOf/Template/Ast/Instances.vo | 0m01.24s | 1016316 ko || -0m00.03s || -68 ko | -2.41% | -0.00% 0m01.21s | 797936 ko | ToTemplate/Utils/MCProd.vo | 0m01.23s | 797820 ko || -0m00.02s || 116 ko | -1.62% | +0.01% 0m01.20s | 802968 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapExtraFact/Instances.vo | 0m01.20s | 803020 ko || +0m00.00s || -52 ko | +0.00% | -0.00% 0m01.20s | 1045036 ko | ToTemplate/Template/AstUtils.vo | 0m01.22s | 1045048 ko || -0m00.02s || -12 ko | -1.63% | -0.00% 0m01.19s | 797908 ko | ToTemplate/Coq/ssr.vo | 0m01.17s | 795840 ko || +0m00.02s || 2068 ko | +1.70% | +0.25% 0m01.19s | 814524 ko | ToTemplate/QuotationOf/Template/ReflectAst/TemplateTermDecide/Instances.vo | 0m01.23s | 810420 ko || -0m00.04s || 4104 ko | -3.25% | +0.50% 0m01.18s | 853736 ko | ToTemplate/QuotationOf/Template/Typing/Instances.vo | 0m01.11s | 853852 ko || +0m00.06s || -116 ko | +6.30% | -0.01% 0m01.14s | 813088 ko | ToTemplate/Coq/Floats.vo | 0m01.13s | 812960 ko || +0m00.01s || 128 ko | +0.88% | +0.01% 0m01.14s | 803824 ko | ToTemplate/Utils/utils.vo | 0m01.13s | 803940 ko || +0m00.01s || -116 ko | +0.88% | -0.01% 0m01.11s | 797868 ko | ToTemplate/Utils/bytestring.vo | 0m01.08s | 797760 ko || +0m00.03s || 108 ko | +2.77% | +0.01% 0m01.10s | 797376 ko | ToTemplate/Coq/Strings.vo | 0m01.09s | 797292 ko || +0m00.01s || 84 ko | +0.91% | +0.01% 0m01.09s | 805596 ko | ToTemplate/QuotationOf/Template/ReflectAst/Instances.vo | 0m01.06s | 805584 ko || +0m00.03s || 12 ko | +2.83% | +0.00% 0m01.08s | 797844 ko | ToTemplate/Coq/Bool.vo | 0m01.10s | 797804 ko || -0m00.02s || 40 ko | -1.81% | +0.00% 0m01.08s | 797720 ko | ToTemplate/Utils/MCList.vo | 0m01.09s | 797892 ko || -0m00.01s || -172 ko | -0.91% | -0.02% 0m01.08s | 795792 ko | ToTemplate/Utils/MCReflect.vo | 0m01.06s | 795700 ko || +0m00.02s || 92 ko | +1.88% | +0.01% 0m01.07s | 797840 ko | ToTemplate/Utils/ReflectEq.vo | 0m01.06s | 797844 ko || +0m00.01s || -4 ko | +0.94% | -0.00% 0m01.06s | 795732 ko | ToTemplate/Common/Primitive.vo | 0m01.05s | 795776 ko || +0m00.01s || -44 ko | +0.95% | -0.00% 0m01.04s | 846836 ko | ToTemplate/QuotationOf/Common/Universes/Instances.vo | 0m01.05s | 846824 ko || -0m00.01s || 12 ko | -0.95% | +0.00% 0m01.03s | 797852 ko | ToTemplate/Utils/MCArith.vo | 0m01.09s | 795680 ko || -0m00.06s || 2172 ko | -5.50% | +0.27% 0m01.02s | 799332 ko | ToTemplate/Utils/MCUtils.vo | 0m01.07s | 799332 ko || -0m00.05s || 0 ko | -4.67% | +0.00% 0m01.00s | 867456 ko | ToTemplate/QuotationOf/Common/Kernames/Instances.vo | 0m01.03s | 867600 ko || -0m00.03s || -144 ko | -2.91% | -0.01% 0m00.98s | 795848 ko | ToTemplate/Common/config.vo | 0m01.04s | 795784 ko || -0m00.06s || 64 ko | -5.76% | +0.00% ``` </p> </details>
JasonGross
force-pushed
the
coq-8.16+reorder-quote
branch
from
77ccf58 to
e0d3486
Compare
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.
We now check whether or not we're going to be using a constant based on its name before trying to check its universes and relevance, on the presumption that getting all the data about a constant / inductive is more expensive than some bytestring manipulation, and additionally that it's more rare to fail on relevance issues than on name checking. We'll pay a small performance hit on quoting modules with many constants in
SPropso that we can get a large performance boost when separating out submodules manually.We also expose code to skip PCUIC translation when all we care about is the universes / relevance.
This is a ~20%--25% speedup in the quotation subproject. Note that absolute numbers are smaller here because I'm using a beefier machine.
Timing Diff