Refactor quotation of MSets,FMaps to use MC{MSets,FSets}
#907
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
JasonGross
force-pushed
the
coq-8.16+refactor-quotation-mfsets
branch
from
c7da0f1 to
106d223
Compare
Hopefully this will speed things up slightly
<details><summary>Timing Diff</summary>
<p>
```
After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem)
-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
32m49.24s | 1809576 ko | Total Time / Peak Mem | 35m43.03s | 1925816 ko || -2m53.78s || -116240 ko | -8.10% | -6.03%
-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
0m10.15s | 1326900 ko | ToTemplate/Coq/MSets.vo | 1m36.58s | 1925816 ko || -1m26.42s || -598916 ko | -89.49% | -31.09%
0m04.62s | 895960 ko | ToTemplate/Coq/FSets.vo | 1m01.77s | 1438240 ko || -0m57.15s || -542280 ko | -92.52% | -37.70%
0m03.77s | 936128 ko | ToTemplate/Common/Universes.vo | 0m18.76s | 955168 ko || -0m14.99s || -19040 ko | -79.90% | -1.99%
0m02.69s | 905776 ko | ToTemplate/Common/Kernames.vo | 0m14.95s | 912648 ko || -0m12.25s || -6872 ko | -82.00% | -0.75%
0m45.20s | 1371440 ko | ToTemplate/QuotationOf/Common/EnvironmentTyping/Sig.vo | 0m56.27s | 1371512 ko || -0m11.07s || -72 ko | -19.67% | -0.00%
1m07.85s | 1119888 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.vo | 1m18.12s | 1121528 ko || -0m10.27s || -1640 ko | -13.14% | -0.14%
0m36.76s | 1197356 ko | ToTemplate/QuotationOf/Common/Environment/Sig.vo | 0m47.34s | 1197080 ko || -0m10.58s || 276 ko | -22.34% | +0.02%
0m07.48s | 829680 ko | ToTemplate/QuotationOf/Utils/MCMSets/Sig.vo | N/A | N/A || +0m07.48s || 829680 ko | ∞ | ∞
4m32.42s | 1508112 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.vo | 4m27.25s | 1506652 ko || +0m05.17s || 1460 ko | +1.93% | +0.09%
0m24.74s | 919412 ko | ToTemplate/QuotationOf/Template/Ast/Env/Instances.vo | 0m30.38s | 918952 ko || -0m05.64s || 460 ko | -18.56% | +0.05%
0m16.06s | 1134552 ko | ToTemplate/Template/Typing.vo | 0m20.44s | 1144740 ko || -0m04.38s || -10188 ko | -21.42% | -0.88%
0m14.20s | 894776 ko | ToTemplate/QuotationOf/Template/Typing/TemplateGlobalMaps/Instances.vo | 0m18.31s | 898256 ko || -0m04.10s || -3480 ko | -22.44% | -0.38%
0m04.82s | 799608 ko | ToTemplate/QuotationOf/Utils/MCFSets/Sig.vo | N/A | N/A || +0m04.82s || 799608 ko | ∞ | ∞
3m45.38s | 1809576 ko | ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.vo | 3m41.87s | 1808760 ko || +0m03.50s || 816 ko | +1.58% | +0.04%
1m53.08s | 1481832 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.vo | 1m49.67s | 1481272 ko || +0m03.40s || 560 ko | +3.10% | +0.03%
0m03.56s | 779808 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapDecide/Instances.vo | N/A | N/A || +0m03.56s || 779808 ko | ∞ | ∞
0m03.48s | 780768 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetExtraDecide/Instances.vo | N/A | N/A || +0m03.48s || 780768 ko | ∞ | ∞
0m03.41s | 785624 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetExtraDecide/Instances.vo | N/A | N/A || +0m03.41s || 785624 ko | ∞ | ∞
0m03.29s | 778348 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetExtraOrdProp/Instances.vo | N/A | N/A || +0m03.29s || 778348 ko | ∞ | ∞
0m03.25s | 784736 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetExtraDecide/Instances.vo | N/A | N/A || +0m03.25s || 784736 ko | ∞ | ∞
0m03.24s | 778800 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSetExtraOrdProp/Instances.vo | N/A | N/A || +0m03.24s || 778800 ko | ∞ | ∞
0m24.45s | 1363716 ko | ToTemplate/Common/EnvironmentTyping.vo | 0m26.98s | 1374772 ko || -0m02.53s || -11056 ko | -9.37% | -0.80%
0m24.41s | 949284 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.vo | 0m22.23s | 950400 ko || +0m02.17s || -1116 ko | +9.80% | -0.11%
0m10.80s | 899512 ko | ToTemplate/QuotationOf/Template/Typing/TemplateEnvTyping/Instances.vo | 0m13.75s | 899380 ko || -0m02.94s || 132 ko | -21.45% | +0.01%
0m02.80s | 772744 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetExtraOrdProp/Instances.vo | N/A | N/A || +0m02.79s || 772744 ko | ∞ | ∞
0m02.44s | 776888 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetExtraOrdProp/Instances.vo | N/A | N/A || +0m02.43s || 776888 ko | ∞ | ∞
1m44.59s | 1485384 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.vo | 1m43.37s | 1483736 ko || +0m01.21s || 1648 ko | +1.18% | +0.11%
1m25.91s | 1544648 ko | ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.vo | 1m24.65s | 1543796 ko || +0m01.25s || 852 ko | +1.48% | +0.05%
1m12.56s | 1087324 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.vo | 1m11.24s | 1087592 ko || +0m01.32s || -268 ko | +1.85% | -0.02%
1m09.02s | 1194132 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.vo | 1m07.47s | 1190520 ko || +0m01.54s || 3612 ko | +2.29% | +0.30%
0m14.03s | 838844 ko | ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.vo | 0m12.82s | 839008 ko || +0m01.20s || -164 ko | +9.43% | -0.01%
0m08.24s | 800288 ko | ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.vo | 0m07.11s | 798764 ko || +0m01.12s || 1524 ko | +15.89% | +0.19%
0m05.32s | 825176 ko | ToTemplate/QuotationOf/Template/Ast/TemplateLookup/Instances.vo | 0m07.11s | 825104 ko || -0m01.79s || 72 ko | -25.17% | +0.00%
0m05.25s | 765576 ko | ToTemplate/QuotationOf/Coq/Structures/Equalities/Sig.vo | 0m03.97s | 764292 ko || +0m01.27s || 1284 ko | +32.24% | +0.16%
0m05.25s | 1037320 ko | ToTemplate/Template/TermEquality.vo | 0m07.14s | 1046940 ko || -0m01.88s || -9620 ko | -26.47% | -0.91%
0m05.02s | 987268 ko | ToTemplate/Common/Environment.vo | 0m06.58s | 991972 ko || -0m01.56s || -4704 ko | -23.70% | -0.47%
0m04.89s | 1035036 ko | ToTemplate/Template/WfAst.vo | 0m06.60s | 1043104 ko || -0m01.71s || -8068 ko | -25.90% | -0.77%
0m03.75s | 772528 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.vo | 0m04.79s | 772052 ko || -0m01.04s || 476 ko | -21.71% | +0.06%
0m03.37s | 772656 ko | ToTemplate/Coq/Init.vo | 0m02.31s | 772388 ko || +0m01.06s || 268 ko | +45.88% | +0.03%
0m02.27s | 1031248 ko | ToTemplate/Template/Ast.vo | 0m03.34s | 1040524 ko || -0m01.06s || -9276 ko | -32.03% | -0.89%
0m01.47s | 769112 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapExtraFact/Instances.vo | N/A | N/A || +0m01.47s || 769112 ko | ∞ | ∞
2m12.82s | 1766888 ko | ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.vo | 2m12.90s | 1765000 ko || -0m00.08s || 1888 ko | -0.06% | +0.10%
1m42.66s | 1481440 ko | ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.vo | 1m41.84s | 1480596 ko || +0m00.81s || 844 ko | +0.80% | +0.05%
1m14.80s | 1102060 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.vo | 1m14.99s | 1102984 ko || -0m00.18s || -924 ko | -0.25% | -0.08%
1m11.16s | 1070524 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.vo | 1m11.13s | 1070236 ko || +0m00.03s || 288 ko | +0.04% | +0.02%
0m56.93s | 1246896 ko | ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.vo | 0m57.32s | 1246120 ko || -0m00.39s || 776 ko | -0.68% | +0.06%
0m46.61s | 1084424 ko | ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.vo | 0m45.78s | 1084136 ko || +0m00.82s || 288 ko | +1.81% | +0.02%
0m21.07s | 911000 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.vo | 0m21.81s | 911652 ko || -0m00.73s || -652 ko | -3.39% | -0.07%
0m20.21s | 909132 ko | ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.vo | 0m19.28s | 909320 ko || +0m00.92s || -188 ko | +4.82% | -0.02%
0m14.95s | 855664 ko | ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.vo | 0m14.40s | 855968 ko || +0m00.54s || -304 ko | +3.81% | -0.03%
0m12.37s | 796096 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.vo | 0m11.99s | 798080 ko || +0m00.37s || -1984 ko | +3.16% | -0.24%
0m07.92s | 789420 ko | ToTemplate/QuotationOf/Coq/FSets/FMapInterface/Sig.vo | 0m07.72s | 789176 ko || +0m00.20s || 244 ko | +2.59% | +0.03%
0m04.43s | 769272 ko | ToTemplate/QuotationOf/Common/Universes/Level/Instances.vo | 0m04.06s | 768948 ko || +0m00.37s || 324 ko | +9.11% | +0.04%
0m04.10s | 839732 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversion/Instances.vo | 0m05.02s | 841736 ko || -0m00.92s || -2004 ko | -18.32% | -0.23%
0m03.92s | 768532 ko | ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.vo | 0m03.49s | 768608 ko || +0m00.42s || -76 ko | +12.32% | -0.00%
0m03.85s | 765572 ko | ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.vo | 0m03.96s | 765728 ko || -0m00.10s || -156 ko | -2.77% | -0.02%
0m03.71s | 766472 ko | ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.vo | 0m03.63s | 766524 ko || +0m00.08s || -52 ko | +2.20% | -0.00%
0m03.57s | 962172 ko | ToTemplate/QuotationOf/Template/Ast/EnvHelper/Instances.vo | 0m04.09s | 969872 ko || -0m00.52s || -7700 ko | -12.71% | -0.79%
0m03.29s | 825368 ko | ToTemplate/QuotationOf/Template/Typing/TemplateDeclarationTyping/Instances.vo | 0m04.17s | 826964 ko || -0m00.87s || -1596 ko | -21.10% | -0.19%
0m02.95s | 768952 ko | ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.vo | 0m02.86s | 768760 ko || +0m00.09s || 192 ko | +3.14% | +0.02%
0m02.79s | 777104 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTerm/Instances.vo | 0m03.04s | 777496 ko || -0m00.25s || -392 ko | -8.22% | -0.05%
0m02.09s | 764712 ko | ToTemplate/Utils/MCOption.vo | 0m02.61s | 766056 ko || -0m00.52s || -1344 ko | -19.92% | -0.17%
0m02.04s | 776460 ko | ToTemplate/Init.vo | 0m01.44s | 777204 ko || +0m00.60s || -744 ko | +41.66% | -0.09%
0m02.02s | 768048 ko | ToTemplate/Coq/Lists.vo | 0m01.13s | 767196 ko || +0m00.89s || 852 ko | +78.76% | +0.11%
0m01.89s | 910040 ko | ToTemplate/Common/BasicAst.vo | 0m01.79s | 914792 ko || +0m00.09s || -4752 ko | +5.58% | -0.51%
0m01.87s | 764676 ko | ToTemplate/Utils/All_Forall.vo | 0m01.93s | 765000 ko || -0m00.05s || -324 ko | -3.10% | -0.04%
0m01.83s | 765676 ko | ToTemplate/Coq/Numbers.vo | 0m01.23s | 764216 ko || +0m00.60s || 1460 ko | +48.78% | +0.19%
0m01.83s | 782892 ko | ToTemplate/QuotationOf/Template/ReflectAst/EnvDecide/Instances.vo | 0m02.25s | 784596 ko || -0m00.41s || -1704 ko | -18.66% | -0.21%
0m01.73s | 773096 ko | CommonUtils.vo | 0m01.14s | 771608 ko || +0m00.59s || 1488 ko | +51.75% | +0.19%
0m01.65s | 1047132 ko | ToTemplate/All.vo | 0m02.18s | 1056668 ko || -0m00.53s || -9536 ko | -24.31% | -0.90%
0m01.64s | 823680 ko | ToTemplate/QuotationOf/Template/Typing/TemplateTyping/Instances.vo | 0m02.31s | 823752 ko || -0m00.67s || -72 ko | -29.00% | -0.00%
0m01.64s | 1029248 ko | ToTemplate/Template/AstUtils.vo | 0m02.19s | 1037580 ko || -0m00.55s || -8332 ko | -25.11% | -0.80%
0m01.62s | 762324 ko | ToTemplate/Utils/MCList.vo | 0m01.62s | 763808 ko || +0m00.00s || -1484 ko | +0.00% | -0.19%
0m01.58s | 1001584 ko | ToTemplate/QuotationOf/Template/Ast/Instances.vo | 0m02.01s | 1011472 ko || -0m00.42s || -9888 ko | -21.39% | -0.97%
0m01.58s | 763604 ko | ToTemplate/Utils/MCProd.vo | 0m01.95s | 763840 ko || -0m00.36s || -236 ko | -18.97% | -0.03%
0m01.53s | 763024 ko | ToTemplate/Coq/Bool.vo | 0m02.18s | 762548 ko || -0m00.65s || 476 ko | -29.81% | +0.06%
0m01.49s | 771112 ko | ToTemplate/Utils/utils.vo | 0m01.98s | 772552 ko || -0m00.49s || -1440 ko | -24.74% | -0.18%
0m01.47s | 840308 ko | ToTemplate/QuotationOf/Common/Kernames/Instances.vo | 0m01.86s | 819720 ko || -0m00.39s || 20588 ko | -20.96% | +2.51%
0m01.47s | 779640 ko | ToTemplate/QuotationOf/Template/ReflectAst/TemplateTermDecide/Instances.vo | 0m01.55s | 781164 ko || -0m00.08s || -1524 ko | -5.16% | -0.19%
0m01.39s | 773124 ko | ToTemplate/Coq/Floats.vo | 0m01.10s | 773644 ko || +0m00.28s || -520 ko | +26.36% | -0.06%
0m01.37s | 778256 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTermUtils/Instances.vo | 0m01.61s | 777632 ko || -0m00.24s || 624 ko | -14.90% | +0.08%
0m01.37s | 762076 ko | ToTemplate/Utils/ReflectEq.vo | 0m01.56s | 762944 ko || -0m00.18s || -868 ko | -12.17% | -0.11%
0m01.35s | 823528 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversionPar/Instances.vo | 0m02.20s | 823100 ko || -0m00.85s || 428 ko | -38.63% | +0.05%
0m01.32s | 760900 ko | ToTemplate/Utils/MCUtils.vo | 0m01.45s | 761788 ko || -0m00.12s || -888 ko | -8.96% | -0.11%
0m01.24s | 763964 ko | ToTemplate/Coq/ssr.vo | 0m01.37s | 764504 ko || -0m00.13s || -540 ko | -9.48% | -0.07%
0m01.24s | 827780 ko | ToTemplate/QuotationOf/Common/Universes/Instances.vo | 0m01.51s | 813848 ko || -0m00.27s || 13932 ko | -17.88% | +1.71%
0m01.22s | 761916 ko | ToTemplate/Utils/bytestring.vo | 0m01.75s | 762988 ko || -0m00.53s || -1072 ko | -30.28% | -0.14%
0m01.15s | 818260 ko | ToTemplate/QuotationOf/Template/Typing/Instances.vo | 0m01.70s | 817216 ko || -0m00.55s || 1044 ko | -32.35% | +0.12%
0m01.14s | 764464 ko | ToTemplate/Utils/MCArith.vo | 0m01.26s | 764108 ko || -0m00.12s || 356 ko | -9.52% | +0.04%
0m01.14s | 762852 ko | ToTemplate/Utils/MCReflect.vo | 0m01.62s | 762192 ko || -0m00.48s || 660 ko | -29.62% | +0.08%
0m01.10s | 761984 ko | ToTemplate/Common/config.vo | 0m01.14s | 762060 ko || -0m00.03s || -76 ko | -3.50% | -0.00%
0m01.06s | 761548 ko | ToTemplate/Coq/Strings.vo | 0m01.41s | 759972 ko || -0m00.34s || 1576 ko | -24.82% | +0.20%
0m00.96s | 766440 ko | ToTemplate/QuotationOf/Template/ReflectAst/Instances.vo | 0m01.12s | 766208 ko || -0m00.16s || 232 ko | -14.28% | +0.03%
0m00.90s | 761844 ko | ToTemplate/Common/Primitive.vo | 0m01.26s | 761984 ko || -0m00.36s || -140 ko | -28.57% | -0.01%
0m00.08s | 63988 ko | ToTemplate/Utils/MCRelations.vo | 0m00.06s | 63740 ko || +0m00.02s || 248 ko | +33.33% | +0.38%
0m00.07s | 63148 ko | ToTemplate/Utils/ByteCompareSpec.vo | 0m00.04s | 63208 ko || +0m00.03s || -60 ko | +75.00% | -0.09%
0m00.07s | 64920 ko | ToTemplate/Utils/monad_utils.vo | 0m00.05s | 63376 ko || +0m00.02s || 1544 ko | +40.00% | +2.43%
0m00.06s | 64912 ko | ToTemplate/Utils/ByteCompare.vo | 0m00.03s | 63964 ko || +0m00.03s || 948 ko | +100.00% | +1.48%
0m00.06s | 62956 ko | ToTemplate/Utils/ByteCompare_opt.vo | 0m00.03s | 63680 ko || +0m00.03s || -724 ko | +100.00% | -1.13%
0m00.06s | 63788 ko | ToTemplate/Utils/MCEquality.vo | 0m00.07s | 64724 ko || -0m00.01s || -936 ko | -14.28% | -1.44%
0m00.06s | 63332 ko | ToTemplate/Utils/MCPred.vo | 0m00.04s | 63728 ko || +0m00.01s || -396 ko | +49.99% | -0.62%
0m00.06s | 63340 ko | ToTemplate/Utils/MCPrelude.vo | 0m00.10s | 63372 ko || -0m00.04s || -32 ko | -40.00% | -0.05%
0m00.06s | 64072 ko | ToTemplate/Utils/MCSquash.vo | 0m00.07s | 64196 ko || -0m00.01s || -124 ko | -14.28% | -0.19%
0m00.05s | 63020 ko | ToTemplate/Utils/MCCompare.vo | 0m00.04s | 64692 ko || +0m00.01s || -1672 ko | +25.00% | -2.58%
0m00.04s | 64704 ko | ToTemplate/Common/Transform.vo | 0m00.05s | 64188 ko || -0m00.01s || 516 ko | -20.00% | +0.80%
0m00.04s | 65740 ko | ToTemplate/Template/LiftSubst.vo | 0m00.04s | 63916 ko || +0m00.00s || 1824 ko | +0.00% | +2.85%
0m00.04s | 64632 ko | ToTemplate/Template/ReflectAst.vo | 0m00.06s | 63748 ko || -0m00.01s || 884 ko | -33.33% | +1.38%
0m00.04s | 63300 ko | ToTemplate/Utils/MCString.vo | 0m00.08s | 63272 ko || -0m00.04s || 28 ko | -50.00% | +0.04%
0m00.03s | 64556 ko | ToTemplate/Common/Reflect.vo | 0m00.06s | 63872 ko || -0m00.03s || 684 ko | -50.00% | +1.07%
0m00.03s | 63960 ko | ToTemplate/Template/UnivSubst.vo | 0m00.04s | 63204 ko || -0m00.01s || 756 ko | -25.00% | +1.19%
0m00.03s | 63800 ko | ToTemplate/Utils/LibHypsNaming.vo | 0m00.04s | 64264 ko || -0m00.01s || -464 ko | -25.00% | -0.72%
0m00.03s | 65040 ko | ToTemplate/Utils/wGraph.vo | 0m00.05s | 65976 ko || -0m00.02s || -936 ko | -40.00% | -1.41%
0m00.02s | 64756 ko | ToTemplate/Template/Induction.vo | 0m00.02s | 64116 ko || +0m00.00s || 640 ko | +0.00% | +0.99%
```
</p>
</details>
JasonGross
force-pushed
the
coq-8.16+refactor-quotation-mfsets
branch
from
106d223 to
816cc64
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.
Hopefully this will speed things up slightly
Currently on top of #905, #906Timing Diff