[quotation] Fuse Template Monad loops #909
Merged
Conversation
This file contains 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
JasonGross
force-pushed
the
coq-8.16+quotation-fuse-loops
branch
from
a641314 to
a2b0407
Compare
This shouldn't really speed things up, but if it does, it's probably
because the template monad spends too long reducing `monad_map`.
<details><summary>Timing Diff</summary>
<p>
```
After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem)
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
24m01.35s | 1722424 ko | Total Time / Peak Mem | 27m56.55s | 1728408 ko || -3m55.20s || -5984 ko | -14.02% | -0.34%
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
0m12.76s | 990836 ko | ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.vo | 1m38.93s | 1412680 ko || -1m26.17s || -421844 ko | -87.10% | -29.86%
0m08.46s | 904728 ko | ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.vo | 1m00.31s | 1284464 ko || -0m51.85s || -379736 ko | -85.97% | -29.56%
0m11.40s | 826920 ko | ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.vo | 0m45.23s | 1003852 ko || -0m33.82s || -176932 ko | -74.79% | -17.62%
1m19.47s | 1596212 ko | ToTemplate/Coq/MSets.vo | 1m38.20s | 1728408 ko || -0m18.73s || -132196 ko | -19.07% | -7.64%
0m03.79s | 751408 ko | ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.vo | 0m11.25s | 747288 ko || -0m07.46s || 4120 ko | -66.31% | +0.55%
0m00.80s | 721232 ko | ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.vo | 0m08.30s | 727596 ko || -0m07.50s || -6364 ko | -90.36% | -0.87%
0m04.49s | 721836 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.vo | 0m10.69s | 741580 ko || -0m06.19s || -19744 ko | -57.99% | -2.66%
0m04.59s | 728460 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.vo | 0m10.48s | 749904 ko || -0m05.89s || -21444 ko | -56.20% | -2.85%
0m02.94s | 734828 ko | ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.vo | 0m07.35s | 717660 ko || -0m04.41s || 17168 ko | -60.00% | +2.39%
0m02.01s | 702228 ko | ToTemplate/QuotationOf/Coq/FSets/FMapInterface/Sig.vo | 0m04.04s | 698904 ko || -0m02.03s || 3324 ko | -50.24% | +0.47%
0m02.24s | 697844 ko | ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.vo | 0m04.03s | 703936 ko || -0m01.79s || -6092 ko | -44.41% | -0.86%
0m02.14s | 696180 ko | ToTemplate/QuotationOf/Coq/Structures/Equalities/Sig.vo | 0m03.62s | 699480 ko || -0m01.48s || -3300 ko | -40.88% | -0.47%
0m02.03s | 705060 ko | ToTemplate/Coq/Init.vo | 0m03.10s | 711792 ko || -0m01.07s || -6732 ko | -34.51% | -0.94%
3m44.84s | 1368456 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.vo | 3m44.84s | 1368456 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
3m18.00s | 1722424 ko | ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.vo | 3m18.00s | 1722424 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
1m29.10s | 1275632 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.vo | 1m29.10s | 1275632 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
1m22.80s | 1276260 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.vo | 1m22.80s | 1276260 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
1m21.35s | 1275952 ko | ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.vo | 1m21.35s | 1275952 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
1m01.47s | 1389880 ko | ToTemplate/Coq/FSets.vo | 1m01.47s | 1389880 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m52.42s | 1086680 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.vo | 0m52.42s | 1086680 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m52.40s | 878548 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.vo | 0m52.40s | 878548 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m50.59s | 872104 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.vo | 0m50.59s | 872104 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m48.68s | 857164 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.vo | 0m48.68s | 857164 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m47.98s | 864128 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.vo | 0m47.98s | 864128 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m38.44s | 931460 ko | ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.vo | 0m38.44s | 931460 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m29.41s | 1116164 ko | ToTemplate/QuotationOf/Common/EnvironmentTyping/Sig.vo | 0m29.41s | 1116164 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m29.22s | 909244 ko | ToTemplate/QuotationOf/Common/Environment/Sig.vo | 0m29.22s | 909244 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m26.12s | 1284060 ko | ToTemplate/Common/EnvironmentTyping.vo | 0m26.12s | 1284060 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m21.51s | 803672 ko | ToTemplate/QuotationOf/Template/Ast/Env/Instances.vo | 0m21.51s | 803672 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m20.82s | 1095908 ko | ToTemplate/Template/Typing.vo | 0m20.82s | 1095908 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m18.82s | 908440 ko | ToTemplate/Common/Universes.vo | 0m18.82s | 908440 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m15.43s | 868820 ko | ToTemplate/Common/Kernames.vo | 0m15.43s | 868820 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m10.08s | 773444 ko | ToTemplate/QuotationOf/Template/Typing/TemplateGlobalMaps/Instances.vo | 0m10.08s | 773444 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m08.17s | 796076 ko | ToTemplate/QuotationOf/Template/Typing/TemplateEnvTyping/Instances.vo | 0m08.17s | 796076 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m06.84s | 697892 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.vo | 0m06.84s | 697892 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m06.58s | 998568 ko | ToTemplate/Template/TermEquality.vo | 0m06.58s | 998568 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m06.30s | 995716 ko | ToTemplate/Template/WfAst.vo | 0m06.30s | 995716 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m05.88s | 935032 ko | ToTemplate/Common/Environment.vo | 0m05.88s | 935032 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m03.94s | 747208 ko | ToTemplate/QuotationOf/Template/Ast/TemplateLookup/Instances.vo | 0m03.94s | 747208 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m03.70s | 769896 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversion/Instances.vo | 0m03.70s | 769896 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m02.90s | 990412 ko | ToTemplate/Template/Ast.vo | 0m02.90s | 990412 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m02.64s | 921532 ko | ToTemplate/QuotationOf/Template/Ast/EnvHelper/Instances.vo | 0m02.64s | 921532 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m02.63s | 700724 ko | ToTemplate/QuotationOf/Common/Universes/Level/Instances.vo | 0m02.63s | 700724 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m02.47s | 698728 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.vo | 0m02.47s | 698728 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m02.38s | 758748 ko | ToTemplate/QuotationOf/Template/Typing/TemplateDeclarationTyping/Instances.vo | 0m02.38s | 758748 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m02.04s | 701080 ko | ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.vo | 0m02.04s | 701080 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m02.01s | 1003068 ko | ToTemplate/All.vo | 0m02.01s | 1003068 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.94s | 701404 ko | ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.vo | 0m01.94s | 701404 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.89s | 757188 ko | ToTemplate/QuotationOf/Template/Typing/TemplateTyping/Instances.vo | 0m01.89s | 757188 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.84s | 705696 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTerm/Instances.vo | 0m01.84s | 705696 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.70s | 698288 ko | ToTemplate/Init.vo | 0m02.35s | 696844 ko || -0m00.65s || 1444 ko | -27.65% | +0.20%
0m01.69s | 700096 ko | ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.vo | 0m01.69s | 700096 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.59s | 712640 ko | ToTemplate/QuotationOf/Template/ReflectAst/EnvDecide/Instances.vo | 0m01.59s | 712640 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.52s | 870516 ko | ToTemplate/Common/BasicAst.vo | 0m01.52s | 870516 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.52s | 694896 ko | ToTemplate/Utils/MCOption.vo | 0m01.54s | 694776 ko || -0m00.02s || 120 ko | -1.29% | +0.01%
0m01.51s | 696876 ko | ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.vo | 0m02.35s | 699696 ko || -0m00.84s || -2820 ko | -35.74% | -0.40%
0m01.50s | 960280 ko | ToTemplate/QuotationOf/Template/Ast/Instances.vo | 0m01.50s | 960280 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.46s | 985456 ko | ToTemplate/Template/AstUtils.vo | 0m01.46s | 985456 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.37s | 695004 ko | ToTemplate/Utils/All_Forall.vo | 0m01.96s | 696624 ko || -0m00.58s || -1620 ko | -30.10% | -0.23%
0m01.34s | 693840 ko | ToTemplate/Coq/ssr.vo | 0m01.34s | 693840 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.32s | 710140 ko | ToTemplate/QuotationOf/Template/ReflectAst/TemplateTermDecide/Instances.vo | 0m01.32s | 710140 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.29s | 754500 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversionPar/Instances.vo | 0m01.29s | 754500 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.27s | 756972 ko | ToTemplate/QuotationOf/Template/Typing/Instances.vo | 0m01.27s | 756972 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.24s | 696128 ko | ToTemplate/Utils/MCProd.vo | 0m01.49s | 693456 ko || -0m00.25s || 2672 ko | -16.77% | +0.38%
0m01.20s | 746972 ko | ToTemplate/QuotationOf/Common/Universes/Instances.vo | 0m01.20s | 746972 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.19s | 765652 ko | ToTemplate/QuotationOf/Common/Kernames/Instances.vo | 0m01.19s | 765652 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.18s | 704780 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTermUtils/Instances.vo | 0m01.18s | 704780 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.14s | 694192 ko | ToTemplate/Utils/bytestring.vo | 0m01.20s | 693144 ko || -0m00.06s || 1048 ko | -5.00% | +0.15%
0m01.13s | 692704 ko | ToTemplate/Coq/Bool.vo | 0m01.24s | 694592 ko || -0m00.11s || -1888 ko | -8.87% | -0.27%
0m01.11s | 692748 ko | ToTemplate/Common/Primitive.vo | 0m01.11s | 692748 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.09s | 695940 ko | ToTemplate/Coq/Strings.vo | 0m01.09s | 695940 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.09s | 694236 ko | ToTemplate/Utils/MCReflect.vo | 0m01.51s | 694220 ko || -0m00.41s || 16 ko | -27.81% | +0.00%
0m01.08s | 696792 ko | CommonUtils.vo | 0m01.76s | 697100 ko || -0m00.68s || -308 ko | -38.63% | -0.04%
0m01.03s | 701348 ko | ToTemplate/QuotationOf/Template/ReflectAst/Instances.vo | 0m01.03s | 701348 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m01.01s | 693148 ko | ToTemplate/Common/config.vo | 0m01.01s | 693148 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m00.99s | 701420 ko | ToTemplate/Utils/utils.vo | 0m01.35s | 700116 ko || -0m00.36s || 1304 ko | -26.66% | +0.18%
0m00.93s | 693664 ko | ToTemplate/Utils/MCList.vo | 0m01.02s | 698120 ko || -0m00.08s || -4456 ko | -8.82% | -0.63%
0m00.92s | 697284 ko | ToTemplate/Coq/Lists.vo | 0m01.36s | 697084 ko || -0m00.44s || 200 ko | -32.35% | +0.02%
0m00.92s | 699756 ko | ToTemplate/Coq/Numbers.vo | 0m01.62s | 700016 ko || -0m00.70s || -260 ko | -43.20% | -0.03%
0m00.91s | 694628 ko | ToTemplate/Utils/ReflectEq.vo | 0m01.08s | 694044 ko || -0m00.17s || 584 ko | -15.74% | +0.08%
0m00.88s | 703368 ko | ToTemplate/Coq/Floats.vo | 0m01.45s | 704060 ko || -0m00.56s || -692 ko | -39.31% | -0.09%
0m00.86s | 693616 ko | ToTemplate/Utils/MCArith.vo | 0m01.01s | 695988 ko || -0m00.15s || -2372 ko | -14.85% | -0.34%
0m00.80s | 693592 ko | ToTemplate/Utils/MCUtils.vo | 0m01.33s | 694508 ko || -0m00.53s || -916 ko | -39.84% | -0.13%
0m00.07s | 63300 ko | ToTemplate/Utils/MCPred.vo | 0m00.07s | 63300 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m00.07s | 63076 ko | ToTemplate/Utils/MCPrelude.vo | 0m00.06s | 62916 ko || +0m00.01s || 160 ko | +16.66% | +0.25%
0m00.06s | 63864 ko | ToTemplate/Utils/LibHypsNaming.vo | 0m00.06s | 63864 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m00.06s | 64240 ko | ToTemplate/Utils/MCString.vo | 0m00.07s | 64460 ko || -0m00.01s || -220 ko | -14.28% | -0.34%
0m00.06s | 66120 ko | ToTemplate/Utils/wGraph.vo | 0m00.06s | 66120 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m00.05s | 67780 ko | ToTemplate/Common/Reflect.vo | 0m00.05s | 67780 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m00.05s | 64504 ko | ToTemplate/Template/LiftSubst.vo | 0m00.05s | 64504 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m00.05s | 64312 ko | ToTemplate/Utils/ByteCompare.vo | 0m00.05s | 64312 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m00.05s | 63592 ko | ToTemplate/Utils/ByteCompareSpec.vo | 0m00.05s | 63592 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m00.05s | 63160 ko | ToTemplate/Utils/MCRelations.vo | 0m00.06s | 64596 ko || -0m00.00s || -1436 ko | -16.66% | -2.22%
0m00.04s | 63060 ko | ToTemplate/Common/Transform.vo | 0m00.04s | 63060 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m00.04s | 63428 ko | ToTemplate/Template/ReflectAst.vo | 0m00.04s | 63428 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m00.03s | 64740 ko | ToTemplate/Template/Induction.vo | 0m00.03s | 64740 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m00.03s | 64172 ko | ToTemplate/Template/UnivSubst.vo | 0m00.03s | 64172 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m00.03s | 63548 ko | ToTemplate/Utils/ByteCompare_opt.vo | 0m00.03s | 63548 ko || +0m00.00s || 0 ko | +0.00% | +0.00%
0m00.03s | 63636 ko | ToTemplate/Utils/MCSquash.vo | 0m00.04s | 63860 ko || -0m00.01s || -224 ko | -25.00% | -0.35%
0m00.02s | 63864 ko | ToTemplate/Utils/MCCompare.vo | 0m00.06s | 64556 ko || -0m00.03s || -692 ko | -66.66% | -1.07%
0m00.02s | 64480 ko | ToTemplate/Utils/MCEquality.vo | 0m00.07s | 63164 ko || -0m00.05s || 1316 ko | -71.42% | +2.08%
0m00.02s | 63544 ko | ToTemplate/Utils/monad_utils.vo | 0m00.07s | 64916 ko || -0m00.05s || -1372 ko | -71.42% | -2.11%
```
</p>
</details>
JasonGross
force-pushed
the
coq-8.16+quotation-fuse-loops
branch
from
a2b0407 to
f918bda
Compare
This comment was marked as resolved.
This comment was marked as resolved.
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.
I don't know if this will speed things up, but if it does, it's probably because the template monad spends too long reducing
monad_map.On top of #908Timing Diff