Recursive TemplateMonad programs are slow to run #441

john-ml · 2020-07-16T22:45:52Z

The runtime of the following function increases drastically with n (comments give the runtimes on my machine):

From MetaCoq Require Import Template.All.
Import MonadNotation.

Fixpoint tm_double n : TemplateMonad nat :=
  match n with
  | 0 => ret 0
  | S n =>
    n' <- tm_double n ;;
    ret (S (S n'))
  end.

Time Run TemplateProgram (tmPrint =<< tm_double 1000). (*  1.296s *)
Time Run TemplateProgram (tmPrint =<< tm_double 2000). (*  4.444s *)
Time Run TemplateProgram (tmPrint =<< tm_double 3000). (* 10.117s *)
Time Run TemplateProgram (tmPrint =<< tm_double 4000). (* 21.374s *)
Time Run TemplateProgram (tmPrint =<< tm_double 5000). (* 29.005s *)

This prevents me from writing nontrivial recursive functions in the template monad.

The text was updated successfully, but these errors were encountered:

gmalecha · 2020-08-02T17:30:10Z

I think that this is an implementation issue in the interpreter. Mtac2 uses a strategy where they work directly on the reduction mechanism whereas the one here is (I'm pretty sure) just calls to hnf followed by pattern matches.

It is possible that we could improve this by fusing tmBind with each operation and then implementing tmBind as a function. This would avoid places where we have tmBind (tmBind .. ..) .. and keep computation within the Coq kernel in that case. In your example, you will essentially build a tmBind (tmBind (tmBind .. ..) ..) ..) ..) tower before actually making any progress which is sub-optimal at best. Out of curiosity, what impact does cps converting this have?

Fixpoint tm_double n (acc : nat) : TemplateMonad nat :=
  match n with
  | 0 => ret acc
  | S n =>
    tm_double n (S (S acc)) 
  end.

I assume that evaluating the above will be significantly faster since there is no tmBinds at all. This is an upper bound on the performance improvement that you could expect from the proposal above but there would be some extra overhead to normalize things. Personally, it seems like both fixing the interpreter and making tmBind a function should be done, but they are different amounts of work.

john-ml · 2020-08-02T17:43:18Z

Out of curiosity, what inpact does cps converting this have?

The CPS converted version is indeed significantly faster---the same benchmarks finish near-instantly.

Fixes MetaCoq#441

This is partial work towards MetaCoq#441.

Fixes MetaCoq#441

Fixes MetaCoq#441 <details><summary>Timing Diff</summary> ``` No timing data ``` </details>

Fixes MetaCoq#441 <details><summary>Timing Diff</summary> ``` No timing data ``` </details> <details><summary>Timing Diff</summary> ``` No timing data ``` </details>

Fixes MetaCoq#441 <details><summary>Timing Diff</summary> ``` No timing data ``` </details> <details><summary>Timing Diff</summary> ``` No timing data ``` </details> <details><summary>Timing Diff</summary> ``` No timing data ``` </details>

Fixes MetaCoq#441

Fixes #441 <details><summary>Timing Diff</summary> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 55m51.35s | 3100356 ko | Total Time / Peak Mem | 54m30.12s | 3101084 ko || +1m21.23s || -728 ko | +2.48% | -0.02% ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 1m16.14s | 1632284 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.vo | 1m09.01s | 1641988 ko || +0m07.12s || -9704 ko | +10.33% | -0.59% 1m13.23s | 1802048 ko | ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.vo | 1m05.28s | 1790720 ko || +0m07.95s || 11328 ko | +12.17% | +0.63% 0m28.45s | 1305696 ko | ToTemplate/Common/EnvironmentTyping.vo | 0m20.61s | 1301284 ko || +0m07.83s || 4412 ko | +38.03% | +0.33% 0m21.90s | 1159880 ko | ToTemplate/Template/Typing.vo | 0m17.21s | 1146964 ko || +0m04.68s || 12916 ko | +27.25% | +1.12% 0m23.80s | 1434644 ko | uGraph.vo | 0m20.31s | 1437728 ko || +0m03.49s || -3084 ko | +17.18% | -0.21% 0m16.48s | 934048 ko | ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.vo | 0m12.89s | 927988 ko || +0m03.58s || 6060 ko | +27.85% | +0.65% 2m14.92s | 2283076 ko | PCUICTypeChecker.vo | 2m17.63s | 2283164 ko || -0m02.71s || -88 ko | -1.96% | -0.00% 1m11.82s | 1356176 ko | PCUICParallelReductionConfluence.vo | 1m09.27s | 1351576 ko || +0m02.54s || 4600 ko | +3.68% | +0.34% 0m45.45s | 1277812 ko | ByteCompareSpec.vo | 0m42.86s | 1279880 ko || +0m02.59s || -2068 ko | +6.04% | -0.16% 0m15.47s | 1074800 ko | ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.vo | 0m13.38s | 1033856 ko || +0m02.08s || 40944 ko | +15.62% | +3.96% 0m12.77s | 874736 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.vo | 0m10.67s | 876020 ko || +0m02.09s || -1284 ko | +19.68% | -0.14% 0m07.43s | 1058920 ko | ToTemplate/Template/WfAst.vo | 0m05.36s | 1059712 ko || +0m02.06s || -792 ko | +38.61% | -0.07% 4m22.24s | 2085704 ko | PCUICSafeConversion.vo | 4m23.65s | 2085152 ko || -0m01.40s || 552 ko | -0.53% | +0.02% 0m50.56s | 2185660 ko | PCUICConversion.vo | 0m49.16s | 2181016 ko || +0m01.40s || 4644 ko | +2.84% | +0.21% 0m46.08s | 1361592 ko | Typed/OptimizeCorrectness.vo | 0m44.76s | 1361288 ko || +0m01.32s || 304 ko | +2.94% | +0.02% 0m15.28s | 870392 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.vo | 0m14.03s | 865688 ko || +0m01.25s || 4704 ko | +8.90% | +0.54% 0m14.89s | 859872 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.vo | 0m13.05s | 859148 ko || +0m01.83s || 724 ko | +14.09% | +0.08% 0m14.39s | 849784 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.vo | 0m12.48s | 855744 ko || +0m01.91s || -5960 ko | +15.30% | -0.69% 0m14.36s | 857096 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.vo | 0m12.56s | 857636 ko || +0m01.79s || -540 ko | +14.33% | -0.06% 0m12.65s | 914672 ko | Conversion/PCUICRenameConv.vo | 0m11.52s | 914804 ko || +0m01.13s || -132 ko | +9.80% | -0.01% 0m12.30s | 887812 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.vo | 0m11.26s | 881520 ko || +0m01.04s || 6292 ko | +9.23% | +0.71% 0m11.44s | 872644 ko | ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.vo | 0m09.99s | 874160 ko || +0m01.44s || -1516 ko | +14.51% | -0.17% 0m11.43s | 945104 ko | ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.vo | 0m09.83s | 982336 ko || +0m01.59s || -37232 ko | +16.27% | -3.79% 0m07.38s | 1059380 ko | ToTemplate/Template/TermEquality.vo | 0m05.73s | 1057968 ko || +0m01.64s || 1412 ko | +28.79% | +0.13% 0m06.49s | 986272 ko | ToTemplate/Common/Environment.vo | 0m04.73s | 985104 ko || +0m01.75s || 1168 ko | +37.20% | +0.11% 0m06.29s | 832232 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.vo | 0m05.27s | 828496 ko || +0m01.02s || 3736 ko | +19.35% | +0.45% 0m03.62s | 799328 ko | ToTemplate/QuotationOf/Coq/Structures/Equalities/Sig.vo | 0m02.53s | 801168 ko || +0m01.09s || -1840 ko | +43.08% | -0.22% 2m48.38s | 1394740 ko | PCUICRetypingEnvIrrelevance.vo | 2m48.94s | 1392792 ko || -0m00.56s || 1948 ko | -0.33% | +0.13% 2m39.53s | 3100356 ko | ErasureFunction.vo | 2m39.98s | 3101084 ko || -0m00.44s || -728 ko | -0.28% | -0.02% 1m52.23s | 1554220 ko | PCUICSafeReduce.vo | 1m51.79s | 1553200 ko || +0m00.43s || 1020 ko | +0.39% | +0.06% 1m11.79s | 2419756 ko | PCUICConfluence.vo | 1m12.41s | 2420136 ko || -0m00.62s || -380 ko | -0.85% | -0.01% 0m50.05s | 1329392 ko | PCUICSafeRetyping.vo | 0m49.37s | 1328380 ko || +0m00.67s || 1012 ko | +1.37% | +0.07% 0m48.12s | 1581644 ko | PCUICSR.vo | 0m48.41s | 1583312 ko || -0m00.28s || -1668 ko | -0.59% | -0.10% 0m47.73s | 1022336 ko | EEtaExpandedFix.vo | 0m47.51s | 1022044 ko || +0m00.21s || 292 ko | +0.46% | +0.02% 0m46.40s | 1245348 ko | PCUICExpandLetsCorrectness.vo | 0m45.87s | 1245448 ko || +0m00.53s || -100 ko | +1.15% | -0.00% 0m41.20s | 1304432 ko | PCUICParallelReduction.vo | 0m41.85s | 1309152 ko || -0m00.64s || -4720 ko | -1.55% | -0.36% 0m38.98s | 1047264 ko | PCUICSigmaCalculus.vo | 0m38.89s | 1046812 ko || +0m00.08s || 452 ko | +0.23% | +0.04% 0m32.62s | 1118676 ko | Conversion/PCUICInstConv.vo | 0m31.85s | 1120584 ko || +0m00.76s || -1908 ko | +2.41% | -0.17% 0m31.10s | 1114448 ko | PCUICInductiveInversion.vo | 0m30.99s | 1111244 ko || +0m00.11s || 3204 ko | +0.35% | +0.28% 0m27.17s | 1110232 ko | PCUICSpine.vo | 0m26.86s | 1110176 ko || +0m00.31s || 56 ko | +1.15% | +0.00% 0m25.95s | 1100860 ko | EWcbvEval.vo | 0m25.73s | 1100976 ko || +0m00.21s || -116 ko | +0.85% | -0.01% 0m24.52s | 1168904 ko | PCUICSafeChecker.vo | 0m24.94s | 1168980 ko || -0m00.42s || -76 ko | -1.68% | -0.00% 0m23.99s | 1265208 ko | ErasureCorrectness.vo | 0m24.46s | 1264596 ko || -0m00.47s || 612 ko | -1.92% | +0.04% 0m22.50s | 1043068 ko | TemplateToPCUICCorrectness.vo | 0m22.24s | 1043052 ko || +0m00.26s || 16 ko | +1.16% | +0.00% 0m22.27s | 1114944 ko | PCUICEquality.vo | 0m21.72s | 1112504 ko || +0m00.55s || 2440 ko | +2.53% | +0.21% 0m21.63s | 984792 ko | ERemoveParams.vo | 0m21.54s | 985820 ko || +0m00.08s || -1028 ko | +0.41% | -0.10% 0m21.41s | 922692 ko | Typing.vo | 0m21.42s | 922792 ko || -0m00.01s || -100 ko | -0.04% | -0.01% 0m19.90s | 992736 ko | PCUICPrincipality.vo | 0m20.79s | 993036 ko || -0m00.89s || -300 ko | -4.28% | -0.03% 0m19.52s | 947280 ko | PCUICWcbvEval.vo | 0m19.61s | 945216 ko || -0m00.08s || 2064 ko | -0.45% | +0.21% 0m19.09s | 927996 ko | PCUICContextConversion.vo | 0m18.66s | 929172 ko || +0m00.42s || -1176 ko | +2.30% | -0.12% 0m18.80s | 900880 ko | PCUICWfUniverses.vo | 0m18.29s | 899852 ko || +0m00.51s || 1028 ko | +2.78% | +0.11% 0m18.06s | 1002184 ko | PCUICTyping.vo | 0m18.18s | 999600 ko || -0m00.12s || 2584 ko | -0.66% | +0.25% 0m17.97s | 913736 ko | Syntax/PCUICOnFreeVars.vo | 0m17.24s | 912672 ko || +0m00.73s || 1064 ko | +4.23% | +0.11% 0m17.52s | 1029036 ko | ErasureProperties.vo | 0m17.51s | 1028488 ko || +0m00.00s || 548 ko | +0.05% | +0.05% 0m17.42s | 1086728 ko | Typed/Erasure.vo | 0m17.37s | 1085240 ko || +0m00.05s || 1488 ko | +0.28% | +0.13% 0m16.97s | 851412 ko | Syntax/PCUICClosed.vo | 0m17.16s | 852008 ko || -0m00.19s || -596 ko | -1.10% | -0.06% 0m16.91s | 1056300 ko | PCUICNormal.vo | 0m16.68s | 1058444 ko || +0m00.23s || -2144 ko | +1.37% | -0.20% 0m16.47s | 1182100 ko | ToTemplate/QuotationOf/Common/EnvironmentTyping/Sig.vo | 0m16.58s | 1186608 ko || -0m00.10s || -4508 ko | -0.66% | -0.37% 0m16.32s | 927268 ko | EtaExpand.vo | 0m15.66s | 927188 ko || +0m00.66s || 80 ko | +4.21% | +0.00% 0m16.13s | 965628 ko | PCUICInductives.vo | 0m15.98s | 968672 ko || +0m00.14s || -3044 ko | +0.93% | -0.31% 0m15.66s | 925032 ko | PCUICSubstitution.vo | 0m14.92s | 924984 ko || +0m00.74s || 48 ko | +4.95% | +0.00% 0m15.47s | 983984 ko | EConstructorsAsBlocks.vo | 0m15.36s | 984812 ko || +0m00.11s || -828 ko | +0.71% | -0.08% 0m14.86s | 1003720 ko | PCUICCumulProp.vo | 0m14.99s | 999676 ko || -0m00.13s || 4044 ko | -0.86% | +0.40% 0m14.71s | 824652 ko | ELiftSubst.vo | 0m14.46s | 823844 ko || +0m00.25s || 808 ko | +1.72% | +0.09% 0m14.48s | 1348108 ko | EWcbvEvalNamed.vo | 0m14.46s | 1348592 ko || +0m00.01s || -484 ko | +0.13% | -0.03% 0m14.46s | 999052 ko | PCUICConvCumInversion.vo | 0m14.24s | 999148 ko || +0m00.22s || -96 ko | +1.54% | -0.00% 0m14.29s | 1034560 ko | Syntax/PCUICPosition.vo | 0m13.91s | 1034840 ko || +0m00.37s || -280 ko | +2.73% | -0.02% 0m13.86s | 837460 ko | UniversesDec.vo | 0m13.23s | 839184 ko || +0m00.62s || -1724 ko | +4.76% | -0.20% 0m13.67s | 878320 ko | EEtaExpanded.vo | 0m13.78s | 878468 ko || -0m00.10s || -148 ko | -0.79% | -0.01% 0m13.65s | 1034068 ko | Bidirectional/BDUnique.vo | 0m13.07s | 1035320 ko || +0m00.58s || -1252 ko | +4.43% | -0.12% 0m13.60s | 1016744 ko | PCUICToTemplateCorrectness.vo | 0m13.63s | 1020824 ko || -0m00.03s || -4080 ko | -0.22% | -0.39% 0m13.12s | 1064192 ko | PCUICEqualityDec.vo | 0m13.21s | 1064180 ko || -0m00.09s || 12 ko | -0.68% | +0.00% 0m12.85s | 860492 ko | Syntax/PCUICLiftSubst.vo | 0m12.31s | 863856 ko || +0m00.53s || -3364 ko | +4.38% | -0.38% 0m12.66s | 965432 ko | PCUICAlpha.vo | 0m12.80s | 966800 ko || -0m00.14s || -1368 ko | -1.09% | -0.14% 0m12.16s | 866212 ko | EWellformed.vo | 0m11.84s | 866092 ko || +0m00.32s || 120 ko | +2.70% | +0.01% 0m11.99s | 620260 ko | wGraph.vo | 0m11.36s | 619948 ko || +0m00.63s || 312 ko | +5.54% | +0.05% 0m11.86s | 954876 ko | ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.vo | 0m10.90s | 940440 ko || +0m00.95s || 14436 ko | +8.80% | +1.53% 0m11.46s | 811992 ko | LiftSubst.vo | 0m11.28s | 812472 ko || +0m00.18s || -480 ko | +1.59% | -0.05% 0m10.69s | 947604 ko | EOptimizePropDiscr.vo | 0m10.81s | 947568 ko || -0m00.12s || 36 ko | -1.11% | +0.00% 0m10.56s | 906820 ko | Typing/PCUICRenameTyp.vo | 0m10.07s | 907072 ko || +0m00.49s || -252 ko | +4.86% | -0.02% 0m10.39s | 934440 ko | PCUICWellScopedCumulativity.vo | 0m10.07s | 934656 ko || +0m00.32s || -216 ko | +3.17% | -0.02% 0m10.27s | 942596 ko | EWcbvEvalCstrsAsBlocksFixLambdaInd.vo | 0m10.16s | 942940 ko || +0m00.10s || -344 ko | +1.08% | -0.03% 0m09.95s | 920116 ko | ToTemplate/QuotationOf/Common/Environment/Sig.vo | 0m09.20s | 915556 ko || +0m00.75s || 4560 ko | +8.15% | +0.49% 0m09.89s | 932192 ko | PCUICInversion.vo | 0m09.86s | 932188 ko || +0m00.03s || 4 ko | +0.30% | +0.00% 0m09.72s | 995656 ko | Typed/WcbvEvalAux.vo | 0m09.63s | 994256 ko || +0m00.08s || 1400 ko | +0.93% | +0.14% 0m09.20s | 929512 ko | EnvironmentTyping.vo | 0m08.82s | 931124 ko || +0m00.37s || -1612 ko | +4.30% | -0.17% 0m08.96s | 966456 ko | PCUICArities.vo | 0m09.04s | 965500 ko || -0m00.07s || 956 ko | -0.88% | +0.09% 0m08.57s | 894340 ko | Conversion/PCUICNamelessConv.vo | 0m08.50s | 894596 ko || +0m00.07s || -256 ko | +0.82% | -0.02% 0m08.53s | 972256 ko | EDeps.vo | 0m08.92s | 970240 ko || -0m00.39s || 2016 ko | -4.37% | +0.20% 0m08.52s | 947428 ko | ESubstitution.vo | 0m08.59s | 948356 ko || -0m00.07s || -928 ko | -0.81% | -0.09% 0m08.34s | 881252 ko | PCUICContexts.vo | 0m07.88s | 880936 ko || +0m00.46s || 316 ko | +5.83% | +0.03% 0m08.31s | 895884 ko | Conversion/PCUICUnivSubstitutionConv.vo | 0m08.09s | 894428 ko || +0m00.22s || 1456 ko | +2.71% | +0.16% 0m08.30s | 918576 ko | EWcbvEvalEtaInd.vo | 0m08.64s | 915772 ko || -0m00.33s || 2804 ko | -3.93% | +0.30% 0m08.30s | 884536 ko | Typing/PCUICInstTyp.vo | 0m08.34s | 881820 ko || -0m00.03s || 2716 ko | -0.47% | +0.30% 0m08.28s | 933904 ko | EInlineProjections.vo | 0m08.43s | 933400 ko || -0m00.15s || 504 ko | -1.77% | +0.05% 0m08.05s | 943040 ko | PCUICCanonicity.vo | 0m08.15s | 943236 ko || -0m00.09s || -196 ko | -1.22% | -0.02% 0m07.68s | 832784 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.vo | 0m06.89s | 822552 ko || +0m00.79s || 10232 ko | +11.46% | +1.24% 0m07.46s | 921956 ko | Typing/PCUICWeakeningConfigTyp.vo | 0m07.46s | 920328 ko || +0m00.00s || 1628 ko | +0.00% | +0.17% 0m07.36s | 860768 ko | Typing/PCUICClosedTyp.vo | 0m07.55s | 860912 ko || -0m00.18s || -144 ko | -2.51% | -0.01% 0m07.26s | 881804 ko | times_bool_fun.vo | 0m06.80s | 882624 ko || +0m00.46s || -820 ko | +6.76% | -0.09% 0m07.11s | 906032 ko | Bidirectional/BDStrengthening.vo | 0m07.25s | 906552 ko || -0m00.13s || -520 ko | -1.93% | -0.05% 0m07.08s | 841896 ko | TypingWf.vo | 0m07.13s | 841328 ko || -0m00.04s || 568 ko | -0.70% | +0.06% 0m06.94s | 958420 ko | TemplateToPCUICWcbvEval.vo | 0m07.05s | 955952 ko || -0m00.10s || 2468 ko | -1.56% | +0.25% 0m06.86s | 821504 ko | Syntax/PCUICUnivSubst.vo | 0m06.80s | 820692 ko || +0m00.06s || 812 ko | +0.88% | +0.09% 0m06.80s | 934628 ko | PCUICElimination.vo | 0m07.23s | 934172 ko || -0m00.43s || 456 ko | -5.94% | +0.04% 0m06.75s | 892964 ko | PCUICCasesHelper.vo | 0m06.67s | 892816 ko || +0m00.08s || 148 ko | +1.19% | +0.01% 0m06.58s | 1113144 ko | ToTemplate/Coq/MSets.vo | 0m06.01s | 1076552 ko || +0m00.57s || 36592 ko | +9.48% | +3.39% 0m06.57s | 527096 ko | All_Forall.vo | 0m06.37s | 527668 ko || +0m00.20s || -572 ko | +3.13% | -0.10% 0m06.33s | 919488 ko | EArities.vo | 0m06.42s | 922716 ko || -0m00.08s || -3228 ko | -1.40% | -0.34% 0m06.24s | 841360 ko | ToTemplate/QuotationOf/Template/Ast/Env/Instances.vo | 0m06.10s | 848544 ko || +0m00.14s || -7184 ko | +2.29% | -0.84% 0m05.90s | 894784 ko | PCUICEtaExpand.vo | 0m05.99s | 894648 ko || -0m00.08s || 136 ko | -1.50% | +0.01% 0m05.73s | 894636 ko | Typing/PCUICContextConversionTyp.vo | 0m05.83s | 889988 ko || -0m00.09s || 4648 ko | -1.71% | +0.52% 0m05.60s | 818316 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.vo | 0m05.04s | 827232 ko || +0m00.55s || -8916 ko | +11.11% | -1.07% 0m05.40s | 853160 ko | Conversion/PCUICOnFreeVarsConv.vo | 0m05.24s | 853176 ko || +0m00.16s || -16 ko | +3.05% | -0.00% 0m05.31s | 890188 ko | EWcbvEvalCstrsAsBlocksInd.vo | 0m05.09s | 888856 ko || +0m00.21s || 1332 ko | +4.32% | +0.14% 0m05.28s | 863400 ko | Typing/PCUICUnivSubstitutionTyp.vo | 0m05.64s | 862668 ko || -0m00.35s || 732 ko | -6.38% | +0.08% 0m05.24s | 774532 ko | Universes.vo | 0m05.26s | 774668 ko || -0m00.01s || -136 ko | -0.38% | -0.01% 0m05.21s | 901132 ko | ToTemplate/QuotationOf/Template/Typing/TemplateEnvTyping/Instances.vo | 0m05.16s | 890940 ko || +0m00.04s || 10192 ko | +0.96% | +1.14% 0m05.20s | 783880 ko | WcbvEval.vo | 0m05.21s | 785540 ko || -0m00.00s || -1660 ko | -0.19% | -0.21% 0m05.19s | 855116 ko | Bidirectional/BDTyping.vo | 0m05.26s | 850480 ko || -0m00.06s || 4636 ko | -1.33% | +0.54% 0m05.17s | 906096 ko | PCUICFirstorder.vo | 0m05.19s | 906676 ko || -0m00.02s || -580 ko | -0.38% | -0.06% 0m05.12s | 914600 ko | PCUICProgress.vo | 0m05.13s | 915224 ko || -0m00.00s || -624 ko | -0.19% | -0.06% 0m05.11s | 844812 ko | PCUICReduction.vo | 0m05.05s | 844324 ko || +0m00.06s || 488 ko | +1.18% | +0.05% 0m05.00s | 872084 ko | PCUICContextReduction.vo | 0m05.01s | 870408 ko || -0m00.00s || 1676 ko | -0.19% | +0.19% 0m04.94s | 779368 ko | TermEquality.vo | 0m04.96s | 780648 ko || -0m00.01s || -1280 ko | -0.40% | -0.16% 0m04.92s | 918480 ko | TemplateToPCUICExpanded.vo | 0m04.71s | 918332 ko || +0m00.20s || 148 ko | +4.45% | +0.01% 0m04.73s | 903548 ko | ToTemplate/Coq/FSets.vo | 0m03.88s | 901912 ko || +0m00.85s || 1636 ko | +21.90% | +0.18% 0m04.68s | 783620 ko | PCUICAst.vo | 0m04.64s | 784380 ko || +0m00.04s || -760 ko | +0.86% | -0.09% 0m04.66s | 736332 ko | Environment.vo | 0m04.48s | 735356 ko || +0m00.17s || 976 ko | +4.01% | +0.13% 0m04.53s | 821968 ko | ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.vo | 0m04.24s | 829116 ko || +0m00.29s || -7148 ko | +6.83% | -0.86% 0m04.53s | 863240 ko | ToTemplate/QuotationOf/Template/Typing/TemplateGlobalMaps/Instances.vo | 0m04.45s | 861816 ko || +0m00.08s || 1424 ko | +1.79% | +0.16% 0m04.51s | 960120 ko | ToTemplate/Common/Universes.vo | 0m04.02s | 961812 ko || +0m00.49s || -1692 ko | +12.18% | -0.17% 0m04.41s | 892628 ko | Bidirectional/BDToPCUIC.vo | 0m04.27s | 892628 ko || +0m00.14s || 0 ko | +3.27% | +0.00% 0m04.41s | 849932 ko | Conversion/PCUICWeakeningEnvConv.vo | 0m04.10s | 850004 ko || +0m00.31s || -72 ko | +7.56% | -0.00% 0m04.37s | 912276 ko | PCUICSafeLemmata.vo | 0m04.48s | 914012 ko || -0m00.11s || -1736 ko | -2.45% | -0.18% 0m04.37s | 1044468 ko | Typed/ErasureCorrectness.vo | 0m04.35s | 1044608 ko || +0m00.02s || -140 ko | +0.45% | -0.01% 0m04.29s | 1062988 ko | Extraction.vo | 0m04.26s | 1063612 ko || +0m00.03s || -624 ko | +0.70% | -0.05% 0m04.29s | 727200 ko | Kernames.vo | 0m04.47s | 729924 ko || -0m00.17s || -2724 ko | -4.02% | -0.37% 0m04.22s | 893696 ko | PCUICValidity.vo | 0m04.35s | 892668 ko || -0m00.12s || 1028 ko | -2.98% | +0.11% 0m04.14s | 770328 ko | UnivSubst.vo | 0m04.90s | 769344 ko || -0m00.76s || 984 ko | -15.51% | +0.12% 0m04.11s | 823284 ko | ReflectAst.vo | 0m05.10s | 821492 ko || -0m00.98s || 1792 ko | -19.41% | +0.21% 0m04.10s | 922912 ko | EGenericMapEnv.vo | 0m04.14s | 921080 ko || -0m00.04s || 1832 ko | -0.96% | +0.19% 0m04.08s | 892140 ko | Bidirectional/BDFromPCUIC.vo | 0m03.96s | 892356 ko || +0m00.12s || -216 ko | +3.03% | -0.02% 0m04.07s | 848564 ko | Typing/PCUICWeakeningEnvTyp.vo | 0m03.66s | 848476 ko || +0m00.41s || 88 ko | +11.20% | +0.01% 0m04.05s | 845280 ko | Syntax/PCUICReflect.vo | 0m04.03s | 844008 ko || +0m00.01s || 1272 ko | +0.49% | +0.15% 0m03.93s | 812692 ko | ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.vo | 0m03.83s | 819012 ko || +0m00.10s || -6320 ko | +2.61% | -0.77% 0m03.84s | 911188 ko | param_generous_packed.vo | 0m03.90s | 916344 ko || -0m00.06s || -5156 ko | -1.53% | -0.56% 0m03.71s | 920876 ko | PCUICWfReduction.vo | 0m03.84s | 921144 ko || -0m00.12s || -268 ko | -3.38% | -0.02% 0m03.65s | 824952 ko | utils/PCUICAstUtils.vo | 0m03.65s | 823420 ko || +0m00.00s || 1532 ko | +0.00% | +0.18% 0m03.64s | 910484 ko | PCUICWfEnvImpl.vo | 0m03.66s | 910424 ko || -0m00.02s || 60 ko | -0.54% | +0.00% 0m03.64s | 782192 ko | WfAst.vo | 0m04.01s | 780548 ko || -0m00.36s || 1644 ko | -9.22% | +0.21% 0m03.61s | 809972 ko | ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.vo | 0m03.75s | 815048 ko || -0m00.14s || -5076 ko | -3.73% | -0.62% 0m03.60s | 851360 ko | Checker.vo | 0m03.67s | 852148 ko || -0m00.06s || -788 ko | -1.90% | -0.09% 0m03.55s | 803224 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.vo | 0m03.30s | 802232 ko || +0m00.25s || 992 ko | +7.57% | +0.12% 0m03.52s | 818516 ko | Syntax/PCUICDepth.vo | 0m03.46s | 817568 ko || +0m00.06s || 948 ko | +1.73% | +0.11% 0m03.49s | 833484 ko | ToTemplate/QuotationOf/Utils/MCMSets/Sig.vo | 0m03.68s | 832740 ko || -0m00.18s || 744 ko | -5.16% | +0.08% 0m03.45s | 845884 ko | Conversion/PCUICWeakeningConfigConv.vo | 0m03.28s | 843928 ko || +0m00.17s || 1956 ko | +5.18% | +0.23% 0m03.44s | 810052 ko | ToTemplate/Coq/Init.vo | 0m02.92s | 807396 ko || +0m00.52s || 2656 ko | +17.80% | +0.32% 0m03.43s | 910028 ko | PCUICWfEnv.vo | 0m03.41s | 911392 ko || +0m00.02s || -1364 ko | +0.58% | -0.14% 0m03.40s | 824912 ko | Syntax/PCUICInduction.vo | 0m03.41s | 825424 ko || -0m00.01s || -512 ko | -0.29% | -0.06% 0m03.33s | 851964 ko | PCUICRedTypeIrrelevance.vo | 0m03.36s | 851668 ko || -0m00.02s || 296 ko | -0.89% | +0.03% 0m03.33s | 837152 ko | times_bool_fun2.vo | 0m03.42s | 836444 ko || -0m00.08s || 708 ko | -2.63% | +0.08% 0m03.32s | 867724 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversion/Instances.vo | 0m03.46s | 867584 ko || -0m00.14s || 140 ko | -4.04% | +0.01% 0m03.27s | 830628 ko | Typed/ClosedAux.vo | 0m03.35s | 829380 ko || -0m00.08s || 1248 ko | -2.38% | +0.15% 0m03.16s | 776476 ko | EInduction.vo | 0m03.10s | 775856 ko || +0m00.06s || 620 ko | +1.93% | +0.07% 0m03.11s | 853220 ko | ToTemplate/QuotationOf/Template/Ast/TemplateLookup/Instances.vo | 0m03.03s | 850768 ko || +0m00.08s || 2452 ko | +2.64% | +0.28% 0m03.00s | 822588 ko | ToTemplate/QuotationOf/Utils/MCFSets/Sig.vo | 0m03.06s | 823584 ko || -0m00.06s || -996 ko | -1.96% | -0.12% 0m02.90s | 920260 ko | Prelim.vo | 0m02.98s | 923452 ko || -0m00.08s || -3192 ko | -2.68% | -0.34% 0m02.89s | 792216 ko | EReflect.vo | 0m02.90s | 790940 ko || -0m00.00s || 1276 ko | -0.34% | +0.16% 0m02.88s | 838560 ko | PCUICCumulativitySpec.vo | 0m02.80s | 839404 ko || +0m00.08s || -844 ko | +2.85% | -0.10% 0m02.81s | 804472 ko | ToTemplate/QuotationOf/Coq/FSets/FMapInterface/Sig.vo | 0m02.69s | 804048 ko || +0m00.12s || 424 ko | +4.46% | +0.05% 0m02.79s | 735800 ko | Reflect.vo | 0m02.75s | 736872 ko || +0m00.04s || -1072 ko | +1.45% | -0.14% 0m02.79s | 817792 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetExtraDecide/Instances.vo | 0m02.45s | 820280 ko || +0m00.33s || -2488 ko | +13.87% | -0.30% 0m02.79s | 798960 ko | ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.vo | 0m02.76s | 800356 ko || +0m00.03s || -1396 ko | +1.08% | -0.17% 0m02.75s | 820112 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapDecide/Instances.vo | 0m02.74s | 822600 ko || +0m00.00s || -2488 ko | +0.36% | -0.30% 0m02.71s | 1039492 ko | SafeTemplateChecker.vo | 0m02.74s | 1038752 ko || -0m00.03s || 740 ko | -1.09% | +0.07% 0m02.66s | 1056696 ko | ToTemplate/Template/Ast.vo | 0m02.60s | 1056880 ko || +0m00.06s || -184 ko | +2.30% | -0.01% 0m02.65s | 819708 ko | Syntax/PCUICCases.vo | 0m02.64s | 824128 ko || +0m00.00s || -4420 ko | +0.37% | -0.53% 0m02.58s | 947292 ko | Typed/CertifyingInlining.vo | 0m02.67s | 947884 ko || -0m00.08s || -592 ko | -3.37% | -0.06% 0m02.57s | 828372 ko | PCUICContextSubst.vo | 0m02.46s | 827776 ko || +0m00.10s || 596 ko | +4.47% | +0.07% 0m02.55s | 945696 ko | Typed/CertifyingBeta.vo | 0m02.57s | 946312 ko || -0m00.02s || -616 ko | -0.77% | -0.06% 0m02.48s | 852488 ko | EWcbvEvalInd.vo | 0m02.32s | 852264 ko || +0m00.16s || 224 ko | +6.89% | +0.02% 0m02.46s | 841304 ko | translation_utils.vo | 0m02.48s | 843552 ko || -0m00.02s || -2248 ko | -0.80% | -0.26% 0m02.43s | 687872 ko | BasicAst.vo | 0m02.31s | 688672 ko || +0m00.12s || -800 ko | +5.19% | -0.11% 0m02.41s | 906244 ko | PCUICNormalization.vo | 0m02.36s | 907128 ko || +0m00.05s || -884 ko | +2.11% | -0.09% 0m02.41s | 934364 ko | ToTemplate/Common/Kernames.vo | 0m02.53s | 932184 ko || -0m00.11s || 2180 ko | -4.74% | +0.23% 0m02.40s | 853032 ko | Conversion/PCUICWeakeningConv.vo | 0m02.39s | 852692 ko || +0m00.00s || 340 ko | +0.41% | +0.03% 0m02.38s | 956236 ko | PCUICTransform.vo | 0m02.45s | 956644 ko || -0m00.07s || -408 ko | -2.85% | -0.04% 0m02.37s | 801120 ko | ToTemplate/Utils/All_Forall.vo | 0m01.94s | 801828 ko || +0m00.43s || -708 ko | +22.16% | -0.08% 0m02.36s | 822124 ko | Syntax/PCUICViews.vo | 0m02.34s | 822132 ko || +0m00.02s || -8 ko | +0.85% | -0.00% 0m02.34s | 900632 ko | Extract.vo | 0m02.35s | 901388 ko || -0m00.01s || -756 ko | -0.42% | -0.08% 0m02.34s | 820292 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetExtraDecide/Instances.vo | 0m02.37s | 822312 ko || -0m00.03s || -2020 ko | -1.26% | -0.24% 0m02.32s | 827228 ko | PCUICErrors.vo | 0m02.49s | 827348 ko || -0m00.17s || -120 ko | -6.82% | -0.01% 0m02.32s | 818804 ko | ToTemplate/Init.vo | 0m02.02s | 816280 ko || +0m00.29s || 2524 ko | +14.85% | +0.30% 0m02.32s | 820452 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetExtraDecide/Instances.vo | 0m02.22s | 821096 ko || +0m00.09s || -644 ko | +4.50% | -0.07% 0m02.32s | 800816 ko | ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.vo | 0m02.04s | 804060 ko || +0m00.27s || -3244 ko | +13.72% | -0.40% 0m02.29s | 972612 ko | ToTemplate/QuotationOf/Template/Ast/EnvHelper/Instances.vo | 0m02.27s | 973124 ko || +0m00.02s || -512 ko | +0.88% | -0.05% 0m02.27s | 633640 ko | MCFSets.vo | 0m02.15s | 633424 ko || +0m00.12s || 216 ko | +5.58% | +0.03% 0m02.27s | 841932 ko | PCUICCumulativity.vo | 0m02.32s | 841096 ko || -0m00.04s || 836 ko | -2.15% | +0.09% 0m02.27s | 944948 ko | Typed/Optimize.vo | 0m02.34s | 945264 ko || -0m00.06s || -316 ko | -2.99% | -0.03% 0m02.22s | 938368 ko | Typed/Annotations.vo | 0m02.17s | 938824 ko || +0m00.05s || -456 ko | +2.30% | -0.04% 0m02.21s | 897268 ko | PCUICSN.vo | 0m02.24s | 896764 ko || -0m00.03s || 504 ko | -1.33% | +0.05% 0m02.20s | 842116 ko | PCUICWeakeningEnv.vo | 0m02.39s | 842780 ko || -0m00.18s || -664 ko | -7.94% | -0.07% 0m02.17s | 363628 ko | MiniHoTT.vo | 0m02.05s | 359728 ko || +0m00.12s || 3900 ko | +5.85% | +1.08% 0m02.17s | 918680 ko | Typed/OptimizePropDiscr.vo | 0m02.14s | 918536 ko || +0m00.02s || 144 ko | +1.40% | +0.01% 0m02.14s | 842556 ko | PCUICCSubst.vo | 0m02.16s | 842540 ko || -0m00.02s || 16 ko | -0.92% | +0.00% 0m02.14s | 903320 ko | PCUICConsistency.vo | 0m02.18s | 904636 ko || -0m00.04s || -1316 ko | -1.83% | -0.14% 0m02.14s | 832348 ko | TemplateCheckWf.vo | 0m01.84s | 831408 ko || +0m00.30s || 940 ko | +16.30% | +0.11% 0m02.14s | 805800 ko | ToTemplate/QuotationOf/Common/Universes/Level/Instances.vo | 0m02.11s | 806120 ko || +0m00.03s || -320 ko | +1.42% | -0.03% 0m02.10s | 452984 ko | MCList.vo | 0m01.91s | 454648 ko || +0m00.19s || -1664 ko | +9.94% | -0.36% 0m02.10s | 939524 ko | Typed/Transform.vo | 0m01.99s | 940004 ko || +0m00.11s || -480 ko | +5.52% | -0.05% 0m02.09s | 821496 ko | PCUICCasesContexts.vo | 0m02.02s | 822196 ko || +0m00.06s || -700 ko | +3.46% | -0.08% 0m02.07s | 1064500 ko | ToTemplate/All.vo | 0m01.97s | 1063376 ko || +0m00.09s || 1124 ko | +5.07% | +0.10% 0m02.07s | 774820 ko | utils/PCUICOnOne.vo | 0m01.82s | 774344 ko || +0m00.24s || 476 ko | +13.73% | +0.06% 0m02.06s | 812456 ko | CommonUtils.vo | 0m02.05s | 812336 ko || +0m00.01s || 120 ko | +0.48% | +0.01% 0m02.06s | 894472 ko | PCUICWeakeningEnvSN.vo | 0m02.00s | 896056 ko || +0m00.06s || -1584 ko | +3.00% | -0.17% 0m02.06s | 1057784 ko | ToTemplate/Template/TypingWf.vo | 0m01.97s | 1056860 ko || +0m00.09s || 924 ko | +4.56% | +0.08% 0m02.04s | 863724 ko | ToTemplate/QuotationOf/Template/Typing/TemplateDeclarationTyping/Instances.vo | 0m02.09s | 864196 ko || -0m00.04s || -472 ko | -2.39% | -0.05% 0m02.01s | 775680 ko | EnvMap.vo | 0m02.49s | 776568 ko || -0m00.48s || -888 ko | -19.27% | -0.11% 0m02.01s | 360548 ko | MiniHoTT_paths.vo | 0m02.12s | 360628 ko || -0m00.11s || -80 ko | -5.18% | -0.02% 0m02.00s | 861100 ko | ToTemplate/QuotationOf/Template/Typing/TemplateTyping/Instances.vo | 0m01.90s | 861460 ko || +0m00.10s || -360 ko | +5.26% | -0.04% 0m02.00s | 853840 ko | Typing/PCUICWeakeningTyp.vo | 0m01.84s | 853116 ko || +0m00.15s || 724 ko | +8.69% | +0.08% 0m01.99s | 825788 ko | param_original.vo | 0m01.90s | 824892 ko || +0m00.09s || 896 ko | +4.73% | +0.10% 0m01.97s | 776900 ko | Reduction.vo | 0m01.74s | 779536 ko || +0m00.23s || -2636 ko | +13.21% | -0.33% 0m01.97s | 806596 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.vo | 0m02.14s | 805556 ko || -0m00.17s || 1040 ko | -7.94% | +0.12% 0m01.96s | 818060 ko | PCUICToTemplate.vo | 0m02.02s | 819568 ko || -0m00.06s || -1508 ko | -2.97% | -0.18% 0m01.95s | 801908 ko | ToTemplate/Utils/MCOption.vo | 0m01.59s | 800856 ko || +0m00.35s || 1052 ko | +22.64% | +0.13% 0m01.94s | 895680 ko | PCUICWeakeningConfigSN.vo | 0m01.99s | 894836 ko || -0m00.05s || 844 ko | -2.51% | +0.09% 0m01.93s | 839884 ko | Conversion/PCUICClosedConv.vo | 0m02.11s | 840164 ko || -0m00.17s || -280 ko | -8.53% | -0.03% 0m01.93s | 801068 ko | ToTemplate/Utils/MCProd.vo | 0m01.80s | 798820 ko || +0m00.12s || 2248 ko | +7.22% | +0.28% 0m01.92s | 766628 ko | EAstUtils.vo | 0m01.66s | 766540 ko || +0m00.26s || 88 ko | +15.66% | +0.01% 0m01.91s | 771324 ko | AstUtils.vo | 0m02.10s | 771088 ko || -0m00.19s || 236 ko | -9.04% | +0.03% 0m01.91s | 1046324 ko | ToTemplate/Template/AstUtils.vo | 0m01.86s | 1047320 ko || +0m00.04s || -996 ko | +2.68% | -0.09% 0m01.90s | 857172 ko | TemplateToPCUIC.vo | 0m01.85s | 856128 ko || +0m00.04s || 1044 ko | +2.70% | +0.12% 0m01.89s | 827596 ko | param_binary.vo | 0m01.93s | 824020 ko || -0m00.04s || 3576 ko | -2.07% | +0.43% 0m01.87s | 935976 ko | ToTemplate/Common/BasicAst.vo | 0m01.86s | 937236 ko || +0m00.01s || -1260 ko | +0.53% | -0.13% 0m01.87s | 808224 ko | ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.vo | 0m01.99s | 806912 ko || -0m00.11s || 1312 ko | -6.03% | +0.16% 0m01.85s | 802992 ko | ToTemplate/Coq/Numbers.vo | 0m01.61s | 801304 ko || +0m00.24s || 1688 ko | +14.90% | +0.21% 0m01.85s | 827872 ko | Typed/Utils.vo | 0m01.87s | 829816 ko || -0m00.02s || -1944 ko | -1.06% | -0.23% 0m01.82s | 829288 ko | Typed/Certifying.vo | 0m01.84s | 830952 ko || -0m00.02s || -1664 ko | -1.08% | -0.20% 0m01.80s | 805532 ko | ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.vo | 0m01.77s | 806420 ko || +0m00.03s || -888 ko | +1.69% | -0.11% 0m01.79s | 1015136 ko | ToTemplate/QuotationOf/Template/Ast/Instances.vo | 0m01.80s | 1015804 ko || -0m00.01s || -668 ko | -0.55% | -0.06% 0m01.78s | 775060 ko | EAst.vo | 0m01.81s | 774280 ko || -0m00.03s || 780 ko | -1.65% | +0.10% 0m01.76s | 835984 ko | Syntax/PCUICInstDef.vo | 0m01.74s | 836472 ko || +0m00.02s || -488 ko | +1.14% | -0.05% 0m01.76s | 805564 ko | ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.vo | 0m01.83s | 805328 ko || -0m00.07s || 236 ko | -3.82% | +0.02% 0m01.75s | 816464 ko | ToTemplate/QuotationOf/Template/ReflectAst/EnvDecide/Instances.vo | 0m01.74s | 816532 ko || +0m00.01s || -68 ko | +0.57% | -0.00% 0m01.75s | 102800 ko | gen-src/typing0.cmx | 0m01.37s | 101808 ko || +0m00.37s || 992 ko | +27.73% | +0.97% 0m01.73s | 855344 ko | TemplateMonadToPCUIC.vo | 0m01.75s | 852844 ko || -0m00.02s || 2500 ko | -1.14% | +0.29% 0m01.71s | 821084 ko | Syntax/PCUICTactics.vo | 0m01.80s | 819320 ko || -0m00.09s || 1764 ko | -5.00% | +0.21% 0m01.70s | 832400 ko | PCUICGeneration.vo | 0m01.65s | 832760 ko || +0m00.05s || -360 ko | +3.03% | -0.04% 0m01.69s | 767724 ko | ECSubst.vo | 0m01.72s | 768096 ko || -0m00.03s || -372 ko | -1.74% | -0.04% 0m01.69s | 858804 ko | PCUICTemplateMonad/Core.vo | 0m01.70s | 858764 ko || -0m00.01s || 40 ko | -0.58% | +0.00% 0m01.69s | 823964 ko | param_cheap_packed.vo | 0m01.64s | 823280 ko || +0m00.05s || 684 ko | +3.04% | +0.08% 0m01.68s | 533576 ko | MCMSets.vo | 0m01.48s | 533696 ko || +0m00.19s || -120 ko | +13.51% | -0.02% 0m01.68s | 840908 ko | PCUICTemplateMonad.vo | 0m01.62s | 841660 ko || +0m00.05s || -752 ko | +3.70% | -0.08% 0m01.67s | 861788 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversionPar/Instances.vo | 0m01.63s | 861476 ko || +0m00.04s || 312 ko | +2.45% | +0.03% 0m01.66s | 837352 ko | PCUICGlobalEnv.vo | 0m01.69s | 836376 ko || -0m00.03s || 976 ko | -1.77% | +0.11% 0m01.66s | 802668 ko | ToTemplate/Coq/Lists.vo | 0m01.43s | 801872 ko || +0m00.23s || 796 ko | +16.08% | +0.09% 0m01.66s | 814952 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetExtraOrdProp/Instances.vo | 0m01.56s | 814500 ko || +0m00.09s || 452 ko | +6.41% | +0.05% 0m01.65s | 799364 ko | ToTemplate/Coq/ssr.vo | 0m01.41s | 800256 ko || +0m00.24s || -892 ko | +17.02% | -0.11% 0m01.64s | 817500 ko | EEnvMap.vo | 0m01.63s | 818800 ko || +0m00.01s || -1300 ko | +0.61% | -0.15% 0m01.64s | 826328 ko | PCUICWeakeningConfig.vo | 0m01.62s | 827336 ko || +0m00.01s || -1008 ko | +1.23% | -0.12% 0m01.63s | 813220 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetExtraOrdProp/Instances.vo | 0m01.73s | 815188 ko || -0m00.10s || -1968 ko | -5.78% | -0.24% 0m01.63s | 89764 ko | gen-src/metacoq_template_plugin.cmxs | 0m01.32s | 89836 ko || +0m00.30s || -72 ko | +23.48% | -0.08% 0m01.62s | 831348 ko | PCUICExpandLets.vo | 0m01.51s | 832060 ko || +0m00.11s || -712 ko | +7.28% | -0.08% 0m01.62s | 834716 ko | PCUICProgram.vo | 0m01.49s | 834740 ko || +0m00.13s || -24 ko | +8.72% | -0.00% 0m01.62s | 810940 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetExtraOrdProp/Instances.vo | 0m01.63s | 810504 ko || -0m00.00s || 436 ko | -0.61% | +0.05% 0m01.62s | 799068 ko | ToTemplate/Utils/MCReflect.vo | 0m01.47s | 799612 ko || +0m00.15s || -544 ko | +10.20% | -0.06% 0m01.62s | 765756 ko | utils/PCUICPrimitive.vo | 0m01.57s | 766036 ko || +0m00.05s || -280 ko | +3.18% | -0.03% 0m01.60s | 831228 ko | Syntax/PCUICRenameDef.vo | 0m01.74s | 831412 ko || -0m00.13s || -184 ko | -8.04% | -0.02% 0m01.60s | 798132 ko | ToTemplate/Common/Primitive.vo | 0m01.52s | 799156 ko || +0m00.08s || -1024 ko | +5.26% | -0.12% 0m01.58s | 814716 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSetExtraOrdProp/Instances.vo | 0m01.68s | 814024 ko || -0m00.09s || 692 ko | -5.95% | +0.08% 0m01.56s | 820584 ko | All.vo | 0m01.64s | 819396 ko || -0m00.07s || 1188 ko | -4.87% | +0.14% 0m01.55s | 799148 ko | ToTemplate/Utils/MCList.vo | 0m01.56s | 798348 ko || -0m00.01s || 800 ko | -0.64% | +0.10% 0m01.54s | 798112 ko | ToTemplate/Utils/bytestring.vo | 0m01.56s | 798592 ko || -0m00.02s || -480 ko | -1.28% | -0.06% 0m01.53s | 810988 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTermUtils/Instances.vo | 0m01.53s | 810968 ko || +0m00.00s || 20 ko | +0.00% | +0.00% 0m01.52s | 823240 ko | TemplateEnvMap.vo | 0m01.64s | 823500 ko || -0m00.11s || -260 ko | -7.31% | -0.03% 0m01.52s | 811556 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTerm/Instances.vo | 0m01.59s | 811208 ko || -0m00.07s || 348 ko | -4.40% | +0.04% 0m01.51s | 807716 ko | ToTemplate/Utils/utils.vo | 0m01.54s | 806820 ko || -0m00.03s || 896 ko | -1.94% | +0.11% 0m01.49s | 820368 ko | EExtends.vo | 0m01.51s | 821928 ko || -0m00.02s || -1560 ko | -1.32% | -0.18% 0m01.48s | 804264 ko | ToTemplate/QuotationOf/Template/ReflectAst/Instances.vo | 0m01.43s | 804068 ko || +0m00.05s || 196 ko | +3.49% | +0.02% 0m01.46s | 770792 ko | Ast.vo | 0m01.68s | 770956 ko || -0m00.21s || -164 ko | -13.09% | -0.02% 0m01.45s | 874796 ko | Typing/PCUICNamelessTyp.vo | 0m01.47s | 874812 ko || -0m00.02s || -16 ko | -1.36% | -0.00% 0m01.44s | 798808 ko | ToTemplate/Coq/Bool.vo | 0m01.58s | 799452 ko || -0m00.14s || -644 ko | -8.86% | -0.08% 0m01.43s | 801932 ko | Constants.vo | 0m01.55s | 802112 ko || -0m00.12s || -180 ko | -7.74% | -0.02% 0m01.43s | 798132 ko | ToTemplate/Utils/MCArith.vo | 0m01.30s | 797944 ko || +0m00.12s || 188 ko | +9.99% | +0.02% 0m01.41s | 817020 ko | ToTemplate/QuotationOf/Template/ReflectAst/TemplateTermDecide/Instances.vo | 0m01.35s | 816940 ko || +0m00.05s || 80 ko | +4.44% | +0.00% 0m01.40s | 868848 ko | ToTemplate/QuotationOf/Common/Kernames/Instances.vo | 0m01.43s | 867412 ko || -0m00.03s || 1436 ko | -2.09% | +0.16% 0m01.40s | 800204 ko | ToTemplate/Utils/MCUtils.vo | 0m01.39s | 799832 ko || +0m00.01s || 372 ko | +0.71% | +0.04% 0m01.40s | 822712 ko | standard_model.vo | 0m01.43s | 822520 ko || -0m00.03s || 192 ko | -2.09% | +0.02% 0m01.39s | 850328 ko | ToTemplate/QuotationOf/Common/Universes/Instances.vo | 0m01.35s | 847584 ko || +0m00.03s || 2744 ko | +2.96% | +0.32% 0m01.39s | 859096 ko | ToTemplate/QuotationOf/Template/Typing/Instances.vo | 0m01.40s | 860304 ko || -0m00.01s || -1208 ko | -0.71% | -0.14% 0m01.39s | 433540 ko | canonicaltries/CanonicalTries.vo | 0m01.12s | 433428 ko || +0m00.26s || 112 ko | +24.10% | +0.02% 0m01.39s | 769428 ko | utils/PCUICSize.vo | 0m01.05s | 770352 ko || +0m00.33s || -924 ko | +32.38% | -0.11% 0m01.38s | 833748 ko | PCUICGuardCondition.vo | 0m01.34s | 832652 ko || +0m00.03s || 1096 ko | +2.98% | +0.13% 0m01.38s | 799788 ko | ToTemplate/Utils/ReflectEq.vo | 0m01.53s | 798212 ko || -0m00.15s || 1576 ko | -9.80% | +0.19% 0m01.34s | 770404 ko | EGlobalEnv.vo | 0m01.32s | 770392 ko || +0m00.02s || 12 ko | +1.51% | +0.00% 0m01.34s | 799112 ko | ToTemplate/Coq/Strings.vo | 0m01.29s | 799124 ko || +0m00.05s || -12 ko | +3.87% | -0.00% 0m01.34s | 817896 ko | sigma.vo | 0m01.46s | 817992 ko || -0m00.11s || -96 ko | -8.21% | -0.01% 0m01.34s | 809816 ko | utils/PCUICPretty.vo | 0m01.24s | 811240 ko || +0m00.10s || -1424 ko | +8.06% | -0.17% 0m01.33s | 798924 ko | ToTemplate/Common/config.vo | 0m01.44s | 798768 ko || -0m00.10s || 156 ko | -7.63% | +0.01% 0m01.32s | 777256 ko | ESpineView.vo | 0m01.42s | 775508 ko || -0m00.09s || 1748 ko | -7.04% | +0.22% 0m01.31s | 829424 ko | Syntax/PCUICNamelessDef.vo | 0m01.33s | 830048 ko || -0m00.02s || -624 ko | -1.50% | -0.07% 0m01.29s | 843928 ko | EProgram.vo | 0m01.43s | 844976 ko || -0m00.13s || -1048 ko | -9.79% | -0.12% 0m01.27s | 809544 ko | ToTemplate/Coq/Floats.vo | 0m01.36s | 809740 ko || -0m00.09s || -196 ko | -6.61% | -0.02% 0m01.26s | 809928 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapExtraFact/Instances.vo | 0m01.34s | 810692 ko || -0m00.08s || -764 ko | -5.97% | -0.09% 0m01.24s | 819324 ko | TemplateProgram.vo | 0m01.24s | 819744 ko || +0m00.00s || -420 ko | +0.00% | -0.05% 0m01.21s | 766624 ko | Pretty.vo | 0m01.19s | 766580 ko || +0m00.02s || 44 ko | +1.68% | +0.00% 0m01.20s | 764756 ko | TemplateMonad/Core.vo | 0m01.29s | 765168 ko || -0m00.09s || -412 ko | -6.97% | -0.05% 0m01.17s | 763876 ko | TemplateMonad/Extractable.vo | 0m01.13s | 763624 ko || +0m00.04s || 252 ko | +3.53% | +0.03% 0m01.13s | 762384 ko | MonadAst.vo | 0m01.15s | 762548 ko || -0m00.02s || -164 ko | -1.73% | -0.02% 0m01.12s | 769344 ko | Typed/ExAst.vo | 0m01.13s | 770056 ko || -0m00.00s || -712 ko | -0.88% | -0.09% 0m01.11s | 775004 ko | Normal.vo | 0m01.11s | 774644 ko || +0m00.00s || 360 ko | +0.00% | +0.04% 0m01.10s | 772256 ko | EPretty.vo | 0m01.20s | 770688 ko || -0m00.09s || 1568 ko | -8.33% | +0.20% 0m01.10s | 761084 ko | TemplateMonad/Common.vo | 0m00.97s | 762364 ko || +0m00.13s || -1280 ko | +13.40% | -0.16% 0m01.09s | 763304 ko | Induction.vo | 0m01.34s | 763428 ko || -0m00.25s || -124 ko | -18.65% | -0.01% 0m01.08s | 752576 ko | TemplateMonad.vo | 0m01.23s | 753836 ko || -0m00.14s || -1260 ko | -12.19% | -0.16% 0m01.03s | 767512 ko | PCUICMonadAst.vo | 0m01.04s | 766860 ko || -0m00.01s || 652 ko | -0.96% | +0.08% 0m00.99s | 217328 ko | gen-src/metacoq_template_plugin.cmx | 0m00.93s | 217300 ko || +0m00.05s || 28 ko | +6.45% | +0.01% 0m00.94s | 53112 ko | gen-src/byte.cmx | 0m00.75s | 53164 ko || +0m00.18s || -52 ko | +25.33% | -0.09% 0m00.92s | 678120 ko | MonadBasicAst.vo | 0m00.83s | 677604 ko || +0m00.09s || 516 ko | +10.84% | +0.07% 0m00.87s | 99152 ko | gen-src/environmentTyping.cmx | 0m00.71s | 97500 ko || +0m00.16s || 1652 ko | +22.53% | +1.69% 0m00.83s | 131532 ko | gen-src/fMapAVL.cmi | 0m00.66s | 131284 ko || +0m00.16s || 248 ko | +25.75% | +0.18% 0m00.71s | 92312 ko | gen-src/fMapAVL.cmx | 0m00.51s | 92304 ko || +0m00.19s || 8 ko | +39.21% | +0.00% 0m00.67s | 73048 ko | gen-src/byte0.cmx | 0m00.47s | 72844 ko || +0m00.20s || 204 ko | +42.55% | +0.28% 0m00.64s | 422780 ko | config.vo | 0m00.64s | 423208 ko || +0m00.00s || -428 ko | +0.00% | -0.10% 0m00.64s | 55492 ko | gen-src/all_Forall.cmx | 0m00.50s | 55460 ko || +0m00.14s || 32 ko | +28.00% | +0.05% 0m00.55s | 441128 ko | monad_utils.vo | 0m00.40s | 441532 ko || +0m00.15s || -404 ko | +37.50% | -0.09% 0m00.55s | 510188 ko | utils/PCUICUtils.vo | 0m00.56s | 509772 ko || -0m00.01s || 416 ko | -1.78% | +0.08% 0m00.53s | 98196 ko | gen-src/kernames.cmx | 0m00.44s | 98860 ko || +0m00.09s || -664 ko | +20.45% | -0.67% 0m00.49s | 85360 ko | gen-src/environmentTyping.cmi | 0m00.35s | 84076 ko || +0m00.14s || 1284 ko | +40.00% | +1.52% 0m00.45s | 502992 ko | MCUtils.vo | 0m00.29s | 502540 ko || +0m00.16s || 452 ko | +55.17% | +0.08% 0m00.45s | 424300 ko | Transform.vo | 0m00.42s | 424744 ko || +0m00.03s || -444 ko | +7.14% | -0.10% 0m00.44s | 72656 ko | wGraph.cmx | 0m00.44s | 72664 ko || +0m00.00s || -8 ko | +0.00% | -0.01% 0m00.42s | 81004 ko | pCUICSafeChecker.cmx | 0m00.46s | 81072 ko || -0m00.04s || -68 ko | -8.69% | -0.08% 0m00.41s | 87512 ko | uGraph0.cmx | 0m00.39s | 88180 ko || +0m00.01s || -668 ko | +5.12% | -0.75% 0m00.40s | 433392 ko | MCPred.vo | 0m00.35s | 434140 ko || +0m00.05s || -748 ko | +14.28% | -0.17% 0m00.40s | 489404 ko | bytestring.vo | 0m00.42s | 488088 ko || -0m00.01s || 1316 ko | -4.76% | +0.26% 0m00.40s | 494060 ko | utils.vo | 0m00.34s | 492788 ko || +0m00.06s || 1272 ko | +17.64% | +0.25% 0m00.38s | 78976 ko | gen-src/universes0.cmx | 0m00.35s | 78828 ko || +0m00.03s || 148 ko | +8.57% | +0.18% 0m00.37s | 434100 ko | MCOption.vo | 0m00.42s | 433376 ko || -0m00.04s || 724 ko | -11.90% | +0.16% 0m00.37s | 60652 ko | gen-src/ast0.cmx | 0m00.28s | 59524 ko || +0m00.08s || 1128 ko | +32.14% | +1.89% 0m00.36s | 79136 ko | pCUICSafeConversion.cmx | 0m00.36s | 78428 ko || +0m00.00s || 708 ko | +0.00% | +0.90% 0m00.35s | 51680 ko | gen-src/environment.cmx | 0m00.24s | 51596 ko || +0m00.10s || 84 ko | +45.83% | +0.16% 0m00.35s | 78552 ko | gen-src/kernames.cmi | 0m00.29s | 78504 ko || +0m00.06s || 48 ko | +20.68% | +0.06% 0m00.35s | 42604 ko | gen-src/termEquality.cmx | 0m00.25s | 42784 ko || +0m00.09s || -180 ko | +39.99% | -0.42% 0m00.33s | 387988 ko | canonicaltries/String2pos.vo | 0m00.25s | 384984 ko || +0m00.08s || 3004 ko | +32.00% | +0.78% 0m00.33s | 60784 ko | gen-src/mCFSets.cmi | 0m00.23s | 60664 ko || +0m00.10s || 120 ko | +43.47% …

JasonGross mentioned this issue Apr 8, 2023

[quotation] Fuse Template Monad loops #909

Merged

JasonGross added a commit to JasonGross/metacoq that referenced this issue Apr 8, 2023

Optimize tmBind

1e0336b

Fixes MetaCoq#441

JasonGross linked a pull request Apr 8, 2023 that will close this issue

Optimize tmBind #916

Draft

JasonGross added a commit to JasonGross/metacoq that referenced this issue Apr 9, 2023

Add an optimized version of tmBind

8dae2e2

This is partial work towards MetaCoq#441.

JasonGross added a commit to JasonGross/metacoq that referenced this issue Apr 9, 2023

Add an optimized version of tmBind

4e22acb

This is partial work towards MetaCoq#441.

JasonGross mentioned this issue Apr 9, 2023

Add an optimized version of tmBind #926

Merged

JasonGross added a commit to JasonGross/metacoq that referenced this issue Apr 9, 2023

Optimize tmBind

cdac0b6

Fixes MetaCoq#441

JasonGross added a commit to JasonGross/metacoq that referenced this issue Apr 9, 2023

Optimize tmBind

d9fc147

Fixes MetaCoq#441

JasonGross added a commit to JasonGross/metacoq that referenced this issue Apr 10, 2023

Optimize tmBind

83d7b84

Fixes MetaCoq#441

JasonGross added a commit to JasonGross/metacoq that referenced this issue Apr 11, 2023

Optimize tmBind

5f99503

Fixes MetaCoq#441

JasonGross added a commit to JasonGross/metacoq that referenced this issue Apr 11, 2023

Optimize tmBind

4c5d352

Fixes MetaCoq#441

JasonGross added a commit to JasonGross/metacoq that referenced this issue Apr 12, 2023

Optimize tmBind

9188e6c

Fixes MetaCoq#441 <details><summary>Timing Diff</summary> ``` No timing data ``` </details>

JasonGross added a commit to JasonGross/metacoq that referenced this issue Apr 12, 2023

Optimize tmBind

b6debad

Fixes MetaCoq#441

JasonGross added a commit to JasonGross/metacoq that referenced this issue Apr 12, 2023

Optimize tmBind

8a7c37f

Fixes MetaCoq#441

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Recursive TemplateMonad programs are slow to run #441

Recursive TemplateMonad programs are slow to run #441

john-ml commented Jul 16, 2020 •

edited

gmalecha commented Aug 2, 2020

john-ml commented Aug 2, 2020

Recursive TemplateMonad programs are slow to run #441

Recursive TemplateMonad programs are slow to run #441

Comments

john-ml commented Jul 16, 2020 • edited

gmalecha commented Aug 2, 2020

john-ml commented Aug 2, 2020

john-ml commented Jul 16, 2020 •

edited