Skip to content

Instantly share code, notes, and snippets.

@jarlg

jarlg/time-of-build-both.log

Last active June 21, 2021 18:44
Show Gist options
  • Save jarlg/5e75f9195ee9379f84fbb38f55d47653 to your computer and use it in GitHub Desktop.
Save jarlg/5e75f9195ee9379f84fbb38f55d47653 to your computer and use it in GitHub Desktop.
Download ZIP
Typeclasses Transparent Commutative vs Hint Unfold
Raw
time-of-build-both.log
After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem)
----------------------------------------------------------------------------------------------------------------------------------------------------
3m00.69s | 528412 ko | Total Time / Peak Mem | 3m05.47s | 523492 ko || -0m04.78s || 4920 ko | -2.58% | +0.93%
----------------------------------------------------------------------------------------------------------------------------------------------------
0m24.78s | 445196 ko | Classes/implementations/natpair_integers.vo | 0m28.40s | 454156 ko || -0m03.61s || -8960 ko | -12.74% | -1.97%
0m06.87s | 399332 ko | Algebra/Groups/FreeProduct.vo | 0m08.81s | 398664 ko || -0m01.94s || 668 ko | -22.02% | +0.16%
0m04.17s | 381368 ko | Algebra/Rings/QuotientRing.vo | 0m03.09s | 378568 ko || +0m01.08s || 2800 ko | +34.95% | +0.73%
0m11.02s | 528412 ko | Homotopy/HomotopyGroup.vo | 0m10.67s | 523492 ko || +0m00.34s || 4920 ko | +3.28% | +0.93%
0m06.80s | 362552 ko | Sets/Hartogs.vo | 0m06.93s | 363032 ko || -0m00.12s || -480 ko | -1.87% | -0.13%
0m06.57s | 385980 ko | Analysis/Locator.vo | 0m06.56s | 386436 ko || +0m00.01s || -456 ko | +0.15% | -0.11%
0m05.18s | 386588 ko | Classes/theory/premetric.vo | 0m05.17s | 386756 ko || +0m00.00s || -168 ko | +0.19% | -0.04%
0m04.54s | 477800 ko | Homotopy/CayleyDickson.vo | 0m03.64s | 477616 ko || +0m00.89s || 184 ko | +24.72% | +0.03%
0m04.28s | 378720 ko | Classes/theory/rationals.vo | 0m04.17s | 377888 ko || +0m00.11s || 832 ko | +2.63% | +0.22%
0m03.64s | 357224 ko | Sets/Ordinals.vo | 0m02.89s | 356224 ko || +0m00.75s || 1000 ko | +25.95% | +0.28%
0m03.11s | 353048 ko | Classes/implementations/field_of_fractions.vo | 0m03.46s | 353200 ko || -0m00.35s || -152 ko | -10.11% | -0.04%
0m03.09s | 373296 ko | Algebra/Rings/CRing.vo | 0m03.10s | 373560 ko || -0m00.01s || -264 ko | -0.32% | -0.07%
0m03.00s | 389816 ko | Algebra/ooGroup.vo | 0m02.90s | 389856 ko || +0m00.10s || -40 ko | +3.44% | -0.01%
0m02.51s | 394252 ko | Homotopy/ClassifyingSpace.vo | 0m02.62s | 394796 ko || -0m00.11s || -544 ko | -4.19% | -0.13%
0m02.49s | 354896 ko | Algebra/Groups/FreeGroup/ListQuotient.vo | 0m02.69s | 353924 ko || -0m00.19s || 972 ko | -7.43% | +0.27%
0m02.47s | 376080 ko | Algebra/AbGroups/Abelianization.vo | 0m01.76s | 375676 ko || +0m00.71s || 404 ko | +40.34% | +0.10%
0m02.42s | 361232 ko | Classes/orders/semirings.vo | 0m02.07s | 360336 ko || +0m00.35s || 896 ko | +16.90% | +0.24%
0m02.40s | 351856 ko | Algebra/Groups/Subgroup.vo | 0m02.56s | 351436 ko || -0m00.16s || 420 ko | -6.25% | +0.11%
0m02.25s | 474436 ko | contrib/HoTTBookExercises.vo | 0m02.36s | 474552 ko || -0m00.10s || -116 ko | -4.66% | -0.02%
0m02.20s | 372228 ko | Algebra/Rings/Z.vo | 0m02.25s | 372384 ko || -0m00.04s || -156 ko | -2.22% | -0.04%
0m02.17s | 349108 ko | Spaces/Card.vo | 0m02.45s | 348952 ko || -0m00.28s || 156 ko | -11.42% | +0.04%
0m02.08s | 367644 ko | Algebra/Groups/GroupCoeq.vo | 0m01.44s | 366872 ko || +0m00.64s || 772 ko | +44.44% | +0.21%
0m02.08s | 357036 ko | Classes/theory/int_abs.vo | 0m01.57s | 356512 ko || +0m00.51s || 524 ko | +32.48% | +0.14%
0m02.06s | 356260 ko | Algebra/Groups/QuotientGroup.vo | 0m02.05s | 356384 ko || +0m00.01s || -124 ko | +0.48% | -0.03%
0m02.03s | 348920 ko | Classes/interfaces/abstract_algebra.vo | 0m02.11s | 348544 ko || -0m00.08s || 376 ko | -3.79% | +0.10%
0m01.96s | 356124 ko | Classes/interfaces/cauchy.vo | 0m02.08s | 355820 ko || -0m00.12s || 304 ko | -5.76% | +0.08%
0m01.88s | 367824 ko | Algebra/AbGroups/AbelianGroup.vo | 0m02.20s | 367756 ko || -0m00.32s || 68 ko | -14.54% | +0.01%
0m01.82s | 349580 ko | Classes/orders/nat_int.vo | 0m01.73s | 349740 ko || +0m00.09s || -160 ko | +5.20% | -0.04%
0m01.75s | 346692 ko | Classes/theory/fields.vo | 0m01.72s | 347732 ko || +0m00.03s || -1040 ko | +1.74% | -0.29%
0m01.68s | 349952 ko | Algebra/Groups/Group.vo | 0m02.26s | 351684 ko || -0m00.57s || -1732 ko | -25.66% | -0.49%
0m01.53s | 356320 ko | Classes/implementations/binary_naturals.vo | 0m01.42s | 356000 ko || +0m00.11s || 320 ko | +7.74% | +0.08%
0m01.47s | 368584 ko | Algebra/AbGroups/AbPushout.vo | 0m02.23s | 368448 ko || -0m00.76s || 136 ko | -34.08% | +0.03%
0m01.46s | 368576 ko | Algebra/AbGroups/AbExt.vo | 0m01.58s | 368508 ko || -0m00.12s || 68 ko | -7.59% | +0.01%
0m01.41s | 349116 ko | Algebra/Groups/GrpPullback.vo | 0m00.89s | 348920 ko || +0m00.51s || 196 ko | +58.42% | +0.05%
0m01.40s | 350684 ko | Classes/orders/rings.vo | 0m01.70s | 350652 ko || -0m00.30s || 32 ko | -17.64% | +0.00%
0m01.38s | 365976 ko | Homotopy/HSpaceS1.vo | 0m01.37s | 366028 ko || +0m00.00s || -52 ko | +0.72% | -0.01%
0m01.37s | 353876 ko | Classes/orders/lattices.vo | 0m01.48s | 354200 ko || -0m00.10s || -324 ko | -7.43% | -0.09%
0m01.36s | 353612 ko | Classes/theory/ua_third_isomorphism.vo | 0m01.96s | 354920 ko || -0m00.59s || -1308 ko | -30.61% | -0.36%
0m01.34s | 361620 ko | Algebra/Groups/Presentation.vo | 0m00.92s | 362856 ko || +0m00.42s || -1236 ko | +45.65% | -0.34%
0m01.28s | 382124 ko | Homotopy/WhiteheadsPrinciple.vo | 0m01.15s | 382480 ko || +0m00.13s || -356 ko | +11.30% | -0.09%
0m01.27s | 345684 ko | Classes/theory/dec_fields.vo | 0m01.23s | 345432 ko || +0m00.04s || 252 ko | +3.25% | +0.07%
0m01.23s | 351844 ko | Classes/theory/ua_second_isomorphism.vo | 0m01.10s | 351848 ko || +0m00.12s || -4 ko | +11.81% | -0.00%
0m01.22s | 360000 ko | Classes/theory/integers.vo | 0m01.04s | 360004 ko || +0m00.17s || -4 ko | +17.30% | -0.00%
0m01.15s | 346480 ko | Classes/theory/rings.vo | 0m01.19s | 346236 ko || -0m00.04s || 244 ko | -3.36% | +0.07%
0m01.13s | 346348 ko | Sets/GCHtoAC.vo | 0m01.19s | 346320 ko || -0m00.06s || 28 ko | -5.04% | +0.00%
0m01.11s | 354544 ko | Classes/implementations/peano_naturals.vo | 0m01.39s | 354384 ko || -0m00.27s || 160 ko | -20.14% | +0.04%
0m01.11s | 349772 ko | Classes/orders/orders.vo | 0m01.41s | 350048 ko || -0m00.29s || -276 ko | -21.27% | -0.07%
0m01.06s | 355296 ko | Classes/orders/integers.vo | 0m01.04s | 355344 ko || +0m00.02s || -48 ko | +1.92% | -0.01%
0m01.05s | 360804 ko | Algebra/Groups/ShortExactSequence.vo | 0m01.08s | 360672 ko || -0m00.03s || 132 ko | -2.77% | +0.03%
0m01.04s | 342420 ko | Classes/implementations/hprop_lattice.vo | 0m01.01s | 342428 ko || +0m00.03s || -8 ko | +2.97% | -0.00%
0m00.99s | 392692 ko | Homotopy/EMSpace.vo | 0m01.51s | 392716 ko || -0m00.52s || -24 ko | -34.43% | -0.00%
0m00.93s | 345256 ko | Classes/tactics/ring_pol.vo | 0m00.97s | 345216 ko || -0m00.03s || 40 ko | -4.12% | +0.01%
0m00.90s | 350632 ko | Classes/theory/naturals.vo | 0m01.06s | 350528 ko || -0m00.16s || 104 ko | -15.09% | +0.02%
0m00.89s | 349468 ko | Classes/orders/dec_fields.vo | 0m00.61s | 349476 ko || +0m00.28s || -8 ko | +45.90% | -0.00%
0m00.89s | 348340 ko | Classes/theory/ua_quotient_algebra.vo | 0m00.77s | 348184 ko || +0m00.12s || 156 ko | +15.58% | +0.04%
0m00.82s | 510520 ko | contrib/HoTTBook.vo | 0m00.85s | 510576 ko || -0m00.03s || -56 ko | -3.52% | -0.01%
0m00.81s | 344760 ko | Classes/isomorphisms/rings.vo | 0m00.90s | 344808 ko || -0m00.08s || -48 ko | -9.99% | -0.01%
0m00.81s | 473836 ko | Tests.vo | 0m00.78s | 473900 ko || +0m00.03s || -64 ko | +3.84% | -0.01%
0m00.80s | 345308 ko | Algebra/Groups/Kernel.vo | 0m00.52s | 345436 ko || +0m00.28s || -128 ko | +53.84% | -0.03%
0m00.79s | 341268 ko | Classes/implementations/pointwise.vo | 0m00.80s | 341408 ko || -0m00.01s || -140 ko | -1.25% | -0.04%
0m00.73s | 345108 ko | Classes/orders/maps.vo | 0m00.59s | 345036 ko || +0m00.14s || 72 ko | +23.72% | +0.02%
0m00.71s | 349888 ko | Classes/theory/ua_first_isomorphism.vo | 0m00.66s | 349928 ko || +0m00.04s || -40 ko | +7.57% | -0.01%
0m00.68s | 381300 ko | Algebra/Groups/FreeGroup/LoopSusp.vo | 0m00.68s | 381192 ko || +0m00.00s || 108 ko | +0.00% | +0.02%
0m00.67s | 340776 ko | Classes/theory/groups.vo | 0m00.71s | 340900 ko || -0m00.03s || -124 ko | -5.63% | -0.03%
0m00.64s | 347800 ko | Classes/tactics/ring_tac.vo | 0m00.63s | 347856 ko || +0m00.01s || -56 ko | +1.58% | -0.01%
0m00.63s | 345392 ko | Algebra/Groups/FreeGroup.vo | 0m00.48s | 345444 ko || +0m00.15s || -52 ko | +31.25% | -0.01%
0m00.63s | 347604 ko | Classes/tests/ring_tac.vo | 0m00.66s | 347588 ko || -0m00.03s || 16 ko | -4.54% | +0.00%
0m00.59s | 347108 ko | Classes/orders/fields.vo | 0m00.58s | 347140 ko || +0m00.01s || -32 ko | +1.72% | -0.00%
0m00.59s | 343872 ko | Sets/AC.vo | 0m00.52s | 343916 ko || +0m00.06s || -44 ko | +13.46% | -0.01%
0m00.58s | 341832 ko | Classes/theory/lattices.vo | 0m00.76s | 341908 ko || -0m00.18s || -76 ko | -23.68% | -0.02%
0m00.57s | 404492 ko | Spaces/Torus/TorusHomotopy.vo | 0m00.85s | 404644 ko || -0m00.28s || -152 ko | -32.94% | -0.03%
0m00.56s | 349568 ko | Classes/orders/naturals.vo | 0m00.86s | 350372 ko || -0m00.29s || -804 ko | -34.88% | -0.22%
0m00.56s | 346880 ko | Classes/theory/ua_isomorphic.vo | 0m00.41s | 346804 ko || +0m00.15s || 76 ko | +36.58% | +0.02%
0m00.53s | 348080 ko | Algebra/Universal/TermAlgebra.vo | 0m00.56s | 347940 ko || -0m00.03s || 140 ko | -5.35% | +0.04%
0m00.52s | 345288 ko | Classes/tactics/ring_quote.vo | 0m00.41s | 345168 ko || +0m00.11s || 120 ko | +26.82% | +0.03%
0m00.52s | 342264 ko | Classes/theory/apartness.vo | 0m00.73s | 342300 ko || -0m00.20s || -36 ko | -28.76% | -0.01%
0m00.51s | 323700 ko | Algebra/Groups/Image.vo | 0m00.32s | 324440 ko || +0m00.19s || -740 ko | +59.37% | -0.22%
0m00.51s | 347472 ko | Classes/theory/ua_homomorphism.vo | 0m00.77s | 347456 ko || -0m00.26s || 16 ko | -33.76% | +0.00%
0m00.49s | 352788 ko | Algebra/Groups/Lagrange.vo | 0m00.51s | 352700 ko || -0m00.02s || 88 ko | -3.92% | +0.02%
0m00.48s | 355920 ko | Classes/orders/archimedean.vo | 0m00.38s | 355920 ko || +0m00.09s || 0 ko | +26.31% | +0.00%
0m00.47s | 301524 ko | Classes/interfaces/ua_algebra.vo | 0m00.50s | 301700 ko || -0m00.03s || -176 ko | -6.00% | -0.05%
0m00.46s | 476348 ko | HoTT.vo | 0m00.47s | 476320 ko || -0m00.00s || 28 ko | -2.12% | +0.00%
0m00.46s | 342064 ko | Sets/GCH.vo | 0m00.73s | 342112 ko || -0m00.26s || -48 ko | -36.98% | -0.01%
0m00.45s | 262176 ko | Classes/theory/ua_subalgebra.vo | 0m00.42s | 262296 ko || +0m00.03s || -120 ko | +7.14% | -0.04%
0m00.42s | 259404 ko | Classes/interfaces/orders.vo | 0m00.29s | 259696 ko || +0m00.13s || -292 ko | +44.82% | -0.11%
0m00.40s | 251516 ko | Classes/categories/ua_category.vo | 0m00.40s | 251416 ko || +0m00.00s || 100 ko | +0.00% | +0.03%
0m00.40s | 245888 ko | Classes/interfaces/ua_congruence.vo | 0m00.27s | 246704 ko || +0m00.13s || -816 ko | +48.14% | -0.33%
0m00.38s | 240196 ko | Algebra/Rings/Ideal.vo | 0m00.39s | 240376 ko || -0m00.01s || -180 ko | -2.56% | -0.07%
0m00.38s | 350124 ko | Classes/theory/nat_distance.vo | 0m00.54s | 349988 ko || -0m00.16s || 136 ko | -29.62% | +0.03%
0m00.35s | 353300 ko | Homotopy/Pi1S1.vo | 0m00.54s | 355492 ko || -0m00.19s || -2192 ko | -35.18% | -0.61%
0m00.34s | 214840 ko | Algebra/Rings.vo | 0m00.22s | 214920 ko || +0m00.12s || -80 ko | +54.54% | -0.03%
0m00.34s | 213884 ko | Classes/interfaces/rationals.vo | 0m00.20s | 214024 ko || +0m00.14s || -140 ko | +70.00% | -0.06%
0m00.34s | 225164 ko | Classes/theory/additional_operations.vo | 0m00.25s | 225684 ko || +0m00.09s || -520 ko | +36.00% | -0.23%
0m00.33s | 231216 ko | Homotopy/HSpace.vo | 0m00.34s | 231536 ko || -0m00.01s || -320 ko | -2.94% | -0.13%
0m00.33s | 196052 ko | Sets/Powers.vo | 0m00.31s | 196292 ko || +0m00.02s || -240 ko | +6.45% | -0.12%
0m00.32s | 280036 ko | Classes/interfaces/canonical_names.vo | 0m00.29s | 280792 ko || +0m00.03s || -756 ko | +10.34% | -0.26%
0m00.31s | 219628 ko | Algebra/AbGroups/Z.vo | 0m00.33s | 219892 ko || -0m00.02s || -264 ko | -6.06% | -0.12%
0m00.31s | 219432 ko | Algebra/Aut.vo | 0m00.35s | 219448 ko || -0m00.03s || -16 ko | -11.42% | -0.00%
0m00.31s | 201472 ko | Algebra/Groups.vo | 0m00.29s | 201500 ko || +0m00.02s || -28 ko | +6.89% | -0.01%
0m00.31s | 204360 ko | Classes/interfaces/integers.vo | 0m00.29s | 204820 ko || +0m00.02s || -460 ko | +6.89% | -0.22%
0m00.30s | 310396 ko | Algebra/AbGroups/AbPullback.vo | 0m00.47s | 311068 ko || -0m00.17s || -672 ko | -36.17% | -0.21%
0m00.30s | 201836 ko | Classes/interfaces/ua_setalgebra.vo | 0m00.31s | 201840 ko || -0m00.01s || -4 ko | -3.22% | -0.00%
0m00.29s | 215812 ko | Algebra/ooAction.vo | 0m00.31s | 215752 ko || -0m00.02s || 60 ko | -6.45% | +0.02%
0m00.29s | 195108 ko | Classes/implementations/assume_rationals.vo | 0m00.28s | 195244 ko || +0m00.00s || -136 ko | +3.57% | -0.06%
0m00.29s | 206544 ko | Classes/implementations/list.vo | 0m00.28s | 206596 ko || +0m00.00s || -52 ko | +3.57% | -0.02%
0m00.29s | 197596 ko | Classes/interfaces/archimedean.vo | 0m00.31s | 197324 ko || -0m00.02s || 272 ko | -6.45% | +0.13%
0m00.29s | 202596 ko | Classes/interfaces/round.vo | 0m00.29s | 203904 ko || +0m00.00s || -1308 ko | +0.00% | -0.64%
0m00.28s | 182076 ko | Classes/orders/sum.vo | 0m00.24s | 182112 ko || +0m00.04s || -36 ko | +16.66% | -0.01%
0m00.26s | 274032 ko | Classes/implementations/bool.vo | 0m00.40s | 281412 ko || -0m00.14s || -7380 ko | -35.00% | -2.62%
0m00.25s | 242700 ko | Algebra/Universal/Congruence.vo | 0m00.33s | 243320 ko || -0m00.08s || -620 ko | -24.24% | -0.25%
0m00.23s | 159848 ko | Algebra/Congruence.vo | 0m00.24s | 159936 ko || -0m00.00s || -88 ko | -4.16% | -0.05%
0m00.23s | 224936 ko | Classes/theory/ua_prod_algebra.vo | 0m00.38s | 224972 ko || -0m00.15s || -36 ko | -39.47% | -0.01%
0m00.22s | 146264 ko | Classes/interfaces/monad.vo | 0m00.20s | 146176 ko || +0m00.01s || 88 ko | +9.99% | +0.06%
0m00.21s | 207088 ko | Algebra/AbGroups.vo | 0m00.34s | 207024 ko || -0m00.13s || 64 ko | -38.23% | +0.03%
0m00.20s | 197616 ko | Classes/implementations/ne_list.vo | 0m00.30s | 197652 ko || -0m00.09s || -36 ko | -33.33% | -0.01%
0m00.18s | 178408 ko | Classes/interfaces/naturals.vo | 0m00.20s | 178520 ko || -0m00.02s || -112 ko | -10.00% | -0.06%
0m00.17s | 174344 ko | Classes/implementations/family_prod.vo | 0m00.25s | 174492 ko || -0m00.07s || -148 ko | -31.99% | -0.08%
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment