Use a more systematic mangling of universe names #908
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
This should hopefully both speed things up and potentially avoid
universe inconsistencies.
<details><summary>Timing Diff</summary>
<p>
```
After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem)
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
27m56.55s | 1728408 ko | Total Time / Peak Mem | 35m28.28s | 1976000 ko || -7m31.72s || -247592 ko | -21.22% | -12.52%
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
3m44.84s | 1368456 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.vo | 4m28.56s | 1347576 ko || -0m43.71s || 20880 ko | -16.27% | +1.54%
1m38.93s | 1412680 ko | ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.vo | 2m13.30s | 1674924 ko || -0m34.37s || -262244 ko | -25.78% | -15.65%
0m29.41s | 1116164 ko | ToTemplate/QuotationOf/Common/EnvironmentTyping/Sig.vo | 0m56.50s | 1261512 ko || -0m27.08s || -145348 ko | -47.94% | -11.52%
3m18.00s | 1722424 ko | ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.vo | 3m42.94s | 1976000 ko || -0m24.93s || -253576 ko | -11.18% | -12.83%
0m52.40s | 878548 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.vo | 1m16.86s | 1041496 ko || -0m24.46s || -162948 ko | -31.82% | -15.64%
0m50.59s | 872104 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.vo | 1m14.63s | 1028104 ko || -0m24.03s || -156000 ko | -32.21% | -15.17%
1m00.31s | 1284464 ko | ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.vo | 1m23.83s | 1355772 ko || -0m23.51s || -71308 ko | -28.05% | -5.25%
0m48.68s | 857164 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.vo | 1m10.88s | 997404 ko || -0m22.19s || -140240 ko | -31.32% | -14.06%
0m47.98s | 864128 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.vo | 1m10.28s | 1009492 ko || -0m22.30s || -145364 ko | -31.73% | -14.39%
1m29.10s | 1275632 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.vo | 1m49.82s | 1297876 ko || -0m20.71s || -22244 ko | -18.86% | -1.71%
1m21.35s | 1275952 ko | ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.vo | 1m40.69s | 1293716 ko || -0m19.34s || -17764 ko | -19.20% | -1.37%
1m22.80s | 1276260 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.vo | 1m41.41s | 1301716 ko || -0m18.60s || -25456 ko | -18.35% | -1.95%
0m29.22s | 909244 ko | ToTemplate/QuotationOf/Common/Environment/Sig.vo | 0m46.57s | 1017928 ko || -0m17.35s || -108684 ko | -37.25% | -10.67%
0m52.42s | 1086680 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.vo | 1m07.19s | 1140600 ko || -0m14.76s || -53920 ko | -21.98% | -4.72%
0m45.23s | 1003852 ko | ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.vo | 0m58.27s | 1188136 ko || -0m13.04s || -184284 ko | -22.37% | -15.51%
0m10.48s | 749904 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.vo | 0m21.82s | 876040 ko || -0m11.33s || -126136 ko | -51.97% | -14.39%
0m10.69s | 741580 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.vo | 0m20.21s | 840224 ko || -0m09.52s || -98644 ko | -47.10% | -11.74%
0m21.51s | 803672 ko | ToTemplate/QuotationOf/Template/Ast/Env/Instances.vo | 0m29.88s | 846932 ko || -0m08.36s || -43260 ko | -28.01% | -5.10%
0m11.25s | 747288 ko | ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.vo | 0m19.67s | 833044 ko || -0m08.42s || -85756 ko | -42.80% | -10.29%
0m10.08s | 773444 ko | ToTemplate/QuotationOf/Template/Typing/TemplateGlobalMaps/Instances.vo | 0m18.07s | 819904 ko || -0m07.99s || -46460 ko | -44.21% | -5.66%
0m38.44s | 931460 ko | ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.vo | 0m45.20s | 1013316 ko || -0m06.76s || -81856 ko | -14.95% | -8.07%
0m08.30s | 727596 ko | ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.vo | 0m14.55s | 787268 ko || -0m06.25s || -59672 ko | -42.95% | -7.57%
0m08.17s | 796076 ko | ToTemplate/QuotationOf/Template/Typing/TemplateEnvTyping/Instances.vo | 0m13.50s | 826120 ko || -0m05.33s || -30044 ko | -39.48% | -3.63%
0m07.35s | 717660 ko | ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.vo | 0m12.66s | 785100 ko || -0m05.31s || -67440 ko | -41.94% | -8.58%
0m06.84s | 697892 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.vo | 0m11.49s | 723484 ko || -0m04.65s || -25592 ko | -40.46% | -3.53%
1m38.20s | 1728408 ko | ToTemplate/Coq/MSets.vo | 1m41.31s | 1939012 ko || -0m03.10s || -210604 ko | -3.06% | -10.86%
0m04.03s | 703936 ko | ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.vo | 0m07.25s | 726368 ko || -0m03.21s || -22432 ko | -44.41% | -3.08%
0m04.04s | 698904 ko | ToTemplate/QuotationOf/Coq/FSets/FMapInterface/Sig.vo | 0m06.85s | 724692 ko || -0m02.80s || -25788 ko | -41.02% | -3.55%
0m03.94s | 747208 ko | ToTemplate/QuotationOf/Template/Ast/TemplateLookup/Instances.vo | 0m06.55s | 759832 ko || -0m02.60s || -12624 ko | -39.84% | -1.66%
0m02.47s | 698728 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.vo | 0m04.68s | 708696 ko || -0m02.20s || -9968 ko | -47.22% | -1.40%
0m03.70s | 769896 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversion/Instances.vo | 0m04.88s | 771648 ko || -0m01.17s || -1752 ko | -24.18% | -0.22%
0m02.64s | 921532 ko | ToTemplate/QuotationOf/Template/Ast/EnvHelper/Instances.vo | 0m04.02s | 926344 ko || -0m01.37s || -4812 ko | -34.32% | -0.51%
0m02.63s | 700724 ko | ToTemplate/QuotationOf/Common/Universes/Level/Instances.vo | 0m04.09s | 700076 ko || -0m01.46s || 648 ko | -35.69% | +0.09%
0m02.38s | 758748 ko | ToTemplate/QuotationOf/Template/Typing/TemplateDeclarationTyping/Instances.vo | 0m04.17s | 759436 ko || -0m01.79s || -688 ko | -42.92% | -0.09%
0m02.04s | 701080 ko | ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.vo | 0m03.37s | 698344 ko || -0m01.33s || 2736 ko | -39.46% | +0.39%
0m01.94s | 701404 ko | ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.vo | 0m03.28s | 697440 ko || -0m01.33s || 3964 ko | -40.85% | +0.56%
0m01.69s | 700096 ko | ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.vo | 0m02.81s | 705736 ko || -0m01.12s || -5640 ko | -39.85% | -0.79%
1m01.47s | 1389880 ko | ToTemplate/Coq/FSets.vo | 1m01.73s | 1402124 ko || -0m00.25s || -12244 ko | -0.42% | -0.87%
0m26.12s | 1284060 ko | ToTemplate/Common/EnvironmentTyping.vo | 0m26.92s | 1338856 ko || -0m00.80s || -54796 ko | -2.97% | -4.09%
0m20.82s | 1095908 ko | ToTemplate/Template/Typing.vo | 0m20.40s | 1099736 ko || +0m00.42s || -3828 ko | +2.05% | -0.34%
0m18.82s | 908440 ko | ToTemplate/Common/Universes.vo | 0m18.48s | 916460 ko || +0m00.33s || -8020 ko | +1.83% | -0.87%
0m15.43s | 868820 ko | ToTemplate/Common/Kernames.vo | 0m14.86s | 872484 ko || +0m00.57s || -3664 ko | +3.83% | -0.41%
0m06.58s | 998568 ko | ToTemplate/Template/TermEquality.vo | 0m07.01s | 1005820 ko || -0m00.42s || -7252 ko | -6.13% | -0.72%
0m06.30s | 995716 ko | ToTemplate/Template/WfAst.vo | 0m06.50s | 1002992 ko || -0m00.20s || -7276 ko | -3.07% | -0.72%
0m05.88s | 935032 ko | ToTemplate/Common/Environment.vo | 0m06.47s | 950944 ko || -0m00.58s || -15912 ko | -9.11% | -1.67%
0m03.62s | 699480 ko | ToTemplate/QuotationOf/Coq/Structures/Equalities/Sig.vo | 0m03.88s | 702452 ko || -0m00.25s || -2972 ko | -6.70% | -0.42%
0m03.10s | 711792 ko | ToTemplate/Coq/Init.vo | 0m02.70s | 705556 ko || +0m00.39s || 6236 ko | +14.81% | +0.88%
0m02.90s | 990412 ko | ToTemplate/Template/Ast.vo | 0m03.14s | 999436 ko || -0m00.24s || -9024 ko | -7.64% | -0.90%
0m02.35s | 696844 ko | ToTemplate/Init.vo | 0m02.30s | 699476 ko || +0m00.05s || -2632 ko | +2.17% | -0.37%
0m02.35s | 699696 ko | ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.vo | 0m03.12s | 700204 ko || -0m00.77s || -508 ko | -24.67% | -0.07%
0m02.01s | 1003068 ko | ToTemplate/All.vo | 0m01.89s | 1010272 ko || +0m00.11s || -7204 ko | +6.34% | -0.71%
0m01.96s | 696624 ko | ToTemplate/Utils/All_Forall.vo | 0m01.91s | 696852 ko || +0m00.05s || -228 ko | +2.61% | -0.03%
0m01.89s | 757188 ko | ToTemplate/QuotationOf/Template/Typing/TemplateTyping/Instances.vo | 0m02.02s | 756856 ko || -0m00.13s || 332 ko | -6.43% | +0.04%
0m01.84s | 705696 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTerm/Instances.vo | 0m02.58s | 710328 ko || -0m00.74s || -4632 ko | -28.68% | -0.65%
0m01.76s | 697100 ko | CommonUtils.vo | 0m01.36s | 697944 ko || +0m00.39s || -844 ko | +29.41% | -0.12%
0m01.62s | 700016 ko | ToTemplate/Coq/Numbers.vo | 0m01.16s | 700136 ko || +0m00.46s || -120 ko | +39.65% | -0.01%
0m01.59s | 712640 ko | ToTemplate/QuotationOf/Template/ReflectAst/EnvDecide/Instances.vo | 0m01.97s | 712756 ko || -0m00.37s || -116 ko | -19.28% | -0.01%
0m01.54s | 694776 ko | ToTemplate/Utils/MCOption.vo | 0m01.99s | 696804 ko || -0m00.44s || -2028 ko | -22.61% | -0.29%
0m01.52s | 870516 ko | ToTemplate/Common/BasicAst.vo | 0m01.60s | 877576 ko || -0m00.08s || -7060 ko | -5.00% | -0.80%
0m01.51s | 694220 ko | ToTemplate/Utils/MCReflect.vo | 0m01.51s | 694328 ko || +0m00.00s || -108 ko | +0.00% | -0.01%
0m01.50s | 960280 ko | ToTemplate/QuotationOf/Template/Ast/Instances.vo | 0m01.55s | 968092 ko || -0m00.05s || -7812 ko | -3.22% | -0.80%
0m01.49s | 693456 ko | ToTemplate/Utils/MCProd.vo | 0m01.50s | 694308 ko || -0m00.01s || -852 ko | -0.66% | -0.12%
0m01.46s | 985456 ko | ToTemplate/Template/AstUtils.vo | 0m01.64s | 995224 ko || -0m00.17s || -9768 ko | -10.97% | -0.98%
0m01.45s | 704060 ko | ToTemplate/Coq/Floats.vo | 0m01.01s | 703292 ko || +0m00.43s || 768 ko | +43.56% | +0.10%
0m01.36s | 697084 ko | ToTemplate/Coq/Lists.vo | 0m01.36s | 698156 ko || +0m00.00s || -1072 ko | +0.00% | -0.15%
0m01.35s | 700116 ko | ToTemplate/Utils/utils.vo | 0m01.26s | 700996 ko || +0m00.09s || -880 ko | +7.14% | -0.12%
0m01.34s | 693840 ko | ToTemplate/Coq/ssr.vo | 0m01.14s | 694884 ko || +0m00.20s || -1044 ko | +17.54% | -0.15%
0m01.33s | 694508 ko | ToTemplate/Utils/MCUtils.vo | 0m01.16s | 694536 ko || +0m00.17s || -28 ko | +14.65% | -0.00%
0m01.32s | 710140 ko | ToTemplate/QuotationOf/Template/ReflectAst/TemplateTermDecide/Instances.vo | 0m01.40s | 711564 ko || -0m00.07s || -1424 ko | -5.71% | -0.20%
0m01.29s | 754500 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversionPar/Instances.vo | 0m01.57s | 755212 ko || -0m00.28s || -712 ko | -17.83% | -0.09%
0m01.27s | 756972 ko | ToTemplate/QuotationOf/Template/Typing/Instances.vo | 0m01.17s | 756196 ko || +0m00.10s || 776 ko | +8.54% | +0.10%
0m01.24s | 694592 ko | ToTemplate/Coq/Bool.vo | 0m01.43s | 695096 ko || -0m00.18s || -504 ko | -13.28% | -0.07%
0m01.20s | 746972 ko | ToTemplate/QuotationOf/Common/Universes/Instances.vo | 0m01.06s | 754076 ko || +0m00.13s || -7104 ko | +13.20% | -0.94%
0m01.20s | 693144 ko | ToTemplate/Utils/bytestring.vo | 0m01.53s | 698048 ko || -0m00.33s || -4904 ko | -21.56% | -0.70%
0m01.19s | 765652 ko | ToTemplate/QuotationOf/Common/Kernames/Instances.vo | 0m01.09s | 771052 ko || +0m00.09s || -5400 ko | +9.17% | -0.70%
0m01.18s | 704780 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTermUtils/Instances.vo | 0m01.70s | 707492 ko || -0m00.52s || -2712 ko | -30.58% | -0.38%
0m01.11s | 692748 ko | ToTemplate/Common/Primitive.vo | 0m01.25s | 693068 ko || -0m00.13s || -320 ko | -11.19% | -0.04%
0m01.09s | 695940 ko | ToTemplate/Coq/Strings.vo | 0m01.01s | 694968 ko || +0m00.08s || 972 ko | +7.92% | +0.13%
0m01.08s | 694044 ko | ToTemplate/Utils/ReflectEq.vo | 0m01.16s | 693864 ko || -0m00.07s || 180 ko | -6.89% | +0.02%
0m01.03s | 701348 ko | ToTemplate/QuotationOf/Template/ReflectAst/Instances.vo | 0m01.07s | 700708 ko || -0m00.04s || 640 ko | -3.73% | +0.09%
0m01.02s | 698120 ko | ToTemplate/Utils/MCList.vo | 0m01.29s | 693604 ko || -0m00.27s || 4516 ko | -20.93% | +0.65%
0m01.01s | 693148 ko | ToTemplate/Common/config.vo | 0m01.23s | 694780 ko || -0m00.21s || -1632 ko | -17.88% | -0.23%
0m01.01s | 695988 ko | ToTemplate/Utils/MCArith.vo | 0m01.19s | 693928 ko || -0m00.17s || 2060 ko | -15.12% | +0.29%
0m00.07s | 63164 ko | ToTemplate/Utils/MCEquality.vo | 0m00.04s | 63060 ko || +0m00.03s || 104 ko | +75.00% | +0.16%
0m00.07s | 63300 ko | ToTemplate/Utils/MCPred.vo | 0m00.03s | 63976 ko || +0m00.04s || -676 ko | +133.33% | -1.05%
0m00.07s | 64460 ko | ToTemplate/Utils/MCString.vo | 0m00.05s | 64348 ko || +0m00.02s || 112 ko | +40.00% | +0.17%
0m00.07s | 64916 ko | ToTemplate/Utils/monad_utils.vo | 0m00.06s | 63088 ko || +0m00.01s || 1828 ko | +16.66% | +2.89%
0m00.06s | 63864 ko | ToTemplate/Utils/LibHypsNaming.vo | 0m00.04s | 64692 ko || +0m00.01s || -828 ko | +49.99% | -1.27%
0m00.06s | 64556 ko | ToTemplate/Utils/MCCompare.vo | 0m00.06s | 64992 ko || +0m00.00s || -436 ko | +0.00% | -0.67%
0m00.06s | 62916 ko | ToTemplate/Utils/MCPrelude.vo | 0m00.07s | 63064 ko || -0m00.01s || -148 ko | -14.28% | -0.23%
0m00.06s | 64596 ko | ToTemplate/Utils/MCRelations.vo | 0m00.07s | 64120 ko || -0m00.01s || 476 ko | -14.28% | +0.74%
0m00.06s | 66120 ko | ToTemplate/Utils/wGraph.vo | 0m00.06s | 64668 ko || +0m00.00s || 1452 ko | +0.00% | +2.24%
0m00.05s | 67780 ko | ToTemplate/Common/Reflect.vo | 0m00.07s | 63112 ko || -0m00.02s || 4668 ko | -28.57% | +7.39%
0m00.05s | 64504 ko | ToTemplate/Template/LiftSubst.vo | 0m00.05s | 63644 ko || +0m00.00s || 860 ko | +0.00% | +1.35%
0m00.05s | 64312 ko | ToTemplate/Utils/ByteCompare.vo | 0m00.05s | 63780 ko || +0m00.00s || 532 ko | +0.00% | +0.83%
0m00.05s | 63592 ko | ToTemplate/Utils/ByteCompareSpec.vo | 0m00.04s | 64228 ko || +0m00.01s || -636 ko | +25.00% | -0.99%
0m00.04s | 63060 ko | ToTemplate/Common/Transform.vo | 0m00.05s | 64720 ko || -0m00.01s || -1660 ko | -20.00% | -2.56%
0m00.04s | 63428 ko | ToTemplate/Template/ReflectAst.vo | 0m00.05s | 64352 ko || -0m00.01s || -924 ko | -20.00% | -1.43%
0m00.04s | 63860 ko | ToTemplate/Utils/MCSquash.vo | 0m00.06s | 63524 ko || -0m00.01s || 336 ko | -33.33% | +0.52%
0m00.03s | 64740 ko | ToTemplate/Template/Induction.vo | 0m00.05s | 64888 ko || -0m00.02s || -148 ko | -40.00% | -0.22%
0m00.03s | 64172 ko | ToTemplate/Template/UnivSubst.vo | 0m00.02s | 63464 ko || +0m00.00s || 708 ko | +49.99% | +1.11%
0m00.03s | 63548 ko | ToTemplate/Utils/ByteCompare_opt.vo | 0m00.05s | 64136 ko || -0m00.02s || -588 ko | -40.00% | -0.91%
```
</p>
</details>
JasonGross
force-pushed
the
coq-8.16+quotation-better-universes
branch
from
aa4c2bb to
8bd85e5
Compare
|
I guess the slowest remaining file, |
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.
This should both speed things up and potentially avoid universe inconsistencies.
Timing Diff