diff options
| author | Jason Gross | 2018-11-19 16:58:43 -0500 |
|---|---|---|
| committer | Jason Gross | 2018-11-28 15:01:17 -0500 |
| commit | 732b3550ada0598f56aeed09527d446a1013e353 (patch) | |
| tree | e7ad054be260bbd66bf679ee19855c97d59ad367 /plugins/extraction/ExtrHaskellString.v | |
| parent | e30e864d61431a0145853fcf90b5f16b781f4a46 (diff) | |
Speed up Byte
We could move another ~ 1s from Init.Byte to Strings.Byte by moving
`of_bits_to_bits` and `to_bits_of_bits`, but I figured it's probably not
worth it.
After | File Name | Before || Change | % Change
----------------------------------------------------------------------------------
1m16.75s | Total | 1m21.45s || -0m04.70s | -5.77%
----------------------------------------------------------------------------------
0m08.95s | Strings/Byte | 0m12.41s || -0m03.46s | -27.88%
0m07.24s | Byte | 0m08.76s || -0m01.51s | -17.35%
0m06.37s | plugins/setoid_ring/Ring_polynom | 0m06.24s || +0m00.12s | +2.08%
0m03.14s | Numbers/Integer/Abstract/ZBits | 0m03.20s || -0m00.06s | -1.87%
0m02.44s | ZArith/BinInt | 0m02.44s || +0m00.00s | +0.00%
0m02.24s | Numbers/Natural/Abstract/NBits | 0m02.20s || +0m00.04s | +1.81%
0m01.97s | Lists/List | 0m01.93s || +0m00.04s | +2.07%
0m01.85s | Numbers/NatInt/NZLog | 0m01.82s || +0m00.03s | +1.64%
0m01.78s | PArith/BinPos | 0m01.78s || +0m00.00s | +0.00%
0m01.74s | plugins/setoid_ring/InitialRing | 0m01.63s || +0m00.11s | +6.74%
0m01.73s | Strings/Ascii | 0m01.58s || +0m00.14s | +9.49%
0m01.39s | NArith/BinNat | 0m01.34s || +0m00.04s | +3.73%
0m01.32s | Numbers/NatInt/NZPow | 0m01.24s || +0m00.08s | +6.45%
0m01.22s | Numbers/NatInt/NZSqrt | 0m01.15s || +0m00.07s | +6.08%
0m01.11s | Arith/PeanoNat | 0m01.16s || -0m00.04s | -4.31%
0m01.10s | Numbers/Integer/Abstract/ZDivTrunc | 0m01.11s || -0m00.01s | -0.90%
0m01.02s | Specif | 0m01.04s || -0m00.02s | -1.92%
0m00.96s | Numbers/NatInt/NZMulOrder | 0m00.84s || +0m00.12s | +14.28%
0m00.95s | Numbers/Integer/Abstract/ZDivFloor | 0m00.97s || -0m00.02s | -2.06%
0m00.85s | plugins/setoid_ring/Ring_theory | 0m00.86s || -0m00.01s | -1.16%
0m00.82s | Structures/GenericMinMax | 0m00.85s || -0m00.03s | -3.52%
0m00.72s | Numbers/Integer/Abstract/ZLcm | 0m00.82s || -0m00.09s | -12.19%
0m00.69s | Numbers/NatInt/NZParity | 0m00.69s || +0m00.00s | +0.00%
0m00.68s | Numbers/NatInt/NZDiv | 0m00.71s || -0m00.02s | -4.22%
0m00.68s | Strings/String | 0m00.65s || +0m00.03s | +4.61%
0m00.64s | Numbers/Integer/Abstract/ZSgnAbs | 0m00.64s || +0m00.00s | +0.00%
0m00.64s | ZArith/Zeven | 0m00.48s || +0m00.16s | +33.33%
0m00.63s | ZArith/Zorder | 0m00.61s || +0m00.02s | +3.27%
0m00.57s | Numbers/Integer/Abstract/ZMulOrder | 0m00.67s || -0m00.10s | -14.92%
0m00.56s | Classes/Morphisms | 0m00.58s || -0m00.01s | -3.44%
0m00.55s | Numbers/NatInt/NZOrder | 0m00.51s || +0m00.04s | +7.84%
0m00.48s | ZArith/BinIntDef | 0m00.48s || +0m00.00s | +0.00%
0m00.46s | Classes/CMorphisms | 0m00.48s || -0m00.01s | -4.16%
0m00.46s | Numbers/Integer/Abstract/ZGcd | 0m00.46s || +0m00.00s | +0.00%
0m00.46s | Numbers/Natural/Abstract/NSub | 0m00.48s || -0m00.01s | -4.16%
0m00.45s | Logic | 0m00.44s || +0m00.01s | +2.27%
0m00.45s | Numbers/Natural/Abstract/NGcd | 0m00.48s || -0m00.02s | -6.24%
0m00.42s | Numbers/Natural/Abstract/NLcm | 0m00.40s || +0m00.01s | +4.99%
0m00.42s | Structures/OrdersFacts | 0m00.48s || -0m00.06s | -12.50%
0m00.41s | ZArith/Zbool | 0m00.38s || +0m00.02s | +7.89%
0m00.38s | Numbers/Integer/Abstract/ZPow | 0m00.34s || +0m00.03s | +11.76%
0m00.36s | Bool/Bool | 0m00.36s || +0m00.00s | +0.00%
0m00.36s | Numbers/NatInt/NZGcd | 0m00.35s || +0m00.01s | +2.85%
0m00.36s | ZArith/ZArith_dec | 0m00.38s || -0m00.02s | -5.26%
0m00.34s | Numbers/Integer/Abstract/ZAdd | 0m00.33s || +0m00.01s | +3.03%
0m00.34s | PArith/Pnat | 0m00.31s || +0m00.03s | +9.67%
0m00.32s | Numbers/Natural/Abstract/NOrder | 0m00.32s || +0m00.00s | +0.00%
0m00.32s | PArith/BinPosDef | 0m00.31s || +0m00.01s | +3.22%
0m00.32s | ZArith/Zcompare | 0m00.28s || +0m00.03s | +14.28%
0m00.30s | Classes/RelationClasses | 0m00.29s || +0m00.01s | +3.44%
0m00.30s | NArith/Nnat | 0m00.30s || +0m00.00s | +0.00%
0m00.29s | Numbers/Natural/Abstract/NAxioms | 0m00.26s || +0m00.02s | +11.53%
0m00.28s | Numbers/Integer/Abstract/ZAddOrder | 0m00.28s || +0m00.00s | +0.00%
0m00.28s | Structures/Orders | 0m00.30s || -0m00.01s | -6.66%
0m00.27s | Numbers/Integer/Abstract/ZAxioms | 0m00.23s || +0m00.04s | +17.39%
0m00.27s | Numbers/NatInt/NZAxioms | 0m00.26s || +0m00.01s | +3.84%
0m00.26s | Numbers/Integer/Abstract/ZMaxMin | 0m00.25s || +0m00.01s | +4.00%
0m00.26s | Numbers/NatInt/NZAdd | 0m00.28s || -0m00.02s | -7.14%
0m00.26s | Numbers/Natural/Abstract/NMaxMin | 0m00.24s || +0m00.02s | +8.33%
0m00.26s | Numbers/Natural/Abstract/NParity | 0m00.31s || -0m00.04s | -16.12%
0m00.26s | plugins/setoid_ring/ArithRing | 0m00.22s || +0m00.04s | +18.18%
0m00.26s | plugins/setoid_ring/Ring_tac | 0m00.24s || +0m00.02s | +8.33%
0m00.25s | Logic/Decidable | 0m00.26s || -0m00.01s | -3.84%
0m00.25s | Structures/OrdersTac | 0m00.25s || +0m00.00s | +0.00%
0m00.24s | Classes/Equivalence | 0m00.25s || -0m00.01s | -4.00%
0m00.24s | Datatypes | 0m00.27s || -0m00.03s | -11.11%
0m00.24s | Numbers/NatInt/NZMul | 0m00.25s || -0m00.01s | -4.00%
0m00.24s | plugins/setoid_ring/Ring | 0m00.20s || +0m00.03s | +19.99%
0m00.23s | Numbers/NatInt/NZAddOrder | 0m00.33s || -0m00.10s | -30.30%
0m00.23s | Numbers/Natural/Abstract/NAdd | 0m00.17s || +0m00.06s | +35.29%
0m00.22s | Arith/Compare_dec | 0m00.22s || +0m00.00s | +0.00%
0m00.22s | Classes/CRelationClasses | 0m00.25s || -0m00.03s | -12.00%
0m00.22s | Logic/EqdepFacts | 0m00.19s || +0m00.03s | +15.78%
0m00.22s | NArith/BinNatDef | 0m00.25s || -0m00.03s | -12.00%
0m00.22s | plugins/setoid_ring/Ring_base | 0m00.23s || -0m00.01s | -4.34%
0m00.21s | Arith/Arith | 0m00.19s || +0m00.01s | +10.52%
0m00.21s | Numbers/Natural/Abstract/NDiv | 0m00.19s || +0m00.01s | +10.52%
0m00.20s | Numbers/Integer/Abstract/ZProperties | 0m00.23s || -0m00.03s | -13.04%
0m00.20s | Relations/Relation_Operators | 0m00.17s || +0m00.03s | +17.64%
0m00.19s | Arith/Between | 0m00.22s || -0m00.03s | -13.63%
0m00.18s | Arith/Wf_nat | 0m00.24s || -0m00.06s | -25.00%
0m00.17s | Arith/Plus | 0m00.16s || +0m00.01s | +6.25%
0m00.17s | Nat | 0m00.18s || -0m00.00s | -5.55%
0m00.17s | Numbers/Natural/Abstract/NProperties | 0m00.22s || -0m00.04s | -22.72%
0m00.17s | Relations/Relation_Definitions | 0m00.08s || +0m00.09s | +112.50%
0m00.16s | Numbers/Integer/Abstract/ZLt | 0m00.16s || +0m00.00s | +0.00%
0m00.16s | Numbers/Natural/Abstract/NBase | 0m00.19s || -0m00.03s | -15.78%
0m00.16s | Numbers/Natural/Abstract/NPow | 0m00.15s || +0m00.01s | +6.66%
0m00.15s | Classes/Morphisms_Prop | 0m00.18s || -0m00.03s | -16.66%
0m00.14s | Arith/Mult | 0m00.12s || +0m00.02s | +16.66%
0m00.14s | Arith/Peano_dec | 0m00.16s || -0m00.01s | -12.49%
0m00.14s | Numbers/NatInt/NZBase | 0m00.13s || +0m00.01s | +7.69%
0m00.14s | Numbers/Natural/Abstract/NMulOrder | 0m00.13s || +0m00.01s | +7.69%
0m00.14s | Relations/Operators_Properties | 0m00.13s || +0m00.01s | +7.69%
0m00.14s | plugins/setoid_ring/BinList | 0m00.16s || -0m00.01s | -12.49%
0m00.13s | Arith/EqNat | 0m00.18s || -0m00.04s | -27.77%
0m00.13s | Structures/Equalities | 0m00.17s || -0m00.04s | -23.52%
0m00.12s | Arith/Lt | 0m00.11s || +0m00.00s | +9.09%
0m00.12s | Arith/Minus | 0m00.13s || -0m00.01s | -7.69%
0m00.12s | Decimal | 0m00.16s || -0m00.04s | -25.00%
0m00.12s | Numbers/Integer/Abstract/ZBase | 0m00.09s || +0m00.03s | +33.33%
0m00.12s | Numbers/Integer/Abstract/ZMul | 0m00.12s || +0m00.00s | +0.00%
0m00.12s | Numbers/Integer/Abstract/ZParity | 0m00.11s || +0m00.00s | +9.09%
0m00.12s | Numbers/Natural/Abstract/NAddOrder | 0m00.12s || +0m00.00s | +0.00%
0m00.11s | Arith/Factorial | 0m00.11s || +0m00.00s | +0.00%
0m00.11s | Lists/ListTactics | 0m00.13s || -0m00.02s | -15.38%
0m00.11s | Logic/Eqdep_dec | 0m00.12s || -0m00.00s | -8.33%
0m00.11s | Numbers/Natural/Abstract/NLog | 0m00.10s || +0m00.00s | +9.99%
0m00.11s | Peano | 0m00.10s || +0m00.00s | +9.99%
0m00.11s | Program/Basics | 0m00.07s || +0m00.03s | +57.14%
0m00.10s | Arith/Gt | 0m00.13s || -0m00.03s | -23.07%
0m00.10s | Bool/Sumbool | 0m00.10s || +0m00.00s | +0.00%
0m00.10s | Numbers/Natural/Abstract/NSqrt | 0m00.12s || -0m00.01s | -16.66%
0m00.10s | Wf | 0m00.11s || -0m00.00s | -9.09%
0m00.09s | Arith/Arith_base | 0m00.09s || +0m00.00s | +0.00%
0m00.09s | Logic_Type | 0m00.08s || +0m00.00s | +12.49%
0m00.08s | Arith/Le | 0m00.11s || -0m00.03s | -27.27%
0m00.08s | Numbers/BinNums | 0m00.06s || +0m00.02s | +33.33%
0m00.08s | Numbers/NatInt/NZBits | 0m00.12s || -0m00.03s | -33.33%
0m00.08s | Numbers/NatInt/NZProperties | 0m00.09s || -0m00.00s | -11.11%
0m00.08s | Program/Tactics | 0m00.08s || +0m00.00s | +0.00%
0m00.07s | Tactics | 0m00.10s || -0m00.03s | -30.00%
0m00.06s | Classes/SetoidTactics | 0m00.06s || +0m00.00s | +0.00%
0m00.06s | Numbers/NumPrelude | 0m00.06s || +0m00.00s | +0.00%
0m00.05s | Classes/Init | 0m00.04s || +0m00.01s | +25.00%
0m00.05s | Prelude | 0m00.09s || -0m00.03s | -44.44%
0m00.05s | Setoids/Setoid | 0m00.08s || -0m00.03s | -37.50%
0m00.04s | Relations/Relations | 0m00.04s || +0m00.00s | +0.00%
0m00.04s | Tauto | 0m00.09s || -0m00.05s | -55.55%
0m00.02s | Notations | 0m00.04s || -0m00.02s | -50.00%
Diffstat (limited to 'plugins/extraction/ExtrHaskellString.v')
0 files changed, 0 insertions, 0 deletions