agda/notes/bench-std-lib.txt

Measuring type-checking time of standard library
========================================================================

2010-09-21

 306,014,890,300 bytes allocated in the heap
  17,346,349,120 bytes copied during GC
   1,464,083,660 bytes maximum residency (50 sample(s))
      12,714,572 bytes maximum slop
            1499 MB total memory in use (24 MB lost due to fragmentation)

  Generation 0: 390212 collections,     0 parallel, 77.29s, 101.98s elapsed
  Generation 1:    50 collections,     0 parallel, 636.20s, 748.34s elapsed

  INIT  time    0.00s  (  0.03s elapsed)
  MUT   time  712.56s  (744.07s elapsed)
  GC    time  713.49s  (850.33s elapsed)
  EXIT  time    0.00s  (  0.00s elapsed)
  Total time  1426.05s  (1594.42s elapsed)

  %GC time      50.0%  (53.3% elapsed)

  Alloc rate    429,456,148 bytes per MUT second

  Productivity  50.0% of total user, 44.7% of total elapsed


real	26m35.108s
user	23m46.053s
sys	0m20.290s

========================================================================

Linux agda 3.2.0-48-generic #74-Ubuntu SMP Thu Jun 6 19:43:26 UTC 2013 x86_64 x86_64 x86_64 GNU/Linux
vendor_id	: GenuineIntel
cpu family	: 6
model		: 23
model name	: Intel(R) Core(TM)2 Duo CPU     P8700  @ 2.53GHz
stepping	: 10
microcode	: 0xa07
cpu MHz		: 800.000
cache size	: 3072 KB
abel@agda:~/Agda$ procinfo
Memory:        Total        Used        Free     Buffers
RAM:         4001044     2963004     1038040       36760
Swap:       13309816      204776    13105040

-- 2012-07-03 Before parallel substitution into clausebody

Finished README.
 130,637,961,424 bytes allocated in the heap
  33,884,918,648 bytes copied during GC
     428,136,736 bytes maximum residency (116 sample(s))
      13,107,944 bytes maximum slop
            1131 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     250680 colls,     0 par   54.42s   54.53s     0.0002s    0.0064s
  Gen  1       116 colls,     0 par   31.07s   31.13s     0.2684s    1.0102s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  157.90s  (159.96s elapsed)
  GC      time   85.50s  ( 85.66s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  243.40s  (245.62s elapsed)

  %GC     time      35.1%  (34.9% elapsed)

  Alloc rate    827,344,868 bytes per MUT second

  Productivity  64.9% of total user, 64.3% of total elapsed


real	4m5.757s
user	4m1.295s
sys	0m2.236s

===========================================================================

bodrum:Agda abel$ hostinfo
Mach kernel version:
	 Darwin Kernel Version 10.8.0: Tue Jun  7 16:33:36 PDT 2011; root:xnu-1504.15.3~1/RELEASE_I386
Kernel configured for up to 2 processors.
2 processors are physically available.
2 processors are logically available.
Processor type: i486 (Intel 80486)
Processors active: 0 1
Primary memory available: 2.00 gigabytes
Default processor set: 94 tasks, 447 threads, 2 processors
Load average: 0.64, Mach factor: 1.35

2013-05-19 after RecCheck

  75,579,752,556 bytes allocated in the heap
  16,756,050,804 bytes copied during GC
     215,039,796 bytes maximum residency (109 sample(s))
       2,594,336 bytes maximum slop
             560 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     144381 colls,     0 par   52.68s   59.11s     0.0004s    0.1718s
  Gen  1       109 colls,     0 par   29.09s   98.23s     0.9012s    39.8655s

  INIT    time    0.00s  (  0.10s elapsed)
  MUT     time  188.68s  (206.39s elapsed)
  GC      time   81.77s  (157.34s elapsed)
  EXIT    time    0.00s  (  0.09s elapsed)
  Total   time  270.46s  (363.91s elapsed)

  %GC     time      30.2%  (43.2% elapsed)

  Alloc rate    400,569,600 bytes per MUT second

  Productivity  69.8% of total user, 51.8% of total elapsed


real	6m4.275s
user	4m30.457s
sys	0m6.233s

2013-05-19 Lazy printing of callInfo in termination checker.

Finished README.
  68,075,601,556 bytes allocated in the heap
  15,854,319,308 bytes copied during GC
     212,038,068 bytes maximum residency (108 sample(s))
       2,746,424 bytes maximum slop
             576 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     130021 colls,     0 par   48.09s   49.02s     0.0004s    0.0261s
  Gen  1       108 colls,     0 par   26.94s   28.28s     0.2619s    1.0745s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  165.06s  (172.83s elapsed)
  GC      time   75.03s  ( 77.30s elapsed)
  EXIT    time    0.00s  (  0.08s elapsed)
  Total   time  240.09s  (250.22s elapsed)

  %GC     time      31.3%  (30.9% elapsed)

  Alloc rate    412,438,874 bytes per MUT second

  Productivity  68.7% of total user, 66.0% of total elapsed


real	4m10.232s
user	4m0.093s
sys	0m2.625s

2013-05-19 After slight de-optimization of CompiledClause.Match

Finished README.
  68,104,175,060 bytes allocated in the heap
  15,854,664,684 bytes copied during GC
     209,297,324 bytes maximum residency (108 sample(s))
       2,616,740 bytes maximum slop
             571 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     130074 colls,     0 par   48.91s   49.87s     0.0004s    0.0112s
  Gen  1       108 colls,     0 par   27.19s   28.30s     0.2621s    0.9740s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  165.43s  (172.18s elapsed)
  GC      time   76.10s  ( 78.17s elapsed)
  EXIT    time    0.00s  (  0.08s elapsed)
  Total   time  241.54s  (250.44s elapsed)

  %GC     time      31.5%  (31.2% elapsed)

  Alloc rate    411,668,523 bytes per MUT second

  Productivity  68.5% of total user, 66.1% of total elapsed


real	4m10.484s
user	4m1.541s
sys	0m2.634s

Finished README.
  68,104,175,380 bytes allocated in the heap
  15,915,415,568 bytes copied during GC
     198,896,912 bytes maximum residency (108 sample(s))
       2,596,308 bytes maximum slop
             553 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     130074 colls,     0 par   48.71s   49.68s     0.0004s    0.0129s
  Gen  1       108 colls,     0 par   27.45s   28.65s     0.2653s    0.9398s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  165.32s  (168.53s elapsed)
  GC      time   76.16s  ( 78.33s elapsed)
  EXIT    time    0.00s  (  0.08s elapsed)
  Total   time  241.48s  (246.94s elapsed)

  %GC     time      31.5%  (31.7% elapsed)

  Alloc rate    411,949,745 bytes per MUT second

  Productivity  68.5% of total user, 66.9% of total elapsed


real	4m6.978s
user	4m1.485s
sys	0m2.605s


2013-05-19 After slight optimization of pushes in CompiledClause.Match

Finished README.
  68,112,580,876 bytes allocated in the heap
  15,920,140,440 bytes copied during GC
     215,269,448 bytes maximum residency (107 sample(s))
       2,656,360 bytes maximum slop
             559 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     130097 colls,     0 par   48.19s   49.28s     0.0004s    0.0377s
  Gen  1       107 colls,     0 par   27.34s   28.51s     0.2664s    0.9359s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  165.63s  (171.94s elapsed)
  GC      time   75.53s  ( 77.78s elapsed)
  EXIT    time    0.00s  (  0.08s elapsed)
  Total   time  241.17s  (249.80s elapsed)

  %GC     time      31.3%  (31.1% elapsed)

  Alloc rate    411,228,296 bytes per MUT second

  Productivity  68.7% of total user, 66.3% of total elapsed

real	4m9.827s
user	4m1.167s
sys	0m2.694s

-- 2013-05-20 After collecting callInfos in a list (instead of Set)

Finished README.
  68,102,263,108 bytes allocated in the heap
  15,988,910,928 bytes copied during GC
     227,494,048 bytes maximum residency (109 sample(s))
       3,045,404 bytes maximum slop
             587 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     130075 colls,     0 par   48.09s   49.07s     0.0004s    0.0222s
  Gen  1       109 colls,     0 par   27.44s   31.56s     0.2896s    2.9997s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  165.16s  (172.37s elapsed)
  GC      time   75.53s  ( 80.64s elapsed)
  EXIT    time    0.00s  (  0.08s elapsed)
  Total   time  240.70s  (253.09s elapsed)

  %GC     time      31.4%  (31.9% elapsed)

  Alloc rate    412,335,427 bytes per MUT second

  Productivity  68.6% of total user, 65.3% of total elapsed


real	4m13.147s
user	4m0.699s
sys	0m2.716s
Finished README.
  68,270,983,432 bytes allocated in the heap
  15,871,009,488 bytes copied during GC
     196,568,668 bytes maximum residency (107 sample(s))
       2,769,564 bytes maximum slop
             526 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     130398 colls,     0 par   48.12s   48.90s     0.0004s    0.0335s
  Gen  1       107 colls,     0 par   26.87s   28.12s     0.2628s    1.0491s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  165.14s  (170.30s elapsed)
  GC      time   74.99s  ( 77.01s elapsed)
  EXIT    time    0.00s  (  0.07s elapsed)
  Total   time  240.14s  (247.39s elapsed)

  %GC     time      31.2%  (31.1% elapsed)

  Alloc rate    413,405,449 bytes per MUT second

  Productivity  68.8% of total user, 66.8% of total elapsed


real	4m7.445s
user	4m0.136s
sys	0m2.577s


2013-05-22  After switching matcher to Elim

Finished README.
  69,157,095,040 bytes allocated in the heap
  15,994,690,448 bytes copied during GC
     197,749,912 bytes maximum residency (109 sample(s))
       3,021,992 bytes maximum slop
             528 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     132084 colls,     0 par   48.35s   49.07s     0.0004s    0.1426s
  Gen  1       109 colls,     0 par   27.08s   28.73s     0.2636s    1.3616s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  168.05s  (174.37s elapsed)
  GC      time   75.43s  ( 77.80s elapsed)
  EXIT    time    0.00s  (  0.07s elapsed)
  Total   time  243.49s  (252.24s elapsed)

  %GC     time      31.0%  (30.8% elapsed)

  Alloc rate    411,516,871 bytes per MUT second

  Productivity  69.0% of total user, 66.6% of total elapsed


real	4m12.313s
user	4m3.492s
sys	0m2.567s


-- After distinguishing projections in the reduction engine.

Finished README.
  69,814,903,748 bytes allocated in the heap
  15,990,476,820 bytes copied during GC
     192,471,484 bytes maximum residency (108 sample(s))
       2,741,844 bytes maximum slop
             526 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     133343 colls,     0 par   49.19s   50.84s     0.0004s    0.0164s
  Gen  1       108 colls,     0 par   27.40s   31.78s     0.2942s    2.6347s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  169.75s  (180.07s elapsed)
  GC      time   76.59s  ( 82.62s elapsed)
  EXIT    time    0.00s  (  0.07s elapsed)
  Total   time  246.35s  (262.76s elapsed)

  %GC     time      31.1%  (31.4% elapsed)

  Alloc rate    411,277,281 bytes per MUT second

  Productivity  68.9% of total user, 64.6% of total elapsed


real	4m22.790s
user	4m6.347s
sys	0m3.042s


----------------------------------------------------------------------

2012-10-04 NO COVERAGE CHECK

Finished README.
  78,037,786,900 bytes allocated in the heap
  16,984,306,616 bytes copied during GC
     190,683,928 bytes maximum residency (109 sample(s))
       3,265,464 bytes maximum slop
             519 MB total memory in use (0 MB lost due to fragmentation)

  Generation 0: 148331 collections,     0 parallel, 44.58s, 45.86s elapsed
  Generation 1:   109 collections,     0 parallel, 27.06s, 45.29s elapsed

  INIT  time    0.00s  (  0.01s elapsed)
  MUT   time  177.28s  (184.03s elapsed)
  GC    time   71.64s  ( 91.15s elapsed)
  EXIT  time    0.00s  (  0.00s elapsed)
  Total time  248.92s  (275.18s elapsed)

  %GC time      28.8%  (33.1% elapsed)

  Alloc rate    440,200,955 bytes per MUT second

  Productivity  71.2% of total user, 64.4% of total elapsed


real	4m35.293s
user	4m8.918s
sys	0m4.334s

Finished README.
  80,247,949,720 bytes allocated in the heap
  17,059,672,804 bytes copied during GC
     204,750,068 bytes maximum residency (108 sample(s))
       2,615,112 bytes maximum slop
             563 MB total memory in use (0 MB lost due to fragmentation)

  Generation 0: 152544 collections,     0 parallel, 44.45s, 45.74s elapsed
  Generation 1:   108 collections,     0 parallel, 26.10s, 32.46s elapsed

  INIT  time    0.00s  (  0.00s elapsed)
  MUT   time  180.51s  (184.48s elapsed)
  GC    time   70.55s  ( 78.20s elapsed)
  EXIT  time    0.00s  (  0.00s elapsed)
  Total time  251.07s  (262.68s elapsed)

  %GC time      28.1%  (29.8% elapsed)

  Alloc rate    444,553,407 bytes per MUT second

  Productivity  71.9% of total user, 68.7% of total elapsed


real	4m22.780s
user	4m11.066s
sys	0m4.140s

========================================================================

2013-10-12 Before big Elims refactoring

Finished README.
 143,958,275,608 bytes allocated in the heap
  37,124,554,568 bytes copied during GC
     438,285,912 bytes maximum residency (119 sample(s))
      11,712,840 bytes maximum slop
            1228 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     276184 colls,     0 par   68.18s   68.41s     0.0002s    0.0054s
  Gen  1       119 colls,     0 par   36.53s   36.73s     0.3086s    1.1208s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  183.17s  (183.97s elapsed)
  GC      time  104.71s  (105.14s elapsed)
  EXIT    time    0.11s  (  0.12s elapsed)
  Total   time  288.00s  (289.23s elapsed)

  %GC     time      36.4%  (36.4% elapsed)

  Alloc rate    785,910,943 bytes per MUT second

  Productivity  63.6% of total user, 63.4% of total elapsed


real	4m49.238s
user	4m45.546s
sys	0m2.476s


2013-10-12 After big Elims refactoring

Finished README.
 140,427,398,528 bytes allocated in the heap
  38,031,973,704 bytes copied during GC
     477,121,784 bytes maximum residency (123 sample(s))
      13,519,312 bytes maximum slop
            1252 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     269329 colls,     0 par   67.81s   68.34s     0.0003s    0.0081s
  Gen  1       123 colls,     0 par   37.01s   37.37s     0.3038s    1.2344s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  183.32s  (186.20s elapsed)
  GC      time  104.82s  (105.71s elapsed)
  EXIT    time    0.10s  (  0.11s elapsed)
  Total   time  288.25s  (292.03s elapsed)

  %GC     time      36.4%  (36.2% elapsed)

  Alloc rate    766,013,316 bytes per MUT second

  Productivity  63.6% of total user, 62.8% of total elapsed


real	4m52.038s
user	4m45.862s
sys	0m2.412s







Dell
===========================================================================

2013-10-29  After big elims refactoring & internal with-type checking.

Finished README.
 136,216,001,296 bytes allocated in the heap
  36,913,612,016 bytes copied during GC
     443,512,744 bytes maximum residency (122 sample(s))
      12,358,224 bytes maximum slop
            1204 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     261258 colls,     0 par   59.37s   59.48s     0.0002s    0.0057s
  Gen  1       122 colls,     0 par   33.92s   34.00s     0.2787s    1.0220s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  161.52s  (164.03s elapsed)
  GC      time   93.29s  ( 93.48s elapsed)
  EXIT    time    0.16s  (  0.17s elapsed)
  Total   time  254.97s  (257.68s elapsed)

  %GC     time      36.6%  (36.3% elapsed)

  Alloc rate    843,329,035 bytes per MUT second

  Productivity  63.4% of total user, 62.7% of total elapsed


real	4m17.703s
user	4m12.820s
sys	0m2.172s

---------------------------------------------------------------------------

2013-09-18 with copatterns in internal syntax

Finished README.
 130,053,317,416 bytes allocated in the heap
  33,621,753,864 bytes copied during GC
     406,414,400 bytes maximum residency (117 sample(s))
      11,609,064 bytes maximum slop
            1137 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     249559 colls,     0 par   61.93s   62.37s     0.0002s    0.0207s
  Gen  1       117 colls,     0 par   32.54s   32.95s     0.2816s    1.0906s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  176.64s  (179.62s elapsed)
  GC      time   94.47s  ( 95.32s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  271.11s  (274.94s elapsed)

  %GC     time      34.8%  (34.7% elapsed)

  Alloc rate    736,259,306 bytes per MUT second

  Productivity  65.2% of total user, 64.2% of total elapsed

---------------------------------------------------------------------------

2013-06-15 on 64bit Linux

AFTER projection-shortcut

Finished README.
 132,988,745,160 bytes allocated in the heap
  35,174,174,456 bytes copied during GC
     429,758,624 bytes maximum residency (117 sample(s))
      12,817,040 bytes maximum slop
            1143 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     255131 colls,     0 par   55.38s   55.46s     0.0002s    0.0074s
  Gen  1       117 colls,     0 par   31.72s   32.03s     0.2738s    1.0241s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  150.17s  (150.51s elapsed)
  GC      time   87.10s  ( 87.49s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  237.27s  (238.01s elapsed)

  %GC     time      36.7%  (36.8% elapsed)

  Alloc rate    885,573,554 bytes per MUT second

  Productivity  63.3% of total user, 63.1% of total elapsed


real	3m58.117s
user	3m55.391s
sys	0m1.996s

Finished README.
 132,987,924,232 bytes allocated in the heap
  35,182,173,632 bytes copied during GC
     430,702,512 bytes maximum residency (117 sample(s))
      12,730,336 bytes maximum slop
            1137 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     255130 colls,     0 par   54.53s   54.60s     0.0002s    0.0052s
  Gen  1       117 colls,     0 par   31.28s   31.35s     0.2679s    1.0141s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  148.40s  (148.64s elapsed)
  GC      time   85.82s  ( 85.95s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  234.21s  (234.59s elapsed)

  %GC     time      36.6%  (36.6% elapsed)

  Alloc rate    896,151,147 bytes per MUT second

  Productivity  63.4% of total user, 63.3% of total elapsed


real	3m54.702s
user	3m52.543s
sys	0m1.792s

Finished README.
 132,987,923,024 bytes allocated in the heap
  35,191,095,408 bytes copied during GC
     388,889,688 bytes maximum residency (117 sample(s))
      10,510,504 bytes maximum slop
            1081 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     255130 colls,     0 par   54.77s   54.84s     0.0002s    0.0123s
  Gen  1       117 colls,     0 par   31.44s   31.49s     0.2691s    0.9095s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  148.96s  (149.20s elapsed)
  GC      time   86.21s  ( 86.33s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  235.17s  (235.53s elapsed)

  %GC     time      36.7%  (36.7% elapsed)

  Alloc rate    892,756,844 bytes per MUT second

  Productivity  63.3% of total user, 63.2% of total elapsed


real	3m55.632s
user	3m53.275s
sys	0m2.004s




BEFORE

Finished README.
 134,909,722,296 bytes allocated in the heap
  35,070,686,432 bytes copied during GC
     425,329,288 bytes maximum residency (118 sample(s))
      11,060,336 bytes maximum slop
            1173 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     258867 colls,     0 par   54.69s   54.80s     0.0002s    0.0091s
  Gen  1       118 colls,     0 par   30.79s   30.92s     0.2620s    0.9669s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  156.70s  (159.68s elapsed)
  GC      time   85.49s  ( 85.71s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  242.19s  (245.39s elapsed)

  %GC     time      35.3%  (34.9% elapsed)

  Alloc rate    860,928,970 bytes per MUT second

  Productivity  64.7% of total user, 63.9% of total elapsed


real	4m5.500s
user	4m0.279s
sys	0m2.028s

Finished README.
 134,909,722,296 bytes allocated in the heap
  35,070,561,616 bytes copied during GC
     425,249,304 bytes maximum residency (118 sample(s))
      11,056,328 bytes maximum slop
            1172 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     258867 colls,     0 par   53.88s   53.95s     0.0002s    0.0084s
  Gen  1       118 colls,     0 par   30.74s   30.80s     0.2610s    0.9587s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  154.45s  (154.71s elapsed)
  GC      time   84.61s  ( 84.75s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  239.07s  (239.46s elapsed)

  %GC     time      35.4%  (35.4% elapsed)

  Alloc rate    873,475,835 bytes per MUT second

  Productivity  64.6% of total user, 64.5% of total elapsed


real	3m59.566s
user	3m46.690s
sys	0m12.493s

Finished README.
 134,909,722,296 bytes allocated in the heap
  35,070,573,616 bytes copied during GC
     425,329,288 bytes maximum residency (118 sample(s))
      11,060,336 bytes maximum slop
            1172 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     258867 colls,     0 par   53.96s   54.02s     0.0002s    0.0049s
  Gen  1       118 colls,     0 par   30.54s   30.59s     0.2592s    0.9685s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  154.51s  (154.71s elapsed)
  GC      time   84.50s  ( 84.61s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  239.00s  (239.32s elapsed)

  %GC     time      35.4%  (35.4% elapsed)

  Alloc rate    873,154,268 bytes per MUT second

  Productivity  64.6% of total user, 64.6% of total elapsed


real	3m59.428s
user	3m57.203s
sys	0m1.920s

---------------------------------------------------------------------------

2012-10-19 after some refactoring in Termination checker

Finished README.
 121,959,633,896 bytes allocated in the heap
  32,558,017,400 bytes copied during GC
     425,995,760 bytes maximum residency (115 sample(s))
      11,374,400 bytes maximum slop
            1171 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     234031 colls,     0 par   49.44s   49.48s     0.0002s    0.0040s
  Gen  1       115 colls,     0 par   28.13s   28.17s     0.2450s    0.9735s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  136.74s  (136.94s elapsed)
  GC      time   77.57s  ( 77.66s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  214.31s  (214.59s elapsed)

  %GC     time      36.2%  (36.2% elapsed)

  Alloc rate    891,883,628 bytes per MUT second

  Productivity  63.8% of total user, 63.7% of total elapsed


real	3m34.684s
user	3m32.753s
sys	0m1.612s

---------------------------------------------------------------------------

2012-10-19 before refactoring in Termination checker

Finished README.
 121,815,567,840 bytes allocated in the heap
  32,445,394,648 bytes copied during GC
     424,453,984 bytes maximum residency (115 sample(s))
      11,429,312 bytes maximum slop
            1167 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     233753 colls,     0 par   50.86s   51.02s     0.0002s    0.0157s
  Gen  1       115 colls,     0 par   28.55s   29.18s     0.2537s    0.9547s

  INIT    time    0.00s  (  0.02s elapsed)
  MUT     time  141.19s  (145.10s elapsed)
  GC      time   79.41s  ( 80.19s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  220.61s  (225.31s elapsed)

  %GC     time      36.0%  (35.6% elapsed)

  Alloc rate    862,751,248 bytes per MUT second

  Productivity  64.0% of total user, 62.7% of total elapsed


real	3m45.487s
user	3m38.674s
sys	0m1.984s

---------------------------------------------------------------------------

2012-10-11  before Q-combinators

Finished README.
 124,694,669,672 bytes allocated in the heap
  32,858,769,616 bytes copied during GC
     393,808,808 bytes maximum residency (116 sample(s))
      11,293,480 bytes maximum slop
            1096 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     239318 colls,     0 par   50.15s   50.23s     0.0002s    0.0058s
  Gen  1       116 colls,     0 par   29.04s   29.11s     0.2509s    0.8877s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  146.12s  (147.23s elapsed)
  GC      time   79.19s  ( 79.33s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  225.32s  (226.56s elapsed)

  %GC     time      35.1%  (35.0% elapsed)

  Alloc rate    853,361,479 bytes per MUT second

  Productivity  64.9% of total user, 64.5% of total elapsed


real	3m46.682s
user	3m43.762s
sys	0m1.620s

2012-10-11 after Q-combinators

Finished README.
 167,955,189,616 bytes allocated in the heap
  34,462,143,544 bytes copied during GC
     436,298,656 bytes maximum residency (117 sample(s))
      12,326,752 bytes maximum slop
            1128 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     323215 colls,     0 par   54.37s   54.40s     0.0002s    0.0042s
  Gen  1       117 colls,     0 par   30.38s   30.43s     0.2601s    1.0572s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  160.82s  (161.01s elapsed)
  GC      time   84.76s  ( 84.83s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  245.58s  (245.84s elapsed)

  %GC     time      34.5%  (34.5% elapsed)

  Alloc rate    1,044,367,122 bytes per MUT second

  Productivity  65.5% of total user, 65.4% of total elapsed


real	4m5.949s
user	4m3.855s
sys	0m1.788s

-- after sharing for Level and Sort

Finished README.
 137,866,022,280 bytes allocated in the heap
  39,203,587,128 bytes copied during GC
     467,675,112 bytes maximum residency (115 sample(s))
      11,606,400 bytes maximum slop
            1272 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     264616 colls,     0 par   58.28s   58.33s     0.0002s    0.0041s
  Gen  1       115 colls,     0 par   30.84s   30.89s     0.2686s    1.0803s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  152.62s  (152.85s elapsed)
  GC      time   89.12s  ( 89.22s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  241.74s  (242.07s elapsed)

  %GC     time      36.9%  (36.9% elapsed)

  Alloc rate    903,303,234 bytes per MUT second

  Productivity  63.1% of total user, 63.1% of total elapsed


real	4m2.185s
user	3m59.791s
sys	0m2.024s

-- after sharing for Type

Finished README.
 137,749,742,112 bytes allocated in the heap
  39,262,668,112 bytes copied during GC
     392,507,192 bytes maximum residency (117 sample(s))
      13,044,776 bytes maximum slop
            1061 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     264398 colls,     0 par   57.97s   58.02s     0.0002s    0.0035s
  Gen  1       117 colls,     0 par   30.96s   31.01s     0.2650s    0.9263s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  152.62s  (152.81s elapsed)
  GC      time   88.93s  ( 89.03s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  241.55s  (241.84s elapsed)

  %GC     time      36.8%  (36.8% elapsed)

  Alloc rate    902,563,883 bytes per MUT second

  Productivity  63.2% of total user, 63.1% of total elapsed


real	4m1.950s
user	3m59.791s
sys	0m1.824s

-- after disabling Q-combinators (replacing by mock impl.)

Finished README.
 128,043,597,248 bytes allocated in the heap
  33,158,554,856 bytes copied during GC
     397,245,144 bytes maximum residency (116 sample(s))
      10,316,488 bytes maximum slop
            1105 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     245725 colls,     0 par   50.90s   51.00s     0.0002s    0.0092s
  Gen  1       116 colls,     0 par   29.58s   29.63s     0.2554s    0.9142s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  145.96s  (146.82s elapsed)
  GC      time   80.48s  ( 80.63s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  226.45s  (227.45s elapsed)

  %GC     time      35.5%  (35.4% elapsed)

  Alloc rate    877,216,735 bytes per MUT second

  Productivity  64.5% of total user, 64.2% of total elapsed


real	3m47.577s
user	3m44.774s
sys	0m1.744s


===========================================================================
  MacBook
===========================================================================

2012-11-05 on ghc 7.6; after not reducing meta var args

Finished README.
  59,509,181,224 bytes allocated in the heap
  14,495,673,316 bytes copied during GC
     195,961,356 bytes maximum residency (105 sample(s))
       2,530,548 bytes maximum slop
             546 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     113647 colls,     0 par   43.12s   44.25s     0.0004s    0.0388s
  Gen  1       105 colls,     0 par   24.28s   28.45s     0.2710s    2.8860s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  142.56s  (145.47s elapsed)
  GC      time   67.41s  ( 72.70s elapsed)
  EXIT    time    0.00s  (  0.08s elapsed)
  Total   time  209.97s  (218.25s elapsed)

  %GC     time      32.1%  (33.3% elapsed)

  Alloc rate    417,442,876 bytes per MUT second

  Productivity  67.9% of total user, 65.3% of total elapsed


real	3m38.275s
user	3m29.967s
sys	0m2.872s

  59,509,174,888 bytes allocated in the heap
  14,421,736,476 bytes copied during GC
     212,352,780 bytes maximum residency (102 sample(s))
       2,448,736 bytes maximum slop
             545 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     113649 colls,     0 par   43.25s   43.96s     0.0004s    0.0135s
  Gen  1       102 colls,     0 par   24.30s   25.12s     0.2463s    0.9028s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  142.11s  (144.55s elapsed)
  GC      time   67.55s  ( 69.08s elapsed)
  EXIT    time    0.00s  (  0.08s elapsed)
  Total   time  209.66s  (213.71s elapsed)

  %GC     time      32.2%  (32.3% elapsed)

  Alloc rate    418,755,431 bytes per MUT second

  Productivity  67.8% of total user, 66.5% of total elapsed


real	3m33.900s
user	3m29.659s
sys	0m2.151s

Finished README.
  59,509,174,888 bytes allocated in the heap
  14,421,441,332 bytes copied during GC
     212,352,792 bytes maximum residency (102 sample(s))
       2,446,640 bytes maximum slop
             545 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     113649 colls,     0 par   44.61s   47.15s     0.0004s    0.0076s
  Gen  1       102 colls,     0 par   24.72s   27.81s     0.2726s    1.8119s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  145.57s  (155.68s elapsed)
  GC      time   69.33s  ( 74.96s elapsed)
  EXIT    time    0.00s  (  0.09s elapsed)
  Total   time  214.90s  (230.72s elapsed)

  %GC     time      32.3%  (32.5% elapsed)

  Alloc rate    408,792,540 bytes per MUT second

  Productivity  67.7% of total user, 63.1% of total elapsed


real	3m50.990s
user	3m34.905s
sys	0m2.824s

-- before ------------------------------------------------------------

Finished README.
  59,879,530,172 bytes allocated in the heap
  14,509,855,452 bytes copied during GC
     196,475,072 bytes maximum residency (104 sample(s))
       2,583,308 bytes maximum slop
             547 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     114354 colls,     0 par   46.99s   49.03s     0.0004s    0.0131s
  Gen  1       104 colls,     0 par   25.66s   27.80s     0.2673s    1.2198s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  146.43s  (153.83s elapsed)
  GC      time   72.64s  ( 76.84s elapsed)
  EXIT    time    0.00s  (  0.08s elapsed)
  Total   time  219.08s  (230.77s elapsed)

  %GC     time      33.2%  (33.3% elapsed)

  Alloc rate    408,924,357 bytes per MUT second

  Productivity  66.8% of total user, 63.5% of total elapsed


real	3m51.019s
user	3m39.078s
sys	0m3.259s

Finished README.
  59,879,529,056 bytes allocated in the heap
  14,510,928,208 bytes copied during GC
     196,475,048 bytes maximum residency (104 sample(s))
       2,584,048 bytes maximum slop
             547 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     114354 colls,     0 par   46.82s   48.84s     0.0004s    0.0546s
  Gen  1       104 colls,     0 par   25.70s   33.63s     0.3234s    5.0270s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  145.85s  (157.93s elapsed)
  GC      time   72.52s  ( 82.47s elapsed)
  EXIT    time    0.00s  (  0.08s elapsed)
  Total   time  218.37s  (240.48s elapsed)

  %GC     time      33.2%  (34.3% elapsed)

  Alloc rate    410,563,952 bytes per MUT second

  Productivity  66.8% of total user, 60.6% of total elapsed


real	4m0.535s
user	3m38.368s
sys	0m3.182s

---------------------------------------------------------------------------

2012-09-28  before optimizing makeProjection (check for rec. occurrence)

Finished README.
  80,721,605,252 bytes allocated in the heap
  17,090,526,016 bytes copied during GC
     196,887,864 bytes maximum residency (109 sample(s))
       2,629,552 bytes maximum slop
             542 MB total memory in use (0 MB lost due to fragmentation)

  Generation 0: 153448 collections,     0 parallel, 44.98s, 45.94s elapsed
  Generation 1:   109 collections,     0 parallel, 25.82s, 32.12s elapsed

  INIT  time    0.00s  (  0.00s elapsed)
  MUT   time  182.49s  (189.00s elapsed)
  GC    time   70.80s  ( 78.07s elapsed)
  EXIT  time    0.00s  (  0.00s elapsed)
  Total time  253.29s  (267.07s elapsed)

  %GC time      28.0%  (29.2% elapsed)

  Alloc rate    442,322,078 bytes per MUT second

  Productivity  72.0% of total user, 68.3% of total elapsed


real	4m27.153s
user	4m13.292s
sys	0m3.450s

-- after optimizing makeProjection

Finished README.
  80,249,881,712 bytes allocated in the heap
  17,097,089,648 bytes copied during GC
     209,054,360 bytes maximum residency (107 sample(s))
       2,853,036 bytes maximum slop
             567 MB total memory in use (0 MB lost due to fragmentation)

  Generation 0: 152548 collections,     0 parallel, 44.26s, 44.98s elapsed
  Generation 1:   107 collections,     0 parallel, 25.97s, 30.17s elapsed

  INIT  time    0.00s  (  0.00s elapsed)
  MUT   time  178.72s  (181.52s elapsed)
  GC    time   70.23s  ( 75.15s elapsed)
  EXIT  time    0.00s  (  0.00s elapsed)
  Total time  248.95s  (256.67s elapsed)

  %GC time      28.2%  (29.3% elapsed)

  Alloc rate    449,024,097 bytes per MUT second

  Productivity  71.8% of total user, 69.6% of total elapsed


real	4m16.767s
user	4m8.953s
sys	0m3.051s

-- further tiny optimization (no noticeable difference)

Finished README.
  80,247,735,324 bytes allocated in the heap
  17,108,704,696 bytes copied during GC
     214,395,356 bytes maximum residency (108 sample(s))
       2,824,328 bytes maximum slop
             560 MB total memory in use (0 MB lost due to fragmentation)

  Generation 0: 152543 collections,     0 parallel, 44.35s, 45.02s elapsed
  Generation 1:   108 collections,     0 parallel, 25.86s, 26.68s elapsed

  INIT  time    0.00s  (  0.00s elapsed)
  MUT   time  179.28s  (181.47s elapsed)
  GC    time   70.21s  ( 71.69s elapsed)
  EXIT  time    0.00s  (  0.00s elapsed)
  Total time  249.50s  (253.16s elapsed)

  %GC time      28.1%  (28.3% elapsed)

  Alloc rate    447,599,035 bytes per MUT second

  Productivity  71.9% of total user, 70.8% of total elapsed


real	4m13.258s
user	4m9.498s
sys	0m2.921s

========================================================================

2013-06-15 on 64bit Linux

AFTER projection-shortcut

Finished README.
 132,988,745,160 bytes allocated in the heap
  35,174,174,456 bytes copied during GC
     429,758,624 bytes maximum residency (117 sample(s))
      12,817,040 bytes maximum slop
            1143 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     255131 colls,     0 par   55.38s   55.46s     0.0002s    0.0074s
  Gen  1       117 colls,     0 par   31.72s   32.03s     0.2738s    1.0241s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  150.17s  (150.51s elapsed)
  GC      time   87.10s  ( 87.49s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  237.27s  (238.01s elapsed)

  %GC     time      36.7%  (36.8% elapsed)

  Alloc rate    885,573,554 bytes per MUT second

  Productivity  63.3% of total user, 63.1% of total elapsed


real	3m58.117s
user	3m55.391s
sys	0m1.996s

Finished README.
 132,987,924,232 bytes allocated in the heap
  35,182,173,632 bytes copied during GC
     430,702,512 bytes maximum residency (117 sample(s))
      12,730,336 bytes maximum slop
            1137 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     255130 colls,     0 par   54.53s   54.60s     0.0002s    0.0052s
  Gen  1       117 colls,     0 par   31.28s   31.35s     0.2679s    1.0141s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  148.40s  (148.64s elapsed)
  GC      time   85.82s  ( 85.95s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  234.21s  (234.59s elapsed)

  %GC     time      36.6%  (36.6% elapsed)

  Alloc rate    896,151,147 bytes per MUT second

  Productivity  63.4% of total user, 63.3% of total elapsed


real	3m54.702s
user	3m52.543s
sys	0m1.792s

Finished README.
 132,987,923,024 bytes allocated in the heap
  35,191,095,408 bytes copied during GC
     388,889,688 bytes maximum residency (117 sample(s))
      10,510,504 bytes maximum slop
            1081 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     255130 colls,     0 par   54.77s   54.84s     0.0002s    0.0123s
  Gen  1       117 colls,     0 par   31.44s   31.49s     0.2691s    0.9095s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  148.96s  (149.20s elapsed)
  GC      time   86.21s  ( 86.33s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  235.17s  (235.53s elapsed)

  %GC     time      36.7%  (36.7% elapsed)

  Alloc rate    892,756,844 bytes per MUT second

  Productivity  63.3% of total user, 63.2% of total elapsed


real	3m55.632s
user	3m53.275s
sys	0m2.004s




BEFORE

Finished README.
 134,909,722,296 bytes allocated in the heap
  35,070,686,432 bytes copied during GC
     425,329,288 bytes maximum residency (118 sample(s))
      11,060,336 bytes maximum slop
            1173 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     258867 colls,     0 par   54.69s   54.80s     0.0002s    0.0091s
  Gen  1       118 colls,     0 par   30.79s   30.92s     0.2620s    0.9669s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  156.70s  (159.68s elapsed)
  GC      time   85.49s  ( 85.71s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  242.19s  (245.39s elapsed)

  %GC     time      35.3%  (34.9% elapsed)

  Alloc rate    860,928,970 bytes per MUT second

  Productivity  64.7% of total user, 63.9% of total elapsed


real	4m5.500s
user	4m0.279s
sys	0m2.028s

Finished README.
 134,909,722,296 bytes allocated in the heap
  35,070,561,616 bytes copied during GC
     425,249,304 bytes maximum residency (118 sample(s))
      11,056,328 bytes maximum slop
            1172 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     258867 colls,     0 par   53.88s   53.95s     0.0002s    0.0084s
  Gen  1       118 colls,     0 par   30.74s   30.80s     0.2610s    0.9587s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  154.45s  (154.71s elapsed)
  GC      time   84.61s  ( 84.75s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  239.07s  (239.46s elapsed)

  %GC     time      35.4%  (35.4% elapsed)

  Alloc rate    873,475,835 bytes per MUT second

  Productivity  64.6% of total user, 64.5% of total elapsed


real	3m59.566s
user	3m46.690s
sys	0m12.493s

Finished README.
 134,909,722,296 bytes allocated in the heap
  35,070,573,616 bytes copied during GC
     425,329,288 bytes maximum residency (118 sample(s))
      11,060,336 bytes maximum slop
            1172 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     258867 colls,     0 par   53.96s   54.02s     0.0002s    0.0049s
  Gen  1       118 colls,     0 par   30.54s   30.59s     0.2592s    0.9685s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  154.51s  (154.71s elapsed)
  GC      time   84.50s  ( 84.61s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  239.00s  (239.32s elapsed)

  %GC     time      35.4%  (35.4% elapsed)

  Alloc rate    873,154,268 bytes per MUT second

  Productivity  64.6% of total user, 64.6% of total elapsed


real	3m59.428s
user	3m57.203s
sys	0m1.920s



2013-03-23 Benchmark facility

Finished README.
Total time         251099 ms
Parsing              2296 ms
Import               4588 ms
Deserialization        48 ms
Scoping             21561 ms
Typing             399617 ms
Termination          9228 ms
Positivity           4420 ms
Injectivity           560 ms
ProjectionLikeness    108 ms
Coverage             1776 ms
Highlighting         5516 ms
Serialization      145509 ms

 138,059,997,864 bytes allocated in the heap
  16,552,778,160 bytes copied during GC
     398,039,296 bytes maximum residency (42 sample(s))
       5,607,064 bytes maximum slop
            1161 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1539 colls,     0 par   46.08s   46.19s     0.0300s    0.3859s
  Gen  1        42 colls,     0 par   14.64s   14.70s     0.3499s    0.8874s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  190.36s  (191.33s elapsed)
  GC      time   60.72s  ( 60.89s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  251.13s  (252.25s elapsed)

  %GC     time      24.2%  (24.1% elapsed)

  Alloc rate    725,244,231 bytes per MUT second

  Productivity  75.8% of total user, 75.5% of total elapsed


real	4m12.375s
user	4m9.632s
sys	0m1.620s

Finished README.
Total time         254387 ms
Parsing              1504 ms
Import               4704 ms
Deserialization        24 ms
Scoping             22953 ms
Typing              53143 ms
Termination          9356 ms
Positivity           4252 ms
Injectivity           608 ms
ProjectionLikeness    132 ms
Coverage             1780 ms
Highlighting         5672 ms
Serialization      146953 ms

 138,019,481,984 bytes allocated in the heap
  16,547,405,232 bytes copied during GC
     398,005,544 bytes maximum residency (42 sample(s))
       5,647,360 bytes maximum slop
            1161 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1543 colls,     0 par   46.39s   46.56s     0.0302s 0.4004s
  Gen  1        42 colls,     0 par   14.98s   15.04s     0.3582s 0.8879s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  193.00s  (193.74s elapsed)
  GC      time   61.38s  ( 61.61s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  254.41s  (255.39s elapsed)

  %GC     time      24.1%  (24.1% elapsed)

  Alloc rate    715,141,070 bytes per MUT second

  Productivity  75.9% of total user, 75.6% of total elapsed


real    4m15.498s
user    4m11.532s
sys    0m2.996s



2014-03-25  Introducing some strictness in billTo

Finished README.
Total time           263108 ms
Parsing                1528 ms
Import                 3976 ms
Deserialization          16 ms
Scoping               22681 ms
Typing                53623 ms
Termination            9804 ms
Termination.Graph       204 ms
Termination.RecCheck   2444 ms
Termination.Reduce       64 ms
Positivity             4592 ms
Injectivity             640 ms
ProjectionLikeness      152 ms
Coverage               1772 ms
Highlighting           6012 ms
Serialization        154949 ms

 137,157,635,640 bytes allocated in the heap
  15,996,149,208 bytes copied during GC
     490,945,992 bytes maximum residency (42 sample(s))
       7,079,880 bytes maximum slop
            1171 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1512 colls,     0 par   48.53s   48.66s     0.0322s    0.4164s
  Gen  1        42 colls,     0 par   17.26s   19.10s     0.4547s    2.5897s

  INIT    time    0.00s  (  0.08s elapsed)
  MUT     time  197.31s  (202.32s elapsed)
  GC      time   65.78s  ( 67.76s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  263.14s  (270.19s elapsed)

  %GC     time      25.0%  (25.1% elapsed)

  Alloc rate    695,123,329 bytes per MUT second

  Productivity  75.0% of total user, 73.0% of total elapsed


real	4m30.546s
user	4m20.856s
sys	0m2.440s


Finished README.
Total time           263288 ms
Parsing                1588 ms
Import                 3844 ms
Deserialization          52 ms
Scoping               22821 ms
Typing                53651 ms
Termination            9856 ms
Termination.Graph       208 ms
Termination.RecCheck   2420 ms
Termination.Reduce       56 ms
Positivity             4416 ms
Injectivity             656 ms
ProjectionLikeness      124 ms
Coverage               1828 ms
Highlighting           6076 ms
Serialization        155185 ms

 137,154,612,136 bytes allocated in the heap
  15,994,583,888 bytes copied during GC
     490,945,664 bytes maximum residency (42 sample(s))
       7,088,584 bytes maximum slop
            1179 MB total memory in use (8 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1512 colls,     0 par   48.10s   48.30s     0.0319s    0.4073s
  Gen  1        42 colls,     0 par   17.17s   17.25s     0.4107s    2.7086s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  198.00s  (198.61s elapsed)
  GC      time   65.27s  ( 65.55s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  263.31s  (264.19s elapsed)

  %GC     time      24.8%  (24.8% elapsed)

  Alloc rate    692,686,792 bytes per MUT second

  Productivity  75.2% of total user, 75.0% of total elapsed


real	4m24.350s
user	4m17.988s
sys	0m5.488s



-- 2014-03-26 before ExtractCalls for Level


Finished README.
Total time           248087 ms
Parsing                1532 ms
Import                 3976 ms
Deserialization          48 ms
Scoping               22465 ms
Typing                52075 ms
Termination            7876 ms
Termination.Graph       200 ms
Termination.RecCheck   1932 ms
Termination.Level        52 ms
Positivity             3912 ms
Injectivity             600 ms
ProjectionLikeness      124 ms
Coverage               1700 ms
Highlighting           5580 ms
Serialization        144605 ms

 137,194,284,352 bytes allocated in the heap
  16,545,914,496 bytes copied during GC
     398,693,144 bytes maximum residency (43 sample(s))
       5,675,176 bytes maximum slop
            1169 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1566 colls,     0 par   45.29s   45.40s     0.0290s    0.3915s
  Gen  1        43 colls,     0 par   14.54s   14.57s     0.3387s    0.8458s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  188.25s  (192.34s elapsed)
  GC      time   59.83s  ( 59.97s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  248.11s  (252.34s elapsed)

  %GC     time      24.1%  (23.8% elapsed)

  Alloc rate    728,801,450 bytes per MUT second

  Productivity  75.9% of total user, 74.6% of total elapsed


real	4m12.456s
user	4m6.387s
sys	0m1.848s


-- 2014-03-26 after ExtractCalls for Level

Finished README.
Total time           246411 ms
Parsing                1556 ms
Import                 3948 ms
Deserialization          16 ms
Scoping               22637 ms
Typing                51807 ms
Termination            7764 ms
Termination.Graph       208 ms
Termination.RecCheck   1880 ms
Termination.Level        20 ms
Positivity             3744 ms
Injectivity             564 ms
ProjectionLikeness      120 ms
Coverage               1848 ms
Highlighting           5836 ms
Serialization        142900 ms

 137,191,518,344 bytes allocated in the heap
  16,546,478,920 bytes copied during GC
     398,694,392 bytes maximum residency (43 sample(s))
       5,636,896 bytes maximum slop
            1169 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1565 colls,     0 par   45.33s   45.42s     0.0290s    0.3917s
  Gen  1        43 colls,     0 par   14.61s   14.64s     0.3405s    0.8372s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  186.45s  (187.16s elapsed)
  GC      time   59.94s  ( 60.06s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  246.43s  (247.25s elapsed)

  %GC     time      24.3%  (24.3% elapsed)

  Alloc rate    735,802,724 bytes per MUT second

  Productivity  75.7% of total user, 75.4% of total elapsed


real	4m7.381s
user	4m5.219s
sys	0m1.344s


-- 2014-03-26 Termination.Order.Decr strict

Finished README.
Total time           247827 ms
Parsing                1432 ms
Import                 3820 ms
Deserialization          24 ms
Scoping               22353 ms
Typing                51875 ms
Termination            7740 ms
Termination.Graph       200 ms
Termination.RecCheck   1836 ms
Positivity             3912 ms
Injectivity             560 ms
ProjectionLikeness      104 ms
Coverage               1792 ms
Highlighting           5668 ms
Serialization        144757 ms

 137,145,130,336 bytes allocated in the heap
  16,545,617,504 bytes copied during GC
     398,689,192 bytes maximum residency (43 sample(s))
       5,650,752 bytes maximum slop
            1169 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1568 colls,     0 par   45.39s   45.50s     0.0290s    0.3973s
  Gen  1        43 colls,     0 par   14.80s   14.83s     0.3448s    0.8503s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  187.62s  (188.07s elapsed)
  GC      time   60.19s  ( 60.32s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  247.85s  (248.43s elapsed)

  %GC     time      24.3%  (24.3% elapsed)

  Alloc rate    730,974,405 bytes per MUT second

  Productivity  75.7% of total user, 75.5% of total elapsed


real	4m8.563s
user	4m6.639s
sys	0m1.340s

-- 2014-03-26 after discovering that prettyTCM g takes 50% of all termination time

Finished README.
Total time           243983 ms
Parsing                1476 ms
Import                 4624 ms
Deserialization          44 ms
Scoping               22457 ms
Typing                50871 ms
Termination            3264 ms
Termination.Graph       176 ms
Termination.RecCheck   1768 ms
Termination.Compare     548 ms
Positivity             3800 ms
Injectivity             656 ms
ProjectionLikeness      132 ms
Coverage               2024 ms
Highlighting           5692 ms
Serialization        144725 ms

 134,339,588,640 bytes allocated in the heap
  16,557,849,448 bytes copied during GC
     398,704,568 bytes maximum residency (43 sample(s))
       5,595,760 bytes maximum slop
            1149 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1547 colls,     0 par   45.49s   45.57s     0.0295s    0.3847s
  Gen  1        43 colls,     0 par   14.54s   14.56s     0.3386s    0.8324s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  183.94s  (184.90s elapsed)
  GC      time   60.02s  ( 60.13s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  244.01s  (245.06s elapsed)

  %GC     time      24.6%  (24.5% elapsed)

  Alloc rate    730,328,148 bytes per MUT second

  Productivity  75.4% of total user, 75.1% of total elapsed


real	4m5.195s
user	4m2.719s
sys	0m1.424s

-- After removing RecCheck

Finished README.
Total time          245271 ms
Parsing               1552 ms
Import                4668 ms
Deserialization         40 ms
Scoping              22497 ms
Typing               49891 ms
Termination           4844 ms
Termination.Graph      256 ms
Termination.Compare    888 ms
Positivity            4832 ms
Injectivity            628 ms
ProjectionLikeness     124 ms
Coverage              1744 ms
Highlighting          5520 ms
Serialization       145605 ms

 135,818,330,608 bytes allocated in the heap
  16,468,596,584 bytes copied during GC
     426,919,256 bytes maximum residency (43 sample(s))
       5,709,968 bytes maximum slop
            1176 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1502 colls,     0 par   44.97s   45.05s     0.0300s    0.3834s
  Gen  1        43 colls,     0 par   14.72s   14.75s     0.3429s    0.8974s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  185.57s  (185.95s elapsed)
  GC      time   59.69s  ( 59.80s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  245.29s  (245.78s elapsed)

  %GC     time      24.3%  (24.3% elapsed)

  Alloc rate    731,909,667 bytes per MUT second

  Productivity  75.7% of total user, 75.5% of total elapsed


real	4m5.918s
user	4m1.731s
sys	0m3.700s
Finished README.
Total time          243775 ms
Parsing               2236 ms
Import                4664 ms
Deserialization         24 ms
Scoping              22137 ms
Typing               50595 ms
Termination           4460 ms
Termination.Graph      288 ms
Termination.Compare    808 ms
Positivity            4696 ms
Injectivity            648 ms
ProjectionLikeness     128 ms
Coverage              1712 ms
Highlighting          5824 ms
Serialization       143376 ms

 135,835,176,176 bytes allocated in the heap
  16,490,714,152 bytes copied during GC
     426,014,240 bytes maximum residency (43 sample(s))
       5,722,440 bytes maximum slop
            1176 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1519 colls,     0 par   44.65s   44.75s     0.0295s    0.3811s
  Gen  1        43 colls,     0 par   14.68s   14.70s     0.3419s    0.8981s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  184.43s  (184.78s elapsed)
  GC      time   59.33s  ( 59.45s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  243.80s  (244.27s elapsed)

  %GC     time      24.3%  (24.3% elapsed)

  Alloc rate    736,509,487 bytes per MUT second

  Productivity  75.7% of total user, 75.5% of total elapsed


real	4m4.401s
user	4m2.587s
sys	0m1.352s

--- putting RecCheck back in

Finished README.
Total time           245663 ms
Parsing                1560 ms
Import                 4660 ms
Deserialization          44 ms
Scoping               22669 ms
Typing                52183 ms
Termination            3184 ms
Termination.Graph       176 ms
Termination.RecCheck   1672 ms
Termination.Compare     580 ms
Positivity             3840 ms
Injectivity             588 ms
ProjectionLikeness      136 ms
Coverage               2072 ms
Highlighting           5792 ms
Serialization        145669 ms

 134,321,914,096 bytes allocated in the heap
  16,557,652,048 bytes copied during GC
     398,706,344 bytes maximum residency (43 sample(s))
       5,600,760 bytes maximum slop
            1149 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1547 colls,     0 par   45.80s   45.98s     0.0297s    0.3851s
  Gen  1        43 colls,     0 par   14.86s   14.90s     0.3464s    0.8987s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  184.99s  (185.78s elapsed)
  GC      time   60.66s  ( 60.88s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  245.69s  (246.70s elapsed)

  %GC     time      24.7%  (24.7% elapsed)

  Alloc rate    726,093,554 bytes per MUT second

  Productivity  75.3% of total user, 75.0% of total elapsed


real	4m6.831s
user	4m4.203s
sys	0m1.616s


------------------------------------------------------------------------
-- With long path name

  Checking Universe (/home/abel/tmp/Agda2/stdlib-alkdsjfhalksdhfalksdjhfaklsdjhfaklsjdhfaklsdjhfaksjdhfaksjdhfaskjdfhaksdjhfaksdhfalskjdhfaiweuhrowiefosidjaflsdjfaalsdjflskdjflsjdflsjkdflskdjflskdjflskdjflskdjflsdkjflskdjflskdjfsldkjfslkdjflskdjflskdjflskdjfs/src/Universe.agda).
  Finished Universe.
 Finished Everything.
Finished README.
Total time           353206 ms
Parsing                1576 ms
Import                 4204 ms
Deserialization          24 ms
Scoping               22521 ms
Typing                50455 ms
Termination            3312 ms
Termination.Graph       208 ms
Termination.RecCheck   1860 ms
Termination.Compare     340 ms
Positivity             4248 ms
Injectivity             608 ms
ProjectionLikeness      144 ms
Coverage               1836 ms
Highlighting           6564 ms
Serialization        253635 ms
Serialization.Sort      896 ms

 133,586,214,616 bytes allocated in the heap
  16,520,741,584 bytes copied during GC
     399,520,016 bytes maximum residency (44 sample(s))
       5,143,488 bytes maximum slop
            1152 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1502 colls,     0 par   45.88s   45.97s     0.0306s    0.3860s
  Gen  1        44 colls,     0 par   14.69s   14.96s     0.3399s    0.8766s

  INIT    time    0.00s  (  0.02s elapsed)
  MUT     time  292.62s  (293.38s elapsed)
  GC      time   60.56s  ( 60.93s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  353.23s  (354.37s elapsed)

  %GC     time      17.1%  (17.2% elapsed)

  Alloc rate    456,513,019 bytes per MUT second

  Productivity  82.9% of total user, 82.6% of total elapsed


real	5m54.583s
user	5m51.534s
sys	0m1.864s


------------------------------------------------------------------------
-- With name 200 characters shorter, we save 100s on the serialization!

  Checking Universe (/home/abel/tmp/Agda2/agda-stdlib/src/Universe.agda).
  Finished Universe.
 Finished Everything.
Finished README.
Total time           245771 ms
Parsing                1492 ms
Import                 4056 ms
Deserialization          36 ms
Scoping               21973 ms
Typing                49727 ms
Termination            3164 ms
Termination.Graph       188 ms
Termination.RecCheck   1800 ms
Termination.Compare     380 ms
Positivity             4376 ms
Injectivity             616 ms
ProjectionLikeness      144 ms
Coverage               2084 ms
Highlighting           5632 ms
Serialization        149369 ms
Serialization.Sort     1660 ms

 133,064,819,520 bytes allocated in the heap
  16,531,909,328 bytes copied during GC
     428,286,528 bytes maximum residency (43 sample(s))
       5,227,824 bytes maximum slop
            1180 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1512 colls,     0 par   46.41s   46.54s     0.0308s    0.4521s
  Gen  1        43 colls,     0 par   14.93s   14.96s     0.3480s    0.8854s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  184.42s  (185.24s elapsed)
  GC      time   61.33s  ( 61.50s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  245.79s  (246.78s elapsed)

  %GC     time      25.0%  (24.9% elapsed)

  Alloc rate    721,524,696 bytes per MUT second

  Productivity  75.0% of total user, 74.7% of total elapsed


real	4m6.929s
user	4m3.339s
sys	0m2.608s

------------------------------------------------------------------------
-- 2014-03-29 After introducing FileId instead of AbsolutePath

  Checking Universe (/home/abel/tmp/Agda2/agda-stdlib/src/Universe.agda).
  Finished Universe.
 Finished Everything.
Finished README.
Total time           213677 ms
Parsing                1424 ms
Import                 3832 ms
Deserialization          36 ms
Scoping               21893 ms
Typing                50927 ms
Termination            3168 ms
Termination.Graph       168 ms
Termination.RecCheck   1660 ms
Termination.Compare     372 ms
Positivity             4276 ms
Injectivity             720 ms
ProjectionLikeness      164 ms
Coverage               1808 ms
Highlighting           5416 ms
Serialization        115539 ms
Serialization.Sort      892 ms

 130,026,213,488 bytes allocated in the heap
  16,523,023,112 bytes copied during GC
     400,507,568 bytes maximum residency (43 sample(s))
       5,147,064 bytes maximum slop
            1170 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1508 colls,     0 par   46.01s   46.19s     0.0306s    0.3979s
  Gen  1        43 colls,     0 par   15.06s   15.13s     0.3519s    0.8771s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  152.59s  (156.66s elapsed)
  GC      time   61.07s  ( 61.32s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  213.70s  (218.03s elapsed)

  %GC     time      28.6%  (28.1% elapsed)

  Alloc rate    852,103,849 bytes per MUT second

  Productivity  71.4% of total user, 70.0% of total elapsed


real	3m38.163s
user	3m29.789s
sys	0m4.056s

  Checking Universe (/home/abel/tmp/Agda2/agda-stdlib/src/Universe.agda).
  Finished Universe.
 Finished Everything.
Finished README.
Total time           212693 ms
Parsing                1464 ms
Import                 3864 ms
Deserialization          20 ms
Scoping               21777 ms
Typing                50887 ms
Termination            3036 ms
Termination.Graph       148 ms
Termination.RecCheck   1556 ms
Termination.Compare     420 ms
Positivity             4296 ms
Injectivity             584 ms
ProjectionLikeness      160 ms
Coverage               1912 ms
Highlighting           5424 ms
Serialization        114959 ms
Serialization.Sort      884 ms

 130,026,790,480 bytes allocated in the heap
  16,522,181,320 bytes copied during GC
     400,505,984 bytes maximum residency (43 sample(s))
       5,166,856 bytes maximum slop
            1170 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1507 colls,     0 par   45.79s   45.93s     0.0305s    0.3922s
  Gen  1        43 colls,     0 par   14.86s   14.90s     0.3465s    0.8798s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  152.04s  (152.60s elapsed)
  GC      time   60.65s  ( 60.83s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  212.72s  (213.46s elapsed)

  %GC     time      28.5%  (28.5% elapsed)

  Alloc rate    855,239,706 bytes per MUT second

  Productivity  71.5% of total user, 71.2% of total elapsed


real	3m33.604s
user	3m30.645s
sys	0m2.220s

  Checking Universe (/home/abel/tmp/Agda2/agda-stdlib/src/Universe.agda).
  Finished Universe.
 Finished Everything.
Finished README.
Total time           220841 ms
Parsing                1488 ms
Import                 4088 ms
Deserialization          48 ms
Scoping               21817 ms
Typing                49995 ms
Termination            2992 ms
Termination.Graph       168 ms
Termination.RecCheck   1824 ms
Termination.Compare     240 ms
Positivity             4476 ms
Injectivity             648 ms
ProjectionLikeness      172 ms
Coverage               1780 ms
Highlighting           5512 ms
Serialization        124823 ms
Serialization.Sort     1688 ms

 132,677,752,384 bytes allocated in the heap
  16,528,069,248 bytes copied during GC
     428,825,752 bytes maximum residency (43 sample(s))
       5,265,552 bytes maximum slop
            1181 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1528 colls,     0 par   46.51s   46.78s     0.0306s    0.3989s
  Gen  1        43 colls,     0 par   15.27s   15.31s     0.3560s    0.9005s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  159.06s  (165.56s elapsed)
  GC      time   61.78s  ( 62.09s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  220.87s  (227.69s elapsed)

  %GC     time      28.0%  (27.3% elapsed)

  Alloc rate    834,160,036 bytes per MUT second

  Productivity  72.0% of total user, 69.9% of total elapsed


real	3m47.836s
user	3m38.266s
sys	0m2.744s

------------------------------------------------------------------------
-- With long path name after fix of AbsolutePath to ByteString

  Checking Universe (/home/abel/tmp/Agda2/stdlib-alkdsjfhalksdhfalksdjhfaklsdjhfaklsjdhfaklsdjhfaksjdhfaksjdhfaskjdfhaksdjhfaksdhfalskjdhfaiweuhrowiefosidjaflsdjfaalsdjflskdjflsjdflsjkdflskdjflskdjflskdjflskdjflsdkjflskdjflskdjfsldkjfslkdjflskdjflskdjflskdjfs/src/Universe.agda).
  Finished Universe.
 Finished Everything.
Finished README.
Total time           222153 ms
Parsing                1464 ms
Import                 4228 ms
Deserialization          36 ms
Scoping               22601 ms
Typing                49139 ms
Termination            3040 ms
Termination.Graph       168 ms
Termination.RecCheck   1816 ms
Termination.Compare     264 ms
Positivity             4460 ms
Injectivity             624 ms
ProjectionLikeness      136 ms
Coverage               1956 ms
Highlighting           5840 ms
Serialization        125359 ms
Serialization.Sort     1688 ms

 133,264,012,992 bytes allocated in the heap
  16,515,962,536 bytes copied during GC
     428,766,200 bytes maximum residency (44 sample(s))
       5,300,328 bytes maximum slop
            1179 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1537 colls,     0 par   46.28s   46.51s     0.0303s    0.4520s
  Gen  1        44 colls,     0 par   15.25s   15.30s     0.3478s    0.9122s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  160.61s  (166.87s elapsed)
  GC      time   61.53s  ( 61.81s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  222.17s  (228.73s elapsed)

  %GC     time      27.7%  (27.0% elapsed)

  Alloc rate    829,753,070 bytes per MUT second

  Productivity  72.3% of total user, 70.2% of total elapsed


real	3m48.878s
user	3m38.730s
sys	0m3.600s


===========================================================================
2014-04-11  After instantiateFull on Definition before positivity check

Finished README.
Total time           227230 ms
Parsing                1420 ms
Import                 4412 ms
Deserialization          28 ms
Scoping               21489 ms
Typing                52759 ms
Termination            3584 ms
Termination.Graph       192 ms
Termination.RecCheck   2092 ms
Termination.Compare     284 ms
Positivity             4448 ms
Injectivity             624 ms
ProjectionLikeness      160 ms
Coverage               1620 ms
Highlighting           6024 ms
Serialization        127403 ms
Serialization.Sort      904 ms

 136,924,304,304 bytes allocated in the heap
  16,568,772,328 bytes copied during GC
     495,581,048 bytes maximum residency (43 sample(s))
       6,235,136 bytes maximum slop
            1187 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1515 colls,     0 par   47.40s   47.49s     0.0313s    0.4077s
  Gen  1        43 colls,     0 par   17.01s   17.04s     0.3964s    2.4627s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  162.81s  (163.19s elapsed)
  GC      time   64.41s  ( 64.53s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  227.26s  (227.76s elapsed)

  %GC     time      28.3%  (28.3% elapsed)

  Alloc rate    841,009,590 bytes per MUT second

  Productivity  71.7% of total user, 71.5% of total elapsed


real	3m47.920s
user	3m45.870s
sys	0m1.540s

------------------------------------------------------------------------
-- Only instantiating the type of definition is cheaper, but still noticeable

Finished README.
Total time           223001 ms
Parsing                2280 ms
Import                 4544 ms
Deserialization          40 ms
Scoping               21673 ms
Typing                49563 ms
Termination            3332 ms
Termination.Graph       212 ms
Termination.RecCheck   1916 ms
Termination.Compare     228 ms
Positivity             4332 ms
Injectivity             632 ms
ProjectionLikeness      160 ms
Coverage               1696 ms
Highlighting           5320 ms
Serialization        126419 ms
Serialization.Sort      892 ms

 136,044,962,088 bytes allocated in the heap
  16,623,561,536 bytes copied during GC
     403,880,936 bytes maximum residency (43 sample(s))
       5,203,312 bytes maximum slop
            1168 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1525 colls,     0 par   46.15s   46.25s     0.0303s    0.3887s
  Gen  1        43 colls,     0 par   14.93s   14.95s     0.3477s    0.8693s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  161.92s  (162.25s elapsed)
  GC      time   61.08s  ( 61.20s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  223.03s  (223.50s elapsed)

  %GC     time      27.4%  (27.4% elapsed)

  Alloc rate    840,219,420 bytes per MUT second

  Productivity  72.6% of total user, 72.5% of total elapsed


real	3m43.618s
user	3m41.702s
sys	0m1.452s

Finished README.
Total time           221633 ms
Parsing                1416 ms
Import                 3844 ms
Deserialization          36 ms
Scoping               22133 ms
Typing                49567 ms
Termination            3044 ms
Termination.Graph       208 ms
Termination.RecCheck   1788 ms
Termination.Compare     328 ms
Positivity             4368 ms
Injectivity             644 ms
ProjectionLikeness      140 ms
Coverage               1584 ms
Highlighting           5460 ms
Serialization        126447 ms
Serialization.Sort      872 ms

 136,054,048,576 bytes allocated in the heap
  16,651,306,312 bytes copied during GC
     403,880,776 bytes maximum residency (43 sample(s))
       5,204,248 bytes maximum slop
            1168 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1510 colls,     0 par   45.62s   45.71s     0.0303s    0.3919s
  Gen  1        43 colls,     0 par   14.92s   14.94s     0.3475s    0.9009s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  161.09s  (161.98s elapsed)
  GC      time   60.54s  ( 60.65s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  221.66s  (222.67s elapsed)

  %GC     time      27.3%  (27.2% elapsed)

  Alloc rate    844,606,506 bytes per MUT second

  Productivity  72.7% of total user, 72.4% of total elapsed


real	3m42.787s
user	3m40.450s
sys	0m1.328s

---------------------------------------------------------------------------
-- Trying: instantiateFull only in Polarity

Finished README.
Total time           223425 ms
Parsing                1404 ms
Import                 4256 ms
Deserialization          44 ms
Scoping               21209 ms
Typing                51463 ms
Termination            3772 ms
Termination.Graph       216 ms
Termination.RecCheck   1868 ms
Termination.Compare     280 ms
Positivity             4160 ms
Injectivity             608 ms
ProjectionLikeness      188 ms
Coverage               1792 ms
Highlighting           5776 ms
Serialization        125499 ms
Serialization.Sort      872 ms

 136,688,456,168 bytes allocated in the heap
  16,477,877,600 bytes copied during GC
     493,230,872 bytes maximum residency (43 sample(s))
       6,203,928 bytes maximum slop
            1183 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1515 colls,     0 par   45.74s   45.83s     0.0302s    0.4169s
  Gen  1        43 colls,     0 par   16.73s   16.75s     0.3896s    2.4386s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  160.94s  (162.44s elapsed)
  GC      time   62.47s  ( 62.58s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  223.45s  (225.05s elapsed)

  %GC     time      28.0%  (27.8% elapsed)

  Alloc rate    849,295,199 bytes per MUT second

  Productivity  72.0% of total user, 71.5% of total elapsed


real	3m45.172s
user	3m41.814s
sys	0m1.756s

Finished README.
Total time           224726 ms
Parsing                1412 ms
Import                 4324 ms
Deserialization          36 ms
Scoping               21425 ms
Typing                51635 ms
Termination            3916 ms
Termination.Graph       192 ms
Termination.RecCheck   2696 ms
Termination.Compare     232 ms
Positivity             4212 ms
Injectivity             600 ms
ProjectionLikeness      156 ms
Coverage               1924 ms
Highlighting           5828 ms
Serialization        126075 ms
Serialization.Sort      812 ms

 136,698,575,640 bytes allocated in the heap
  16,478,298,080 bytes copied during GC
     493,232,264 bytes maximum residency (43 sample(s))
       6,204,712 bytes maximum slop
            1183 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1515 colls,     0 par   45.97s   46.04s     0.0304s    0.4158s
  Gen  1        43 colls,     0 par   16.74s   16.78s     0.3902s    2.4438s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  162.00s  (162.28s elapsed)
  GC      time   62.71s  ( 62.82s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  224.75s  (225.14s elapsed)

  %GC     time      27.9%  (27.9% elapsed)

  Alloc rate    843,816,730 bytes per MUT second

  Productivity  72.1% of total user, 72.0% of total elapsed


real	3m45.256s
user	3m43.586s
sys	0m1.280s

========================================================================
2014-07-12  Try: Data.Text for names

Finished README.
Total time           223417 ms
Parsing                1836 ms
Parsing.Operators      9856 ms
Import                 4104 ms
Deserialization          28 ms
Scoping                8668 ms
Typing                50403 ms
Termination            3268 ms
Termination.Graph       172 ms
Termination.RecCheck   1824 ms
Termination.Compare     284 ms
Positivity             4456 ms
Injectivity             716 ms
ProjectionLikeness      152 ms
Coverage               1668 ms
Highlighting           4924 ms
Serialization        130248 ms
Serialization.Sort      900 ms
ModuleName               24 ms

 138,974,834,800 bytes allocated in the heap
  16,604,694,896 bytes copied during GC
     401,008,464 bytes maximum residency (43 sample(s))
       5,281,432 bytes maximum slop
            1176 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1569 colls,     0 par   46.97s   47.64s     0.0304s    0.3948s
  Gen  1        43 colls,     0 par   14.77s   14.88s     0.3461s    0.8923s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  158.89s  (161.28s elapsed)
  GC      time   61.74s  ( 62.52s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  220.67s  (223.84s elapsed)

  %GC     time      28.0%  (27.9% elapsed)

  Alloc rate    874,661,055 bytes per MUT second

  Productivity  72.0% of total user, 71.0% of total elapsed


real	3m44.031s
user	3m40.674s
sys	0m2.928s



===========================================================================

2014-09-07

Finished README.
Total time           222,833 ms
Parsing                1,276 ms
Parsing.Operators      9,888 ms
Import                 4,400 ms
Deserialization           24 ms
Scoping                8,756 ms
Typing                49,715 ms
Termination            1,796 ms
Termination.Graph        196 ms
Termination.RecCheck     532 ms
Termination.Compare      256 ms
Positivity             5,112 ms
Injectivity              844 ms
ProjectionLikeness       148 ms
Coverage               1,712 ms
Highlighting           7,600 ms
Serialization        127,731 ms
Serialization.Sort       920 ms
ModuleName                24 ms

 140,853,143,208 bytes allocated in the heap
  16,042,507,616 bytes copied during GC
     394,876,856 bytes maximum residency (42 sample(s))
       5,304,704 bytes maximum slop
            1162 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1575 colls,     0 par   45.68s   46.05s     0.0292s    0.4089s
  Gen  1        42 colls,     0 par   14.52s   14.56s     0.3467s    0.8748s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  161.28s  (163.19s elapsed)
  GC      time   60.20s  ( 60.61s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  221.52s  (223.84s elapsed)

  %GC     time      27.2%  (27.1% elapsed)

  Alloc rate    873,355,692 bytes per MUT second

  Productivity  72.8% of total user, 72.1% of total elapsed


real	3m43.962s
user	3m41.522s
sys	0m1.460s

-- after refactoring of Free into Reader monad
-- (no change expected)

Finished README.
Total time           222,437 ms
Parsing                1,284 ms
Parsing.Operators      9,580 ms
Import                 3,968 ms
Deserialization           12 ms
Scoping                9,124 ms
Typing                50,295 ms
Termination            1,944 ms
Termination.Graph        204 ms
Termination.RecCheck     484 ms
Termination.Compare      444 ms
Positivity             5,480 ms
Injectivity              760 ms
ProjectionLikeness       172 ms
Coverage               1,956 ms
Highlighting           7,148 ms
Serialization        126,827 ms
Serialization.Sort       880 ms
ModuleName                24 ms

 143,764,787,248 bytes allocated in the heap
  16,412,471,264 bytes copied during GC
     422,751,256 bytes maximum residency (43 sample(s))
       5,211,104 bytes maximum slop
            1219 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1581 colls,     0 par   44.82s   45.21s     0.0286s    0.4164s
  Gen  1        43 colls,     0 par   14.56s   14.62s     0.3400s    0.9447s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  161.80s  (163.19s elapsed)
  GC      time   59.38s  ( 59.83s elapsed)
  EXIT    time    0.02s  (  0.02s elapsed)
  Total   time  221.21s  (223.05s elapsed)

  %GC     time      26.8%  (26.8% elapsed)

  Alloc rate    888,522,381 bytes per MUT second

  Productivity  73.2% of total user, 72.6% of total elapsed


real	3m43.157s
user	3m41.210s
sys	0m1.356s

-- After not returning bound variables in Free Finished Everything.

Finished README.
Total time           221,953 ms
Parsing                1,260 ms
Parsing.Operators      9,560 ms
Import                 4,092 ms
Deserialization           24 ms
Scoping                8,972 ms
Typing                49,899 ms
Termination            2,804 ms
Termination.Graph        208 ms
Termination.RecCheck   1,356 ms
Termination.Compare      476 ms
Positivity             5,352 ms
Injectivity              808 ms
ProjectionLikeness       156 ms
Coverage               1,920 ms
Highlighting           6,220 ms
Serialization        127,075 ms
Serialization.Sort       908 ms
ModuleName                24 ms

 143,466,267,472 bytes allocated in the heap
  16,419,616,000 bytes copied during GC
     422,751,184 bytes maximum residency (43 sample(s))
       5,215,864 bytes maximum slop
            1219 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1580 colls,     0 par   45.04s   45.47s     0.0288s    0.4112s
  Gen  1        43 colls,     0 par   14.60s   14.64s     0.3405s    0.9250s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  161.00s  (163.61s elapsed)
  GC      time   59.64s  ( 60.12s elapsed)
  EXIT    time    0.03s  (  0.02s elapsed)
  Total   time  220.68s  (223.76s elapsed)

  %GC     time      27.0%  (26.9% elapsed)

  Alloc rate    891,105,632 bytes per MUT second

  Productivity  73.0% of total user, 72.0% of total elapsed


real	3m43.882s
user	3m40.678s
sys	0m1.420s

-- With strict context (Int)

Finished README.
Total time           221,545 ms
Parsing                1,264 ms
Parsing.Operators      9,628 ms
Import                 4,028 ms
Deserialization           24 ms
Scoping                8,676 ms
Typing                49,915 ms
Termination            2,556 ms
Termination.Graph        228 ms
Termination.RecCheck   1,192 ms
Termination.Compare      340 ms
Positivity             5,416 ms
Injectivity              752 ms
ProjectionLikeness       152 ms
Coverage               1,992 ms
Highlighting           6,416 ms
Serialization        126,939 ms
Serialization.Sort       880 ms
ModuleName                24 ms

 143,445,608,864 bytes allocated in the heap
  16,418,682,328 bytes copied during GC
     422,751,112 bytes maximum residency (43 sample(s))
       5,227,832 bytes maximum slop
            1219 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1580 colls,     0 par   45.09s   45.44s     0.0288s    0.4103s
  Gen  1        43 colls,     0 par   14.59s   14.65s     0.3407s    0.9078s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  160.44s  (161.78s elapsed)
  GC      time   59.68s  ( 60.10s elapsed)
  EXIT    time    0.02s  (  0.02s elapsed)
  Total   time  220.15s  (221.91s elapsed)

  %GC     time      27.1%  (27.1% elapsed)

  Alloc rate    894,087,368 bytes per MUT second

  Productivity  72.9% of total user, 72.3% of total elapsed


real	3m42.026s
user	3m40.154s
sys	0m1.528s
Finished README.
Total time           220,913 ms
Parsing                1,288 ms
Parsing.Operators      9,524 ms
Import                 3,996 ms
Deserialization            8 ms
Scoping                8,904 ms
Typing                49,991 ms
Termination            2,596 ms
Termination.Graph        344 ms
Termination.RecCheck   1,220 ms
Termination.Compare      376 ms
Positivity             5,380 ms
Injectivity              716 ms
ProjectionLikeness       216 ms
Coverage               1,952 ms
Highlighting           6,216 ms
Serialization        126,319 ms
Serialization.Sort       940 ms
ModuleName                24 ms

 143,445,608,312 bytes allocated in the heap
  16,418,927,200 bytes copied during GC
     422,751,160 bytes maximum residency (43 sample(s))
       5,213,904 bytes maximum slop
            1219 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1580 colls,     0 par   44.51s   44.87s     0.0284s    0.4063s
  Gen  1        43 colls,     0 par   14.48s   14.55s     0.3384s    0.8998s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  160.61s  (161.86s elapsed)
  GC      time   58.98s  ( 59.42s elapsed)
  EXIT    time    0.02s  (  0.02s elapsed)
  Total   time  219.62s  (221.31s elapsed)

  %GC     time      26.9%  (26.8% elapsed)

  Alloc rate    893,152,020 bytes per MUT second

  Productivity  73.1% of total user, 72.6% of total elapsed


real	3m41.409s
user	3m39.622s
sys	0m1.416s



2014-10-16 AIM XX

Huffman-only compression increases .agdai size by 30% but saves > 50 %
of compression time.  (5 sec on std-lib).

 Finished Everything.
Finished README.
Total time                 215,597ms
Parsing                      1,304ms
Parsing.Operators           10,452ms
Import                       5,800ms
Deserialization                 36ms
Scoping                      9,020ms
Typing                      50,631ms
Termination                  1,828ms
Termination.Graph              216ms
Termination.RecCheck           496ms
Termination.Compare            228ms
Positivity                   4,548ms
Injectivity                    752ms
ProjectionLikeness             148ms
Coverage                     2,200ms
Highlighting                 6,368ms
Serialization               95,829ms
Serialization.Sort             964ms
Serialization.BinaryEncode  17,509ms
Serialization.Compress       4,280ms
ModuleName                      24ms

 143,280,163,896 bytes allocated in the heap
  16,076,672,192 bytes copied during GC
     421,917,664 bytes maximum residency (44 sample(s))
       6,044,976 bytes maximum slop
            1218 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1854 colls,     0 par   45.51s   46.04s     0.0248s    0.4052s
  Gen  1        44 colls,     0 par   14.10s   14.24s     0.3237s    0.8752s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  153.36s  (156.31s elapsed)
  GC      time   59.61s  ( 60.28s elapsed)
  EXIT    time    0.02s  (  0.03s elapsed)
  Total   time  213.01s  (216.63s elapsed)

  %GC     time      28.0%  (27.8% elapsed)

  Alloc rate    934,263,561 bytes per MUT second

  Productivity  72.0% of total user, 70.8% of total elapsed


real	3m36.724s
user	3m33.005s
sys	0m2.716s


After specializing icodeX to Integer, String, Double, Node.
------------------------------------------------------------------------

  Finished Universe.
 Finished Everything.
Finished README.
Total time                 215,509ms
Parsing                      1,292ms
Parsing.Operators           10,916ms
Import                       4,088ms
Deserialization                 20ms
Scoping                      8,684ms
Typing                      50,087ms
Termination                  1,844ms
Termination.Graph              216ms
Termination.RecCheck           508ms
Termination.Compare            348ms
Positivity                   5,132ms
Injectivity                    732ms
ProjectionLikeness             160ms
Coverage                     2,288ms
Highlighting                 7,092ms
Serialization               97,366ms
Serialization.Sort           1,200ms
Serialization.BinaryEncode  18,557ms
Serialization.Compress       4,132ms
ModuleName                      24ms

 138,864,328,792 bytes allocated in the heap
  16,214,969,216 bytes copied during GC
     479,648,664 bytes maximum residency (45 sample(s))
       5,928,496 bytes maximum slop
            1171 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1663 colls,     0 par   45.62s   46.22s     0.0278s    0.4175s
  Gen  1        45 colls,     0 par   14.44s   14.54s     0.3230s    1.0345s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  152.37s  (155.12s elapsed)
  GC      time   60.06s  ( 60.76s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  212.47s  (215.92s elapsed)

  %GC     time      28.3%  (28.1% elapsed)

  Alloc rate    911,365,449 bytes per MUT second

  Productivity  71.7% of total user, 70.6% of total elapsed


real	3m36.018s
user	3m32.469s
sys	0m3.168s


After INLINE icode<nn>[']
------------------------------------------------------------------------
Finished README.
Total time                 215,789ms
Parsing                      1,292ms
Parsing.Operators           10,440ms
Import                       4,228ms
Deserialization                 28ms
Scoping                      8,948ms
Typing                      50,175ms
Termination                  2,048ms
Termination.Graph              208ms
Termination.RecCheck           432ms
Termination.Compare            428ms
Positivity                   4,328ms
Injectivity                    744ms
ProjectionLikeness             160ms
Coverage                     2,312ms
Highlighting                 7,464ms
Serialization               96,422ms
Serialization.Sort             944ms
Serialization.BinaryEncode  19,589ms
Serialization.Compress       3,856ms
ModuleName                      24ms

 141,379,633,872 bytes allocated in the heap
  16,330,082,400 bytes copied during GC
     448,454,176 bytes maximum residency (45 sample(s))
       6,032,632 bytes maximum slop
            1163 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1666 colls,     0 par   45.15s   45.63s     0.0274s    0.4114s
  Gen  1        45 colls,     0 par   14.32s   14.35s     0.3189s    0.9113s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  155.12s  (156.34s elapsed)
  GC      time   59.47s  ( 59.98s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  214.63s  (216.36s elapsed)

  %GC     time      27.7%  (27.7% elapsed)

  Alloc rate    911,434,673 bytes per MUT second

  Productivity  72.3% of total user, 71.7% of total elapsed


real	3m36.457s
user	3m34.629s
sys	0m1.292s


After removing -O2  (but reverting INLINE icode)
------------------------------------------------------------------------
Finished README.
Total time                 214,393ms
Parsing                      1,268ms
Parsing.Operators           11,148ms
Import                       3,964ms
Deserialization                 28ms
Scoping                      8,812ms
Typing                      50,215ms
Termination                  1,816ms
Termination.Graph              212ms
Termination.RecCheck           528ms
Termination.Compare            376ms
Positivity                   4,324ms
Injectivity                    764ms
ProjectionLikeness             160ms
Coverage                     2,344ms
Highlighting                 7,008ms
Serialization               96,814ms
Serialization.Sort           1,140ms
Serialization.BinaryEncode  18,589ms
Serialization.Compress       4,036ms
ModuleName                      24ms

 140,104,546,568 bytes allocated in the heap
  16,220,714,584 bytes copied during GC
     479,648,656 bytes maximum residency (45 sample(s))
       5,905,712 bytes maximum slop
            1189 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1662 colls,     0 par   45.35s   45.65s     0.0275s    0.4145s
  Gen  1        45 colls,     0 par   14.36s   14.44s     0.3209s    1.0499s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  153.34s  (154.68s elapsed)
  GC      time   59.71s  ( 60.09s elapsed)
  EXIT    time    0.03s  (  0.03s elapsed)
  Total   time  213.09s  (214.81s elapsed)

  %GC     time      28.0%  (28.0% elapsed)

  Alloc rate    913,699,986 bytes per MUT second

  Productivity  72.0% of total user, 71.4% of total elapsed


real	3m34.906s
user	3m33.085s
sys	0m1.436s


2014-10-18 Hashmap reuse statistics for Serialize.

======================================================================
========================== Standard library ==========================
======================================================================
Ticks for Agda.Primitive
Double  (fresh)         0
Double (reused)         0
Integer  (fresh)      148
Integer (reused)      321
Node  (fresh)         401
Node (reused)        3584
String  (fresh)        21
String (reused)       785
max-open-constraints    0
max-open-metas          1
metas                   5
pointers  (fresh)       0
pointers (reused)       0

Checking README (/home/abel/agda/agda-stdlib/README.agda).
 Checking Data.Bool (/home/abel/agda/agda-stdlib/src/Data/Bool.agda).
  Checking Function (/home/abel/agda/agda-stdlib/src/Function.agda).
   Checking Level (/home/abel/agda/agda-stdlib/src/Level.agda).
Ticks for Level
Double  (fresh)         0
Double (reused)         0
Integer  (fresh)      113
Integer (reused)      632
Node  (fresh)         640
Node (reused)        7028
String  (fresh)        17
String (reused)      1117
max-open-constraints    0
max-open-metas          4
metas                   5
pointers  (fresh)       0
pointers (reused)       0

   Finished Level.
Ticks for Function
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)       1446
Integer (reused)       2404
Node  (fresh)          4297
Node (reused)         29099
String  (fresh)          61
String (reused)        3466
attempted-constraints     3
max-open-constraints      1
max-open-metas           10
metas                   170
pointers  (fresh)         0
pointers (reused)         0

  Finished Function.
  Checking Data.Unit (/home/abel/agda/agda-stdlib/src/Data/Unit.agda).
   Checking Data.Sum (/home/abel/agda/agda-stdlib/src/Data/Sum.agda).
    Checking Data.Maybe.Core (/home/abel/agda/agda-stdlib/src/Data/Maybe/Core.agda).
Ticks for Data.Maybe.Core
Double  (fresh)         0
Double (reused)         0
Integer  (fresh)      103
Integer (reused)      754
Node  (fresh)         604
Node (reused)        7843
String  (fresh)        25
String (reused)      2198
max-open-constraints    0
max-open-metas          2
metas                   7
pointers  (fresh)       0
pointers (reused)       0

    Finished Data.Maybe.Core.
Ticks for Data.Sum
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        804
Integer (reused)       3369
Node  (fresh)          3662
Node (reused)         38848
String  (fresh)          83
String (reused)        8084
attempted-constraints    36
max-open-constraints      8
max-open-metas           18
metas                   145
pointers  (fresh)         0
pointers (reused)         0

   Finished Data.Sum.
   Checking Relation.Nullary (/home/abel/agda/agda-stdlib/src/Relation/Nullary.agda).
    Checking Relation.Nullary.Core (/home/abel/agda/agda-stdlib/src/Relation/Nullary/Core.agda).
     Checking Data.Empty (/home/abel/agda/agda-stdlib/src/Data/Empty.agda).
Ticks for Data.Empty
Double  (fresh)         0
Double (reused)         0
Integer  (fresh)       92
Integer (reused)      414
Node  (fresh)         565
Node (reused)        4901
String  (fresh)        21
String (reused)      1017
max-open-constraints    0
max-open-metas          2
metas                   4
pointers  (fresh)       0
pointers (reused)       0

     Finished Data.Empty.
Ticks for Relation.Nullary.Core
Double  (fresh)          0
Double (reused)          0
Integer  (fresh)       154
Integer (reused)       975
Node  (fresh)          867
Node (reused)        10337
String  (fresh)         30
String (reused)       2890
max-open-constraints     0
max-open-metas           2
metas                   13
pointers  (fresh)        0
pointers (reused)        0

    Finished Relation.Nullary.Core.
Ticks for Relation.Nullary
Double  (fresh)         0
Double (reused)         0
Integer  (fresh)       72
Integer (reused)      309
Node  (fresh)         311
Node (reused)        3448
String  (fresh)         8
String (reused)      1111
max-open-constraints    0
metas                   0
pointers  (fresh)       0
pointers (reused)       0

   Finished Relation.Nullary.
   Checking Relation.Binary (/home/abel/agda/agda-stdlib/src/Relation/Binary.agda).
    Checking Data.Product (/home/abel/agda/agda-stdlib/src/Data/Product.agda).
Ticks for Data.Product
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)       1918
Integer (reused)       6345
Node  (fresh)          6970
Node (reused)         68703
String  (fresh)         116
String (reused)       12578
attempted-constraints    33
max-open-constraints      3
max-open-metas           12
metas                   298
pointers  (fresh)         0
pointers (reused)         0

    Finished Data.Product.
    Checking Relation.Binary.PropositionalEquality.Core (/home/abel/agda/agda-stdlib/src/Relation/Binary/PropositionalEquality/Core.agda).
     Checking Relation.Binary.Core (/home/abel/agda/agda-stdlib/src/Relation/Binary/Core.agda).
Ticks for Relation.Binary.Core
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2528
Integer (reused)       12345
Node  (fresh)           9562
Node (reused)         128774
String  (fresh)          165
String (reused)        30975
attempted-constraints     51
max-open-constraints       2
max-open-metas            15
metas                    506
pointers  (fresh)          0
pointers (reused)          0

     Finished Relation.Binary.Core.
     Checking Relation.Binary.Consequences.Core (/home/abel/agda/agda-stdlib/src/Relation/Binary/Consequences/Core.agda).
Ticks for Relation.Binary.Consequences.Core
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        253
Integer (reused)       2164
Node  (fresh)          1995
Node (reused)         25018
String  (fresh)          89
String (reused)        8810
attempted-constraints     6
max-open-constraints      2
max-open-metas            6
metas                    23
pointers  (fresh)         0
pointers (reused)         0

     Finished Relation.Binary.Consequences.Core.
Ticks for Relation.Binary.PropositionalEquality.Core
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        371
Integer (reused)       2976
Node  (fresh)          2622
Node (reused)         33261
String  (fresh)          85
String (reused)       11678
attempted-constraints    14
max-open-constraints      5
max-open-metas            7
metas                    60
pointers  (fresh)         0
pointers (reused)         0

    Finished Relation.Binary.PropositionalEquality.Core.
    Checking Relation.Binary.Consequences (/home/abel/agda/agda-stdlib/src/Relation/Binary/Consequences.agda).
Ticks for Relation.Binary.Consequences
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1646
Integer (reused)       12803
Node  (fresh)           9881
Node (reused)         144923
String  (fresh)          199
String (reused)        35712
attempted-constraints    124
max-open-constraints       6
max-open-metas            10
metas                    394
pointers  (fresh)          0
pointers (reused)          0

    Finished Relation.Binary.Consequences.
    Checking Relation.Binary.Indexed.Core (/home/abel/agda/agda-stdlib/src/Relation/Binary/Indexed/Core.agda).
Ticks for Relation.Binary.Indexed.Core
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        812
Integer (reused)       9050
Node  (fresh)          4853
Node (reused)         88668
String  (fresh)         111
String (reused)       28380
attempted-constraints    38
max-open-constraints      4
max-open-metas           19
metas                   182
pointers  (fresh)         0
pointers (reused)         0

    Finished Relation.Binary.Indexed.Core.
Ticks for Relation.Binary
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         3422
Integer (reused)       177876
Node  (fresh)           37023
Node (reused)         1737401
String  (fresh)           218
String (reused)        380321
attempted-constraints     189
max-open-constraints        6
max-open-metas             11
metas                     675
pointers  (fresh)           0
pointers (reused)           0

   Finished Relation.Binary.
   Checking Relation.Binary.PropositionalEquality (/home/abel/agda/agda-stdlib/src/Relation/Binary/PropositionalEquality.agda).
    Checking Function.Equality (/home/abel/agda/agda-stdlib/src/Function/Equality.agda).
     Checking Relation.Binary.Indexed (/home/abel/agda/agda-stdlib/src/Relation/Binary/Indexed.agda).
Ticks for Relation.Binary.Indexed
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         615
Integer (reused)       12140
Node  (fresh)           6943
Node (reused)         120483
String  (fresh)          136
String (reused)        35203
attempted-constraints      4
max-open-constraints       2
max-open-metas             8
metas                     56
pointers  (fresh)          0
pointers (reused)          0

     Finished Relation.Binary.Indexed.
Ticks for Function.Equality
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1626
Integer (reused)       24131
Node  (fresh)          11804
Node (reused)         241359
String  (fresh)          198
String (reused)        61572
attempted-constraints     61
max-open-constraints       2
max-open-metas            12
metas                    365
pointers  (fresh)          0
pointers (reused)          0

    Finished Function.Equality.
    Checking Data.Unit.Core (/home/abel/agda/agda-stdlib/src/Data/Unit/Core.agda).
Ticks for Data.Unit.Core
Double  (fresh)          0
Double (reused)          0
Integer  (fresh)       243
Integer (reused)       993
Node  (fresh)         1095
Node (reused)        10564
String  (fresh)         31
String (reused)       2818
max-open-constraints     0
max-open-metas           4
metas                   20
pointers  (fresh)        0
pointers (reused)        0

    Finished Data.Unit.Core.
    Checking Relation.Binary.HeterogeneousEquality.Core (/home/abel/agda/agda-stdlib/src/Relation/Binary/HeterogeneousEquality/Core.agda).
Ticks for Relation.Binary.HeterogeneousEquality.Core
Double  (fresh)          0
Double (reused)          0
Integer  (fresh)       210
Integer (reused)      1635
Node  (fresh)         1363
Node (reused)        17180
String  (fresh)         58
String (reused)       6668
max-open-constraints     0
max-open-metas           3
metas                   18
pointers  (fresh)        0
pointers (reused)        0

    Finished Relation.Binary.HeterogeneousEquality.Core.
    Checking Relation.Binary.EqReasoning (/home/abel/agda/agda-stdlib/src/Relation/Binary/EqReasoning.agda).
     Checking Relation.Binary.PreorderReasoning (/home/abel/agda/agda-stdlib/src/Relation/Binary/PreorderReasoning.agda).
Ticks for Relation.Binary.PreorderReasoning
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         755
Integer (reused)       14786
Node  (fresh)           7539
Node (reused)         151785
String  (fresh)          129
String (reused)        41014
attempted-constraints      1
max-open-constraints       1
max-open-metas             7
metas                     55
pointers  (fresh)          0
pointers (reused)          0

     Finished Relation.Binary.PreorderReasoning.
Ticks for Relation.Binary.EqReasoning
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         493
Integer (reused)       14443
Node  (fresh)           7078
Node (reused)         146178
String  (fresh)          127
String (reused)        40311
attempted-constraints      2
max-open-constraints       1
max-open-metas             5
metas                     10
pointers  (fresh)          0
pointers (reused)          0

    Finished Relation.Binary.EqReasoning.
Ticks for Relation.Binary.PropositionalEquality
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2518
Integer (reused)       29483
Node  (fresh)          16946
Node (reused)         304975
String  (fresh)          287
String (reused)        85968
attempted-constraints     38
max-open-constraints       4
max-open-metas            24
metas                    430
pointers  (fresh)          0
pointers (reused)          0

   Finished Relation.Binary.PropositionalEquality.
Ticks for Data.Unit
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         807
Integer (reused)       12883
Node  (fresh)           8067
Node (reused)         132872
String  (fresh)          177
String (reused)        36784
attempted-constraints     13
max-open-constraints       2
max-open-metas            10
metas                     61
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Unit.
Ticks for Data.Bool
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         833
Integer (reused)       13051
Node  (fresh)           9241
Node (reused)         137428
String  (fresh)          216
String (reused)        37958
attempted-constraints      3
max-open-constraints       2
max-open-metas             6
metas                     32
pointers  (fresh)          0
pointers (reused)          0

 Finished Data.Bool.
 Checking Data.Char (/home/abel/agda/agda-stdlib/src/Data/Char.agda).
  Checking Data.Nat (/home/abel/agda/agda-stdlib/src/Data/Nat.agda).
   Checking Function.Injection (/home/abel/agda/agda-stdlib/src/Function/Injection.agda).
Ticks for Function.Injection
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         885
Integer (reused)       20631
Node  (fresh)          10841
Node (reused)         207665
String  (fresh)          245
String (reused)        49707
attempted-constraints     28
max-open-constraints       1
max-open-metas            15
metas                    173
pointers  (fresh)          0
pointers (reused)          0

   Finished Function.Injection.
   Checking Relation.Nullary.Decidable (/home/abel/agda/agda-stdlib/src/Relation/Nullary/Decidable.agda).
    Checking Function.Equivalence (/home/abel/agda/agda-stdlib/src/Function/Equivalence.agda).
Ticks for Function.Equivalence
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1574
Integer (reused)       19780
Node  (fresh)          12191
Node (reused)         199851
String  (fresh)          279
String (reused)        47088
attempted-constraints     93
max-open-constraints       4
max-open-metas            22
metas                    390
pointers  (fresh)          0
pointers (reused)          0

    Finished Function.Equivalence.
Ticks for Relation.Nullary.Decidable
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1628
Integer (reused)       24650
Node  (fresh)          14821
Node (reused)         254833
String  (fresh)          286
String (reused)        67793
attempted-constraints     29
max-open-constraints       2
max-open-metas            14
metas                    241
pointers  (fresh)          0
pointers (reused)          0

   Finished Relation.Nullary.Decidable.
   Checking Relation.Binary.PartialOrderReasoning (/home/abel/agda/agda-stdlib/src/Relation/Binary/PartialOrderReasoning.agda).
Ticks for Relation.Binary.PartialOrderReasoning
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         439
Integer (reused)       16848
Node  (fresh)           7440
Node (reused)         167044
String  (fresh)          125
String (reused)        45258
attempted-constraints      2
max-open-constraints       1
max-open-metas             7
metas                     13
pointers  (fresh)          0
pointers (reused)          0

   Finished Relation.Binary.PartialOrderReasoning.
Ticks for Data.Nat
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2707
Integer (reused)       32718
Node  (fresh)          19504
Node (reused)         357379
String  (fresh)          310
String (reused)        94880
attempted-constraints     21
max-open-constraints       3
max-open-metas            12
metas                    246
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Nat.
  Checking Data.Nat.Properties (/home/abel/agda/agda-stdlib/src/Data/Nat/Properties.agda).
   Checking Algebra (/home/abel/agda/agda-stdlib/src/Algebra.agda).
    Checking Algebra.FunctionProperties (/home/abel/agda/agda-stdlib/src/Algebra/FunctionProperties.agda).
     Checking Algebra.FunctionProperties.Core (/home/abel/agda/agda-stdlib/src/Algebra/FunctionProperties/Core.agda).
Ticks for Algebra.FunctionProperties.Core
Double  (fresh)         0
Double (reused)         0
Integer  (fresh)      120
Integer (reused)      411
Node  (fresh)         594
Node (reused)        4956
String  (fresh)        21
String (reused)      1183
max-open-constraints    0
max-open-metas          2
metas                   9
pointers  (fresh)       0
pointers (reused)       0

     Finished Algebra.FunctionProperties.Core.
Ticks for Algebra.FunctionProperties
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)       1416
Integer (reused)      13196
Node  (fresh)          9196
Node (reused)        142228
String  (fresh)         182
String (reused)       35158
max-open-constraints      0
max-open-metas            8
metas                   160
pointers  (fresh)         0
pointers (reused)         0

    Finished Algebra.FunctionProperties.
    Checking Algebra.Structures (/home/abel/agda/agda-stdlib/src/Algebra/Structures.agda).
Ticks for Algebra.Structures
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         4798
Integer (reused)       392229
Node  (fresh)           74532
Node (reused)         4026413
String  (fresh)           299
String (reused)        784917
attempted-constraints     224
max-open-constraints        2
max-open-metas             25
metas                     894
pointers  (fresh)           0
pointers (reused)           0

    Finished Algebra.Structures.
Ticks for Algebra
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         4004
Integer (reused)       310641
Node  (fresh)           64410
Node (reused)         3195439
String  (fresh)           301
String (reused)        501421
attempted-constraints      93
max-open-constraints        2
max-open-metas              9
metas                     606
pointers  (fresh)           0
pointers (reused)           0

   Finished Algebra.
   Checking Data.Nat.Properties.Simple (/home/abel/agda/agda-stdlib/src/Data/Nat/Properties/Simple.agda).
Ticks for Data.Nat.Properties.Simple
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1477
Integer (reused)       19823
Node  (fresh)          10097
Node (reused)         230988
String  (fresh)          172
String (reused)        68018
attempted-constraints      4
max-open-constraints       1
max-open-metas            19
metas                    301
pointers  (fresh)          0
pointers (reused)          0

   Finished Data.Nat.Properties.Simple.
   Checking Algebra.RingSolver.Simple (/home/abel/agda/agda-stdlib/src/Algebra/RingSolver/Simple.agda).
    Checking Algebra.RingSolver.AlmostCommutativeRing (/home/abel/agda/agda-stdlib/src/Algebra/RingSolver/AlmostCommutativeRing.agda).
     Checking Algebra.Morphism (/home/abel/agda/agda-stdlib/src/Algebra/Morphism.agda).
      Checking Algebra.Properties.Group (/home/abel/agda/agda-stdlib/src/Algebra/Properties/Group.agda).
Ticks for Algebra.Properties.Group
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1389
Integer (reused)       40802
Node  (fresh)          16619
Node (reused)         411480
String  (fresh)          265
String (reused)        87907
attempted-constraints     32
max-open-constraints       2
max-open-metas            18
metas                    273
pointers  (fresh)          0
pointers (reused)          0

      Finished Algebra.Properties.Group.
Ticks for Algebra.Morphism
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1316
Integer (reused)       90433
Node  (fresh)          31024
Node (reused)         958395
String  (fresh)          372
String (reused)       170683
attempted-constraints     18
max-open-constraints       2
max-open-metas            11
metas                    109
pointers  (fresh)          0
pointers (reused)          0

     Finished Algebra.Morphism.
     Checking Algebra.Properties.Ring (/home/abel/agda/agda-stdlib/src/Algebra/Properties/Ring.agda).
      Checking Algebra.Properties.AbelianGroup (/home/abel/agda/agda-stdlib/src/Algebra/Properties/AbelianGroup.agda).
Ticks for Algebra.Properties.AbelianGroup
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1019
Integer (reused)       37672
Node  (fresh)          14641
Node (reused)         379071
String  (fresh)          247
String (reused)        81412
attempted-constraints     20
max-open-constraints       2
max-open-metas            20
metas                    163
pointers  (fresh)          0
pointers (reused)          0

      Finished Algebra.Properties.AbelianGroup.
Ticks for Algebra.Properties.Ring
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1280
Integer (reused)       51742
Node  (fresh)          16598
Node (reused)         521914
String  (fresh)          257
String (reused)       108464
attempted-constraints     38
max-open-constraints       2
max-open-metas            25
metas                    259
pointers  (fresh)          0
pointers (reused)          0

     Finished Algebra.Properties.Ring.
Ticks for Algebra.RingSolver.AlmostCommutativeRing
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         1979
Integer (reused)       242043
Node  (fresh)           48163
Node (reused)         2354025
String  (fresh)           373
String (reused)        589968
attempted-constraints      31
max-open-constraints        2
max-open-metas              9
metas                     195
pointers  (fresh)           0
pointers (reused)           0

    Finished Algebra.RingSolver.AlmostCommutativeRing.
    Checking Algebra.RingSolver (/home/abel/agda/agda-stdlib/src/Algebra/RingSolver.agda).
     Checking Algebra.RingSolver.Lemmas (/home/abel/agda/agda-stdlib/src/Algebra/RingSolver/Lemmas.agda).
Ticks for Algebra.RingSolver.Lemmas
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         2953
Integer (reused)       114152
Node  (fresh)           29708
Node (reused)         1262930
String  (fresh)           290
String (reused)        332679
attempted-constraints      84
max-open-constraints        2
max-open-metas             29
metas                     712
pointers  (fresh)           0
pointers (reused)           0

     Finished Algebra.RingSolver.Lemmas.
     Checking Algebra.Operations (/home/abel/agda/agda-stdlib/src/Algebra/Operations.agda).
Ticks for Algebra.Operations
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2472
Integer (reused)       56863
Node  (fresh)          27466
Node (reused)         607394
String  (fresh)          410
String (reused)       125822
attempted-constraints     51
max-open-constraints       2
max-open-metas            16
metas                    347
pointers  (fresh)          0
pointers (reused)          0

     Finished Algebra.Operations.
     Checking Relation.Binary.Reflection (/home/abel/agda/agda-stdlib/src/Relation/Binary/Reflection.agda).
      Checking Data.Fin (/home/abel/agda/agda-stdlib/src/Data/Fin.agda).
Ticks for Data.Fin
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2657
Integer (reused)       25557
Node  (fresh)          17474
Node (reused)         277544
String  (fresh)          251
String (reused)        67764
attempted-constraints      8
max-open-constraints       2
max-open-metas             8
metas                    283
pointers  (fresh)          0
pointers (reused)          0

      Finished Data.Fin.
      Checking Data.Vec (/home/abel/agda/agda-stdlib/src/Data/Vec.agda).
       Checking Category.Applicative (/home/abel/agda/agda-stdlib/src/Category/Applicative.agda).
        Checking Category.Applicative.Indexed (/home/abel/agda/agda-stdlib/src/Category/Applicative/Indexed.agda).
         Checking Category.Functor (/home/abel/agda/agda-stdlib/src/Category/Functor.agda).
Ticks for Category.Functor
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        182
Integer (reused)       1110
Node  (fresh)          1432
Node (reused)         13651
String  (fresh)          50
String (reused)        2584
attempted-constraints     1
max-open-constraints      1
max-open-metas            6
metas                    26
pointers  (fresh)         0
pointers (reused)         0

         Finished Category.Functor.
Ticks for Category.Applicative.Indexed
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1191
Integer (reused)       23919
Node  (fresh)          10985
Node (reused)         276699
String  (fresh)          171
String (reused)        62976
attempted-constraints     43
max-open-constraints       2
max-open-metas            19
metas                    363
pointers  (fresh)          0
pointers (reused)          0

        Finished Category.Applicative.Indexed.
Ticks for Category.Applicative
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        197
Integer (reused)       4038
Node  (fresh)          2570
Node (reused)         44109
String  (fresh)          61
String (reused)       11613
attempted-constraints     1
max-open-constraints      1
max-open-metas            4
metas                    13
pointers  (fresh)         0
pointers (reused)         0

       Finished Category.Applicative.
       Checking Data.List (/home/abel/agda/agda-stdlib/src/Data/List.agda).
        Checking Data.Maybe (/home/abel/agda/agda-stdlib/src/Data/Maybe.agda).
         Checking Category.Monad (/home/abel/agda/agda-stdlib/src/Category/Monad.agda).
          Checking Category.Monad.Indexed (/home/abel/agda/agda-stdlib/src/Category/Monad/Indexed.agda).
Ticks for Category.Monad.Indexed
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         942
Integer (reused)       23734
Node  (fresh)           7917
Node (reused)         254070
String  (fresh)          112
String (reused)        65234
attempted-constraints     12
max-open-constraints       2
max-open-metas            12
metas                    203
pointers  (fresh)          0
pointers (reused)          0

          Finished Category.Monad.Indexed.
Ticks for Category.Monad
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         476
Integer (reused)       18608
Node  (fresh)           6295
Node (reused)         200302
String  (fresh)           90
String (reused)        48895
attempted-constraints      3
max-open-constraints       1
max-open-metas             4
metas                     39
pointers  (fresh)          0
pointers (reused)          0

         Finished Category.Monad.
         Checking Category.Monad.Identity (/home/abel/agda/agda-stdlib/src/Category/Monad/Identity.agda).
Ticks for Category.Monad.Identity
Double  (fresh)          0
Double (reused)          0
Integer  (fresh)       188
Integer (reused)      1734
Node  (fresh)         1423
Node (reused)        18997
String  (fresh)         53
String (reused)       6111
max-open-constraints     0
max-open-metas           4
metas                    6
pointers  (fresh)        0
pointers (reused)        0

         Finished Category.Monad.Identity.
         Checking Relation.Unary (/home/abel/agda/agda-stdlib/src/Relation/Unary.agda).
Ticks for Relation.Unary
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2688
Integer (reused)       19411
Node  (fresh)          15164
Node (reused)         207444
String  (fresh)          253
String (reused)        47682
attempted-constraints     86
max-open-constraints       5
max-open-metas            20
metas                    540
pointers  (fresh)          0
pointers (reused)          0

         Finished Relation.Unary.
Ticks for Data.Maybe
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2771
Integer (reused)       35116
Node  (fresh)          21349
Node (reused)         359768
String  (fresh)          329
String (reused)        87586
attempted-constraints     90
max-open-constraints       4
max-open-metas            14
metas                    433
pointers  (fresh)          0
pointers (reused)          0

        Finished Data.Maybe.
Ticks for Data.List
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        4694
Integer (reused)       48208
Node  (fresh)          33356
Node (reused)         517450
String  (fresh)          496
String (reused)       114226
attempted-constraints     53
max-open-constraints       7
max-open-metas            10
metas                    669
pointers  (fresh)          0
pointers (reused)          0

       Finished Data.List.
Ticks for Data.Vec
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        4148
Integer (reused)       28736
Node  (fresh)          21480
Node (reused)         329244
String  (fresh)          313
String (reused)        74542
attempted-constraints     41
max-open-constraints       4
max-open-metas            13
metas                    734
pointers  (fresh)          0
pointers (reused)          0

      Finished Data.Vec.
      Checking Data.Vec.N-ary (/home/abel/agda/agda-stdlib/src/Data/Vec/N-ary.agda).
Ticks for Data.Vec.N-ary
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        3460
Integer (reused)       32381
Node  (fresh)          21834
Node (reused)         352370
String  (fresh)          351
String (reused)        90959
attempted-constraints    194
max-open-constraints       9
max-open-metas            15
metas                    768
pointers  (fresh)          0
pointers (reused)          0

      Finished Data.Vec.N-ary.
Ticks for Relation.Binary.Reflection
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1469
Integer (reused)       35657
Node  (fresh)          16611
Node (reused)         396744
String  (fresh)          362
String (reused)        94361
attempted-constraints     65
max-open-constraints       5
max-open-metas            21
metas                    326
pointers  (fresh)          0
pointers (reused)          0

     Finished Relation.Binary.Reflection.
Ticks for Algebra.RingSolver
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         9078
Integer (reused)       228151
Node  (fresh)           77200
Node (reused)         2753471
String  (fresh)           657
String (reused)        560536
attempted-constraints      94
max-open-constraints        2
max-open-metas             32
metas                    1521
pointers  (fresh)           0
pointers (reused)           0

    Finished Algebra.RingSolver.
Ticks for Algebra.RingSolver.Simple
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         559
Integer (reused)       91976
Node  (fresh)          22331
Node (reused)         925604
String  (fresh)          323
String (reused)       242005
attempted-constraints      6
max-open-constraints       2
max-open-metas             8
metas                     20
pointers  (fresh)          0
pointers (reused)          0

   Finished Algebra.RingSolver.Simple.
Ticks for Data.Nat.Properties
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         7644
Integer (reused)       226768
Node  (fresh)           68737
Node (reused)         2360840
String  (fresh)           643
String (reused)        626097
attempted-constraints      59
max-open-constraints        2
max-open-metas             18
metas                    1348
pointers  (fresh)           0
pointers (reused)           0

  Finished Data.Nat.Properties.
  Checking Relation.Binary.On (/home/abel/agda/agda-stdlib/src/Relation/Binary/On.agda).
Ticks for Relation.Binary.On
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        3261
Integer (reused)       62064
Node  (fresh)          24791
Node (reused)         621252
String  (fresh)          230
String (reused)       133509
attempted-constraints    345
max-open-constraints       2
max-open-metas            13
metas                    987
pointers  (fresh)          0
pointers (reused)          0

  Finished Relation.Binary.On.
  Checking Relation.Binary.PropositionalEquality.TrustMe (/home/abel/agda/agda-stdlib/src/Relation/Binary/PropositionalEquality/TrustMe.agda).
Ticks for Relation.Binary.PropositionalEquality.TrustMe
Double  (fresh)          0
Double (reused)          0
Integer  (fresh)       170
Integer (reused)      1741
Node  (fresh)         1474
Node (reused)        19113
String  (fresh)         62
String (reused)       7508
max-open-constraints     0
max-open-metas           4
metas                   16
pointers  (fresh)        0
pointers (reused)        0

  Finished Relation.Binary.PropositionalEquality.TrustMe.
Ticks for Data.Char
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         849
Integer (reused)       16543
Node  (fresh)          11877
Node (reused)         171952
String  (fresh)          390
String (reused)        50794
attempted-constraints      6
max-open-constraints       2
max-open-metas             8
metas                     49
pointers  (fresh)          0
pointers (reused)          0

 Finished Data.Char.
 Checking Data.Stream (/home/abel/agda/agda-stdlib/src/Data/Stream.agda).
  Checking Coinduction (/home/abel/agda/agda-stdlib/src/Coinduction.agda).
Ticks for Coinduction
Double  (fresh)         0
Double (reused)         0
Integer  (fresh)      265
Integer (reused)      720
Node  (fresh)        1027
Node (reused)        8087
String  (fresh)        26
String (reused)      1062
max-open-constraints    0
max-open-metas          4
metas                  35
pointers  (fresh)       0
pointers (reused)       0

  Finished Coinduction.
  Checking Data.Colist (/home/abel/agda/agda-stdlib/src/Data/Colist.agda).
   Checking Data.BoundedVec.Inefficient (/home/abel/agda/agda-stdlib/src/Data/BoundedVec/Inefficient.agda).
Ticks for Data.BoundedVec.Inefficient
Double  (fresh)          0
Double (reused)          0
Integer  (fresh)       450
Integer (reused)      4966
Node  (fresh)         3719
Node (reused)        58801
String  (fresh)        136
String (reused)      17012
max-open-constraints     0
max-open-metas           4
metas                   50
pointers  (fresh)        0
pointers (reused)        0

   Finished Data.BoundedVec.Inefficient.
   Checking Data.Conat (/home/abel/agda/agda-stdlib/src/Data/Conat.agda).
Ticks for Data.Conat
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         813
Integer (reused)       15013
Node  (fresh)           8860
Node (reused)         155174
String  (fresh)          197
String (reused)        38779
attempted-constraints     17
max-open-constraints       3
max-open-metas             9
metas                     73
pointers  (fresh)          0
pointers (reused)          0

   Finished Data.Conat.
   Checking Data.List.NonEmpty (/home/abel/agda/agda-stdlib/src/Data/List/NonEmpty.agda).
    Checking Data.Bool.Properties (/home/abel/agda/agda-stdlib/src/Data/Bool/Properties.agda).
     Checking Algebra.Properties.BooleanAlgebra (/home/abel/agda/agda-stdlib/src/Algebra/Properties/BooleanAlgebra.agda).
      Checking Algebra.Properties.DistributiveLattice (/home/abel/agda/agda-stdlib/src/Algebra/Properties/DistributiveLattice.agda).
       Checking Algebra.Properties.Lattice (/home/abel/agda/agda-stdlib/src/Algebra/Properties/Lattice.agda).
Ticks for Algebra.Properties.Lattice
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1939
Integer (reused)       50212
Node  (fresh)          23649
Node (reused)         510171
String  (fresh)          366
String (reused)       118578
attempted-constraints     41
max-open-constraints       2
max-open-metas            14
metas                    342
pointers  (fresh)          0
pointers (reused)          0

       Finished Algebra.Properties.Lattice.
Ticks for Algebra.Properties.DistributiveLattice
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1756
Integer (reused)       58056
Node  (fresh)          24759
Node (reused)         590233
String  (fresh)          359
String (reused)       134445
attempted-constraints     33
max-open-constraints       2
max-open-metas            21
metas                    234
pointers  (fresh)          0
pointers (reused)          0

      Finished Algebra.Properties.DistributiveLattice.
Ticks for Algebra.Properties.BooleanAlgebra
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         9525
Integer (reused)       296826
Node  (fresh)           58456
Node (reused)         2952237
String  (fresh)           422
String (reused)        642371
attempted-constraints     291
max-open-constraints        2
max-open-metas             26
metas                    2295
pointers  (fresh)           0
pointers (reused)           0

     Finished Algebra.Properties.BooleanAlgebra.
Ticks for Data.Bool.Properties
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         3550
Integer (reused)       296735
Node  (fresh)           48700
Node (reused)         2889302
String  (fresh)           549
String (reused)        736755
attempted-constraints      48
max-open-constraints        5
max-open-metas             16
metas                     547
pointers  (fresh)           0
pointers (reused)           0

    Finished Data.Bool.Properties.
Ticks for Data.List.NonEmpty
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        4179
Integer (reused)       56841
Node  (fresh)          29091
Node (reused)         629831
String  (fresh)          515
String (reused)       164189
attempted-constraints    217
max-open-constraints       7
max-open-metas            37
metas                   1006
pointers  (fresh)          0
pointers (reused)          0

   Finished Data.List.NonEmpty.
   Checking Function.Inverse (/home/abel/agda/agda-stdlib/src/Function/Inverse.agda).
    Checking Function.Bijection (/home/abel/agda/agda-stdlib/src/Function/Bijection.agda).
     Checking Function.Surjection (/home/abel/agda/agda-stdlib/src/Function/Surjection.agda).
      Checking Function.LeftInverse (/home/abel/agda/agda-stdlib/src/Function/LeftInverse.agda).
Ticks for Function.LeftInverse
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1492
Integer (reused)       37523
Node  (fresh)          15936
Node (reused)         381137
String  (fresh)          257
String (reused)        88413
attempted-constraints     78
max-open-constraints       1
max-open-metas            18
metas                    476
pointers  (fresh)          0
pointers (reused)          0

      Finished Function.LeftInverse.
Ticks for Function.Surjection
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1237
Integer (reused)       23894
Node  (fresh)          12875
Node (reused)         241532
String  (fresh)          263
String (reused)        55559
attempted-constraints     48
max-open-constraints       1
max-open-metas            17
metas                    274
pointers  (fresh)          0
pointers (reused)          0

     Finished Function.Surjection.
Ticks for Function.Bijection
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1105
Integer (reused)       25225
Node  (fresh)          12098
Node (reused)         256137
String  (fresh)          223
String (reused)        56977
attempted-constraints     46
max-open-constraints       1
max-open-metas            21
metas                    277
pointers  (fresh)          0
pointers (reused)          0

    Finished Function.Bijection.
Ticks for Function.Inverse
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2115
Integer (reused)       53305
Node  (fresh)          20087
Node (reused)         533739
String  (fresh)          357
String (reused)       103411
attempted-constraints    153
max-open-constraints       5
max-open-metas            25
metas                    657
pointers  (fresh)          0
pointers (reused)          0

   Finished Function.Inverse.
   Checking Relation.Binary.InducedPreorders (/home/abel/agda/agda-stdlib/src/Relation/Binary/InducedPreorders.agda).
Ticks for Relation.Binary.InducedPreorders
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         723
Integer (reused)       13009
Node  (fresh)           7906
Node (reused)         134649
String  (fresh)          182
String (reused)        35752
attempted-constraints     19
max-open-constraints       4
max-open-metas            12
metas                     70
pointers  (fresh)          0
pointers (reused)          0

   Finished Relation.Binary.InducedPreorders.
   Checking Relation.Nullary.Negation (/home/abel/agda/agda-stdlib/src/Relation/Nullary/Negation.agda).
    Checking Data.Fin.Dec (/home/abel/agda/agda-stdlib/src/Data/Fin/Dec.agda).
     Checking Data.Vec.Equality (/home/abel/agda/agda-stdlib/src/Data/Vec/Equality.agda).
Ticks for Data.Vec.Equality
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1629
Integer (reused)       42969
Node  (fresh)          18799
Node (reused)         437137
String  (fresh)          352
String (reused)       115478
attempted-constraints      5
max-open-constraints       1
max-open-metas            12
metas                    276
pointers  (fresh)          0
pointers (reused)          0

     Finished Data.Vec.Equality.
     Checking Data.Fin.Subset (/home/abel/agda/agda-stdlib/src/Data/Fin/Subset.agda).
      Checking Algebra.Properties.BooleanAlgebra.Expression (/home/abel/agda/agda-stdlib/src/Algebra/Properties/BooleanAlgebra/Expression.agda).
       Checking Data.Vec.Properties (/home/abel/agda/agda-stdlib/src/Data/Vec/Properties.agda).
        Checking Data.List.Any (/home/abel/agda/agda-stdlib/src/Data/List/Any.agda).
         Checking Function.Related (/home/abel/agda/agda-stdlib/src/Function/Related.agda).
Ticks for Function.Related
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        4235
Integer (reused)       61233
Node  (fresh)          29216
Node (reused)         629749
String  (fresh)          318
String (reused)       142569
attempted-constraints    253
max-open-constraints       4
max-open-metas            22
metas                   1143
pointers  (fresh)          0
pointers (reused)          0

         Finished Function.Related.
         Checking Relation.Binary.List.Pointwise (/home/abel/agda/agda-stdlib/src/Relation/Binary/List/Pointwise.agda).
Ticks for Relation.Binary.List.Pointwise
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        3446
Integer (reused)       53898
Node  (fresh)          25927
Node (reused)         558108
String  (fresh)          389
String (reused)       152197
attempted-constraints    246
max-open-constraints       4
max-open-metas            18
metas                   1100
pointers  (fresh)          0
pointers (reused)          0

         Finished Relation.Binary.List.Pointwise.
Ticks for Data.List.Any
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2969
Integer (reused)       55164
Node  (fresh)          26303
Node (reused)         567483
String  (fresh)          488
String (reused)       152886
attempted-constraints    104
max-open-constraints       4
max-open-metas            20
metas                    597
pointers  (fresh)          0
pointers (reused)          0

        Finished Data.List.Any.
        Checking Data.Fin.Properties (/home/abel/agda/agda-stdlib/src/Data/Fin/Properties.agda).
Ticks for Data.Fin.Properties
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        4111
Integer (reused)       92668
Node  (fresh)          43602
Node (reused)         951452
String  (fresh)          671
String (reused)       236905
attempted-constraints     88
max-open-constraints       3
max-open-metas            15
metas                    736
pointers  (fresh)          0
pointers (reused)          0

        Finished Data.Fin.Properties.
        Checking Relation.Binary.HeterogeneousEquality (/home/abel/agda/agda-stdlib/src/Relation/Binary/HeterogeneousEquality.agda).
Ticks for Relation.Binary.HeterogeneousEquality
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        3449
Integer (reused)       25223
Node  (fresh)          19192
Node (reused)         272225
String  (fresh)          320
String (reused)        79545
attempted-constraints     38
max-open-constraints       9
max-open-metas            18
metas                    611
pointers  (fresh)          0
pointers (reused)          0

        Finished Relation.Binary.HeterogeneousEquality.
Ticks for Data.Vec.Properties
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         7155
Integer (reused)       119891
Node  (fresh)           61424
Node (reused)         1285659
String  (fresh)           852
String (reused)        315272
attempted-constraints     158
max-open-constraints        5
max-open-metas             18
metas                    1846
pointers  (fresh)           0
pointers (reused)           0

       Finished Data.Vec.Properties.
       Checking Relation.Binary.Vec.Pointwise (/home/abel/agda/agda-stdlib/src/Relation/Binary/Vec/Pointwise.agda).
        Checking Data.Plus (/home/abel/agda/agda-stdlib/src/Data/Plus.agda).
Ticks for Data.Plus
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1249
Integer (reused)       13354
Node  (fresh)           9776
Node (reused)         153517
String  (fresh)          200
String (reused)        37127
attempted-constraints     71
max-open-constraints       4
max-open-metas            15
metas                    272
pointers  (fresh)          0
pointers (reused)          0

        Finished Data.Plus.
Ticks for Relation.Binary.Vec.Pointwise
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        3758
Integer (reused)       71981
Node  (fresh)          31529
Node (reused)         762533
String  (fresh)          495
String (reused)       207944
attempted-constraints    364
max-open-constraints      15
max-open-metas            48
metas                   1197
pointers  (fresh)          0
pointers (reused)          0

       Finished Relation.Binary.Vec.Pointwise.
Ticks for Algebra.Properties.BooleanAlgebra.Expression
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         3152
Integer (reused)       330354
Node  (fresh)           35442
Node (reused)         3324608
String  (fresh)           531
String (reused)        864863
attempted-constraints      42
max-open-constraints        4
max-open-metas             22
metas                     859
pointers  (fresh)           0
pointers (reused)           0

      Finished Algebra.Properties.BooleanAlgebra.Expression.
Ticks for Data.Fin.Subset
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1360
Integer (reused)       29852
Node  (fresh)          19067
Node (reused)         319158
String  (fresh)          522
String (reused)        83054
attempted-constraints      3
max-open-constraints       1
max-open-metas             8
metas                    102
pointers  (fresh)          0
pointers (reused)          0

     Finished Data.Fin.Subset.
     Checking Data.Fin.Subset.Properties (/home/abel/agda/agda-stdlib/src/Data/Fin/Subset/Properties.agda).
Ticks for Data.Fin.Subset.Properties
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2759
Integer (reused)       75101
Node  (fresh)          33873
Node (reused)         760902
String  (fresh)          579
String (reused)       209194
attempted-constraints     29
max-open-constraints       2
max-open-metas            14
metas                    536
pointers  (fresh)          0
pointers (reused)          0

     Finished Data.Fin.Subset.Properties.
Ticks for Data.Fin.Dec
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        3015
Integer (reused)       48124
Node  (fresh)          27393
Node (reused)         503211
String  (fresh)          494
String (reused)       130720
attempted-constraints     66
max-open-constraints       5
max-open-metas            24
metas                    434
pointers  (fresh)          0
pointers (reused)          0

    Finished Data.Fin.Dec.
Ticks for Relation.Nullary.Negation
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2482
Integer (reused)       16090
Node  (fresh)          13591
Node (reused)         176179
String  (fresh)          288
String (reused)        44950
attempted-constraints     75
max-open-constraints       5
max-open-metas            21
metas                    512
pointers  (fresh)          0
pointers (reused)          0

   Finished Relation.Nullary.Negation.
Ticks for Data.Colist
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         7392
Integer (reused)       114114
Node  (fresh)           55571
Node (reused)         1241398
String  (fresh)           742
String (reused)        280095
attempted-constraints     335
max-open-constraints        8
max-open-metas             28
metas                    1830
pointers  (fresh)           0
pointers (reused)           0

  Finished Data.Colist.
Ticks for Data.Stream
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2310
Integer (reused)       26916
Node  (fresh)          18346
Node (reused)         302896
String  (fresh)          378
String (reused)        72700
attempted-constraints     32
max-open-constraints       3
max-open-metas            14
metas                    421
pointers  (fresh)          0
pointers (reused)          0

 Finished Data.Stream.
 Checking Data.String (/home/abel/agda/agda-stdlib/src/Data/String.agda).
  Checking Relation.Binary.List.StrictLex (/home/abel/agda/agda-stdlib/src/Relation/Binary/List/StrictLex.agda).
Ticks for Relation.Binary.List.StrictLex
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         4576
Integer (reused)       101270
Node  (fresh)           37878
Node (reused)         1042526
String  (fresh)           390
String (reused)        284005
attempted-constraints     191
max-open-constraints        4
max-open-metas             22
metas                    1288
pointers  (fresh)           0
pointers (reused)           0

  Finished Relation.Binary.List.StrictLex.
Ticks for Data.String
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1176
Integer (reused)       19825
Node  (fresh)          14620
Node (reused)         202784
String  (fresh)          401
String (reused)        58488
attempted-constraints      7
max-open-constraints       2
max-open-metas             8
metas                    102
pointers  (fresh)          0
pointers (reused)          0

 Finished Data.String.
 Checking Induction (/home/abel/agda/agda-stdlib/src/Induction.agda).
Ticks for Induction
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        635
Integer (reused)       2867
Node  (fresh)          3129
Node (reused)         32006
String  (fresh)          84
String (reused)        5848
attempted-constraints    28
max-open-constraints      3
max-open-metas            8
metas                   140
pointers  (fresh)         0
pointers (reused)         0

 Finished Induction.
 Checking Induction.WellFounded (/home/abel/agda/agda-stdlib/src/Induction/WellFounded.agda).
Ticks for Induction.WellFounded
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2113
Integer (reused)       20803
Node  (fresh)          14733
Node (reused)         223165
String  (fresh)          272
String (reused)        50719
attempted-constraints    108
max-open-constraints       7
max-open-metas            11
metas                    402
pointers  (fresh)          0
pointers (reused)          0

 Finished Induction.WellFounded.
 Checking Induction.Nat (/home/abel/agda/agda-stdlib/src/Induction/Nat.agda).
Ticks for Induction.Nat
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2238
Integer (reused)       25283
Node  (fresh)          15294
Node (reused)         283512
String  (fresh)          323
String (reused)        73862
attempted-constraints    187
max-open-constraints       7
max-open-metas            20
metas                    411
pointers  (fresh)          0
pointers (reused)          0

 Finished Induction.Nat.
 Checking IO (/home/abel/agda/agda-stdlib/src/IO.agda).
  Checking IO.Primitive (/home/abel/agda/agda-stdlib/src/IO/Primitive.agda).
   Checking Foreign.Haskell (/home/abel/agda/agda-stdlib/src/Foreign/Haskell.agda).
Ticks for Foreign.Haskell
Double  (fresh)         0
Double (reused)         0
Integer  (fresh)       47
Integer (reused)      277
Node  (fresh)         188
Node (reused)        2866
String  (fresh)         5
String (reused)       648
max-open-constraints    0
max-open-metas          1
metas                   1
pointers  (fresh)       0
pointers (reused)       0

   Finished Foreign.Haskell.
Ticks for IO.Primitive
Double  (fresh)          0
Double (reused)          0
Integer  (fresh)       395
Integer (reused)      1322
Node  (fresh)         1566
Node (reused)        14800
String  (fresh)         53
String (reused)       3411
max-open-constraints     0
max-open-metas           4
metas                   41
pointers  (fresh)        0
pointers (reused)        0

  Finished IO.Primitive.
Ticks for IO
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1268
Integer (reused)       11414
Node  (fresh)           9497
Node (reused)         128068
String  (fresh)          219
String (reused)        23796
attempted-constraints      6
max-open-constraints       1
max-open-metas            10
metas                    182
pointers  (fresh)          0
pointers (reused)          0

 Finished IO.
 Checking README.Nat (/home/abel/agda/agda-stdlib/README/Nat.agda).
Ticks for README.Nat
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         952
Integer (reused)       29905
Node  (fresh)          15896
Node (reused)         318590
String  (fresh)          419
String (reused)        78338
attempted-constraints      1
max-open-constraints       1
max-open-metas            12
metas                     55
pointers  (fresh)          0
pointers (reused)          0

 Finished README.Nat.
 Checking README.Integer (/home/abel/agda/agda-stdlib/README/Integer.agda).
  Checking Data.Integer (/home/abel/agda/agda-stdlib/src/Data/Integer.agda).
   Checking Data.Nat.Show (/home/abel/agda/agda-stdlib/src/Data/Nat/Show.agda).
    Checking Data.Digit (/home/abel/agda/agda-stdlib/src/Data/Digit.agda).
     Checking Data.Nat.DivMod (/home/abel/agda/agda-stdlib/src/Data/Nat/DivMod.agda).
Ticks for Data.Nat.DivMod
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1508
Integer (reused)       46260
Node  (fresh)          14558
Node (reused)         483720
String  (fresh)          403
String (reused)       135158
attempted-constraints     31
max-open-constraints       3
max-open-metas            22
metas                    184
pointers  (fresh)          0
pointers (reused)          0

     Finished Data.Nat.DivMod.
Ticks for Data.Digit
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1382
Integer (reused)       27293
Node  (fresh)          15425
Node (reused)         295313
String  (fresh)          469
String (reused)        80468
attempted-constraints    130
max-open-constraints      14
max-open-metas            16
metas                    153
pointers  (fresh)          0
pointers (reused)          0

    Finished Data.Digit.
Ticks for Data.Nat.Show
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        358
Integer (reused)       4550
Node  (fresh)          4911
Node (reused)         55503
String  (fresh)         214
String (reused)       15715
attempted-constraints     2
max-open-constraints      1
max-open-metas           10
metas                    41
pointers  (fresh)         0
pointers (reused)         0

   Finished Data.Nat.Show.
   Checking Data.Sign (/home/abel/agda/agda-stdlib/src/Data/Sign.agda).
Ticks for Data.Sign
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         495
Integer (reused)       11769
Node  (fresh)           7257
Node (reused)         122841
String  (fresh)          158
String (reused)        35200
attempted-constraints      2
max-open-constraints       2
max-open-metas             6
metas                     14
pointers  (fresh)          0
pointers (reused)          0

   Finished Data.Sign.
Ticks for Data.Integer
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2902
Integer (reused)       41545
Node  (fresh)          23401
Node (reused)         444051
String  (fresh)          335
String (reused)       115434
attempted-constraints     23
max-open-constraints       3
max-open-metas            23
metas                    392
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Integer.
  Checking Data.Integer.Properties (/home/abel/agda/agda-stdlib/src/Data/Integer/Properties.agda).
   Checking Data.Integer.Addition.Properties (/home/abel/agda/agda-stdlib/src/Data/Integer/Addition/Properties.agda).
Ticks for Data.Integer.Addition.Properties
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1991
Integer (reused)       68583
Node  (fresh)          28439
Node (reused)         727040
String  (fresh)          471
String (reused)       203765
attempted-constraints     33
max-open-constraints       1
max-open-metas             9
metas                    177
pointers  (fresh)          0
pointers (reused)          0

   Finished Data.Integer.Addition.Properties.
   Checking Data.Integer.Multiplication.Properties (/home/abel/agda/agda-stdlib/src/Data/Integer/Multiplication/Properties.agda).
Ticks for Data.Integer.Multiplication.Properties
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1953
Integer (reused)       62161
Node  (fresh)          26785
Node (reused)         648706
String  (fresh)          494
String (reused)       178707
attempted-constraints     27
max-open-constraints       3
max-open-metas            10
metas                    227
pointers  (fresh)          0
pointers (reused)          0

   Finished Data.Integer.Multiplication.Properties.
   Checking Data.Sign.Properties (/home/abel/agda/agda-stdlib/src/Data/Sign/Properties.agda).
Ticks for Data.Sign.Properties
Double  (fresh)          0
Double (reused)          0
Integer  (fresh)       261
Integer (reused)      3793
Node  (fresh)         2793
Node (reused)        42215
String  (fresh)         92
String (reused)      13267
max-open-constraints     0
max-open-metas           9
metas                   31
pointers  (fresh)        0
pointers (reused)        0

   Finished Data.Sign.Properties.
Ticks for Data.Integer.Properties
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         5844
Integer (reused)       379799
Node  (fresh)           71251
Node (reused)         3903863
String  (fresh)           754
String (reused)       1019261
attempted-constraints      39
max-open-constraints        3
max-open-metas             14
metas                     726
pointers  (fresh)           0
pointers (reused)           0

  Finished Data.Integer.Properties.
Ticks for README.Integer
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1071
Integer (reused)       31390
Node  (fresh)          15993
Node (reused)         330449
String  (fresh)          361
String (reused)        79058
attempted-constraints      1
max-open-constraints       1
max-open-metas            12
metas                     59
pointers  (fresh)          0
pointers (reused)          0

 Finished README.Integer.
 Checking README.AVL (/home/abel/agda/agda-stdlib/README/AVL.agda).
  Checking Data.AVL (/home/abel/agda/agda-stdlib/src/Data/AVL.agda).
   Checking Data.DifferenceList (/home/abel/agda/agda-stdlib/src/Data/DifferenceList.agda).
Ticks for Data.DifferenceList
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        844
Integer (reused)       4571
Node  (fresh)          5099
Node (reused)         54415
String  (fresh)         164
String (reused)       12745
attempted-constraints    22
max-open-constraints      5
max-open-metas           10
metas                   140
pointers  (fresh)         0
pointers (reused)         0

   Finished Data.DifferenceList.
Ticks for Data.AVL
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         6528
Integer (reused)       115477
Node  (fresh)           50458
Node (reused)         1302702
String  (fresh)           490
String (reused)        268342
attempted-constraints      72
max-open-constraints        4
max-open-metas             14
metas                     954
pointers  (fresh)           0
pointers (reused)           0

  Finished Data.AVL.
  Checking Data.AVL.IndexedMap (/home/abel/agda/agda-stdlib/src/Data/AVL/IndexedMap.agda).
Ticks for Data.AVL.IndexedMap
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1144
Integer (reused)       66341
Node  (fresh)          23898
Node (reused)         699777
String  (fresh)          366
String (reused)       143085
attempted-constraints     52
max-open-constraints       3
max-open-metas            14
metas                    190
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.AVL.IndexedMap.
  Checking Data.AVL.Sets (/home/abel/agda/agda-stdlib/src/Data/AVL/Sets.agda).
Ticks for Data.AVL.Sets
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         847
Integer (reused)       48733
Node  (fresh)          21280
Node (reused)         534806
String  (fresh)          368
String (reused)       115735
attempted-constraints     26
max-open-constraints       3
max-open-metas            16
metas                    123
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.AVL.Sets.
Ticks for README.AVL
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1207
Integer (reused)       78438
Node  (fresh)          23542
Node (reused)         778073
String  (fresh)          536
String (reused)       190415
attempted-constraints     30
max-open-constraints       5
max-open-metas            17
metas                    110
pointers  (fresh)          0
pointers (reused)          0

 Finished README.AVL.
 Checking README.Record (/home/abel/agda/agda-stdlib/README/Record.agda).
  Checking Record (/home/abel/agda/agda-stdlib/src/Record.agda).
Ticks for Record
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        3231
Integer (reused)       37970
Node  (fresh)          23356
Node (reused)         465799
String  (fresh)          348
String (reused)        94258
attempted-constraints     35
max-open-constraints       2
max-open-metas            10
metas                    390
pointers  (fresh)          0
pointers (reused)          0

  Finished Record.
Ticks for README.Record
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         755
Integer (reused)       24205
Node  (fresh)          11645
Node (reused)         248862
String  (fresh)          230
String (reused)        54584
attempted-constraints      8
max-open-constraints       2
max-open-metas            10
metas                     82
pointers  (fresh)          0
pointers (reused)          0

 Finished README.Record.
 Checking README.Case (/home/abel/agda/agda-stdlib/README/Case.agda).
Ticks for README.Case
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        358
Integer (reused)       4380
Node  (fresh)          4221
Node (reused)         55083
String  (fresh)         158
String (reused)       14788
attempted-constraints     3
max-open-constraints      1
max-open-metas            4
metas                    29
pointers  (fresh)         0
pointers (reused)         0

 Finished README.Case.
 Checking Everything (/home/abel/agda/agda-stdlib/Everything.agda).
  Checking Algebra.Monoid-solver (/home/abel/agda/agda-stdlib/src/Algebra/Monoid-solver.agda).
Ticks for Algebra.Monoid-solver
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2008
Integer (reused)       45649
Node  (fresh)          24797
Node (reused)         494688
String  (fresh)          511
String (reused)       105535
attempted-constraints     17
max-open-constraints       2
max-open-metas            11
metas                    298
pointers  (fresh)          0
pointers (reused)          0

  Finished Algebra.Monoid-solver.
  Checking Algebra.Props.AbelianGroup (/home/abel/agda/agda-stdlib/src/Algebra/Props/AbelianGroup.agda).
Ticks for Algebra.Props.AbelianGroup
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         600
Integer (reused)       12660
Node  (fresh)           8419
Node (reused)         128336
String  (fresh)          165
String (reused)        27334
attempted-constraints      1
max-open-constraints       1
max-open-metas             5
metas                      7
pointers  (fresh)          0
pointers (reused)          0

  Finished Algebra.Props.AbelianGroup.
  Checking Algebra.Props.BooleanAlgebra (/home/abel/agda/agda-stdlib/src/Algebra/Props/BooleanAlgebra.agda).
Ticks for Algebra.Props.BooleanAlgebra
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         644
Integer (reused)       23496
Node  (fresh)          11194
Node (reused)         234165
String  (fresh)          201
String (reused)        53805
attempted-constraints      1
max-open-constraints       1
max-open-metas             5
metas                      7
pointers  (fresh)          0
pointers (reused)          0

  Finished Algebra.Props.BooleanAlgebra.
  Checking Algebra.Props.DistributiveLattice (/home/abel/agda/agda-stdlib/src/Algebra/Props/DistributiveLattice.agda).
Ticks for Algebra.Props.DistributiveLattice
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         608
Integer (reused)       11932
Node  (fresh)           8749
Node (reused)         124325
String  (fresh)          175
String (reused)        26764
attempted-constraints      1
max-open-constraints       1
max-open-metas             5
metas                      7
pointers  (fresh)          0
pointers (reused)          0

  Finished Algebra.Props.DistributiveLattice.
  Checking Algebra.Props.Group (/home/abel/agda/agda-stdlib/src/Algebra/Props/Group.agda).
Ticks for Algebra.Props.Group
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         599
Integer (reused)       10900
Node  (fresh)           8193
Node (reused)         114218
String  (fresh)          163
String (reused)        23805
attempted-constraints      1
max-open-constraints       1
max-open-metas             5
metas                      7
pointers  (fresh)          0
pointers (reused)          0

  Finished Algebra.Props.Group.
  Checking Algebra.Props.Lattice (/home/abel/agda/agda-stdlib/src/Algebra/Props/Lattice.agda).
Ticks for Algebra.Props.Lattice
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         610
Integer (reused)       10391
Node  (fresh)           8313
Node (reused)         109627
String  (fresh)          169
String (reused)        22839
attempted-constraints      1
max-open-constraints       1
max-open-metas             5
metas                      7
pointers  (fresh)          0
pointers (reused)          0

  Finished Algebra.Props.Lattice.
  Checking Algebra.Props.Ring (/home/abel/agda/agda-stdlib/src/Algebra/Props/Ring.agda).
Ticks for Algebra.Props.Ring
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         604
Integer (reused)       14987
Node  (fresh)           8780
Node (reused)         147756
String  (fresh)          175
String (reused)        32114
attempted-constraints      1
max-open-constraints       1
max-open-metas             5
metas                      7
pointers  (fresh)          0
pointers (reused)          0

  Finished Algebra.Props.Ring.
  Checking Algebra.RingSolver.Natural-coefficients (/home/abel/agda/agda-stdlib/src/Algebra/RingSolver/Natural-coefficients.agda).
Ticks for Algebra.RingSolver.Natural-coefficients
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         1211
Integer (reused)       140579
Node  (fresh)           33914
Node (reused)         1471920
String  (fresh)           446
String (reused)        316170
attempted-constraints      11
max-open-constraints        1
max-open-metas             12
metas                      82
pointers  (fresh)           0
pointers (reused)           0

  Finished Algebra.RingSolver.Natural-coefficients.
  Checking Category.Applicative.Predicate (/home/abel/agda/agda-stdlib/src/Category/Applicative/Predicate.agda).
   Checking Category.Functor.Predicate (/home/abel/agda/agda-stdlib/src/Category/Functor/Predicate.agda).
    Checking Relation.Unary.PredicateTransformer (/home/abel/agda/agda-stdlib/src/Relation/Unary/PredicateTransformer.agda).
Ticks for Relation.Unary.PredicateTransformer
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1686
Integer (reused)       15399
Node  (fresh)          11128
Node (reused)         161472
String  (fresh)          245
String (reused)        41465
attempted-constraints     35
max-open-constraints       3
max-open-metas            12
metas                    279
pointers  (fresh)          0
pointers (reused)          0

    Finished Relation.Unary.PredicateTransformer.
Ticks for Category.Functor.Predicate
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        296
Integer (reused)       3380
Node  (fresh)          3114
Node (reused)         36800
String  (fresh)         118
String (reused)        9449
attempted-constraints    11
max-open-constraints      2
max-open-metas           14
metas                    51
pointers  (fresh)         0
pointers (reused)         0

   Finished Category.Functor.Predicate.
Ticks for Category.Applicative.Predicate
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        585
Integer (reused)       7444
Node  (fresh)          5265
Node (reused)         84564
String  (fresh)         158
String (reused)       21188
attempted-constraints    69
max-open-constraints      4
max-open-metas           16
metas                   194
pointers  (fresh)         0
pointers (reused)         0

  Finished Category.Applicative.Predicate.
  Checking Category.Monad.Continuation (/home/abel/agda/agda-stdlib/src/Category/Monad/Continuation.agda).
Ticks for Category.Monad.Continuation
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         970
Integer (reused)       24490
Node  (fresh)           9964
Node (reused)         256827
String  (fresh)          136
String (reused)        63283
attempted-constraints     20
max-open-constraints       2
max-open-metas            12
metas                    157
pointers  (fresh)          0
pointers (reused)          0

  Finished Category.Monad.Continuation.
  Checking Category.Monad.Partiality (/home/abel/agda/agda-stdlib/src/Category/Monad/Partiality.agda).
Ticks for Category.Monad.Partiality
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)        13064
Integer (reused)       305900
Node  (fresh)           90059
Node (reused)         3038830
String  (fresh)           617
String (reused)        775601
attempted-constraints     598
max-open-constraints        7
max-open-metas             31
metas                    3220
pointers  (fresh)           0
pointers (reused)           0

  Finished Category.Monad.Partiality.
  Checking Category.Monad.Partiality.All (/home/abel/agda/agda-stdlib/src/Category/Monad/Partiality/All.agda).
Ticks for Category.Monad.Partiality.All
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        3008
Integer (reused)       46659
Node  (fresh)          23994
Node (reused)         475775
String  (fresh)          370
String (reused)       141052
attempted-constraints    143
max-open-constraints       5
max-open-metas            13
metas                    672
pointers  (fresh)          0
pointers (reused)          0

  Finished Category.Monad.Partiality.All.
  Checking Category.Monad.Predicate (/home/abel/agda/agda-stdlib/src/Category/Monad/Predicate.agda).
Ticks for Category.Monad.Predicate
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1006
Integer (reused)       23644
Node  (fresh)          11775
Node (reused)         256352
String  (fresh)          268
String (reused)        68404
attempted-constraints     41
max-open-constraints       5
max-open-metas            18
metas                    243
pointers  (fresh)          0
pointers (reused)          0

  Finished Category.Monad.Predicate.
  Checking Category.Monad.State (/home/abel/agda/agda-stdlib/src/Category/Monad/State.agda).
Ticks for Category.Monad.State
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1815
Integer (reused)       55371
Node  (fresh)          18408
Node (reused)         575571
String  (fresh)          180
String (reused)       137500
attempted-constraints     57
max-open-constraints       3
max-open-metas            11
metas                    348
pointers  (fresh)          0
pointers (reused)          0

  Finished Category.Monad.State.
  Checking Data.Bin (/home/abel/agda/agda-stdlib/src/Data/Bin.agda).
Ticks for Data.Bin
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         3921
Integer (reused)       116465
Node  (fresh)           45858
Node (reused)         1209415
String  (fresh)           698
String (reused)        281672
attempted-constraints      29
max-open-constraints        2
max-open-metas             13
metas                     484
pointers  (fresh)           0
pointers (reused)           0

  Finished Data.Bin.
  Checking Data.Bool.Show (/home/abel/agda/agda-stdlib/src/Data/Bool/Show.agda).
Ticks for Data.Bool.Show
Double  (fresh)         0
Double (reused)         0
Integer  (fresh)       83
Integer (reused)      770
Node  (fresh)         884
Node (reused)        9297
String  (fresh)        30
String (reused)      2784
max-open-constraints    0
max-open-metas          1
metas                   2
pointers  (fresh)       0
pointers (reused)       0

  Finished Data.Bool.Show.
  Checking Data.BoundedVec (/home/abel/agda/agda-stdlib/src/Data/BoundedVec.agda).
Ticks for Data.BoundedVec
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         977
Integer (reused)       12645
Node  (fresh)           9414
Node (reused)         145751
String  (fresh)          338
String (reused)        43553
attempted-constraints      3
max-open-constraints       1
max-open-metas             6
metas                    104
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.BoundedVec.
  Checking Data.Cofin (/home/abel/agda/agda-stdlib/src/Data/Cofin.agda).
Ticks for Data.Cofin
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        449
Integer (reused)       4487
Node  (fresh)          3686
Node (reused)         48301
String  (fresh)         107
String (reused)       11768
attempted-constraints     8
max-open-constraints      2
max-open-metas            5
metas                    37
pointers  (fresh)         0
pointers (reused)         0

  Finished Data.Cofin.
  Checking Data.Colist.Infinite-merge (/home/abel/agda/agda-stdlib/src/Data/Colist/Infinite-merge.agda).
   Checking Function.Related.TypeIsomorphisms (/home/abel/agda/agda-stdlib/src/Function/Related/TypeIsomorphisms.agda).
    Checking Relation.Binary.Product.Pointwise (/home/abel/agda/agda-stdlib/src/Relation/Binary/Product/Pointwise.agda).
     Checking Relation.Nullary.Product (/home/abel/agda/agda-stdlib/src/Relation/Nullary/Product.agda).
Ticks for Relation.Nullary.Product
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        213
Integer (reused)       1644
Node  (fresh)          2020
Node (reused)         20034
String  (fresh)          74
String (reused)        5490
attempted-constraints     8
max-open-constraints      2
max-open-metas            6
metas                    32
pointers  (fresh)         0
pointers (reused)         0

     Finished Relation.Nullary.Product.
Ticks for Relation.Binary.Product.Pointwise
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        6316
Integer (reused)       88991
Node  (fresh)          39945
Node (reused)         909297
String  (fresh)          522
String (reused)       225017
attempted-constraints    491
max-open-constraints       4
max-open-metas            24
metas                   2339
pointers  (fresh)          0
pointers (reused)          0

    Finished Relation.Binary.Product.Pointwise.
    Checking Relation.Binary.Sum (/home/abel/agda/agda-stdlib/src/Relation/Binary/Sum.agda).
Ticks for Relation.Binary.Sum
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         9347
Integer (reused)       154485
Node  (fresh)           62027
Node (reused)         1609388
String  (fresh)           578
String (reused)        359245
attempted-constraints    1091
max-open-constraints       12
max-open-metas             36
metas                    3743
pointers  (fresh)           0
pointers (reused)           0

    Finished Relation.Binary.Sum.
Ticks for Function.Related.TypeIsomorphisms
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         7628
Integer (reused)       735311
Node  (fresh)           80630
Node (reused)         7377329
String  (fresh)           816
String (reused)       1781465
attempted-constraints     926
max-open-constraints       21
max-open-metas             35
metas                    2971
pointers  (fresh)           0
pointers (reused)           0

   Finished Function.Related.TypeIsomorphisms.
Ticks for Data.Colist.Infinite-merge
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         3902
Integer (reused)       104164
Node  (fresh)           35897
Node (reused)         1122904
String  (fresh)           642
String (reused)        274241
attempted-constraints     757
max-open-constraints       20
max-open-metas             44
metas                    1356
pointers  (fresh)           0
pointers (reused)           0

  Finished Data.Colist.Infinite-merge.
  Checking Data.Container (/home/abel/agda/agda-stdlib/src/Data/Container.agda).
   Checking Data.M (/home/abel/agda/agda-stdlib/src/Data/M.agda).
Ticks for Data.M
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        297
Integer (reused)       1111
Node  (fresh)          1386
Node (reused)         12208
String  (fresh)          33
String (reused)        2287
attempted-constraints     6
max-open-constraints      1
max-open-metas            5
metas                    41
pointers  (fresh)         0
pointers (reused)         0

   Finished Data.M.
   Checking Data.W (/home/abel/agda/agda-stdlib/src/Data/W.agda).
Ticks for Data.W
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        376
Integer (reused)       1301
Node  (fresh)          1689
Node (reused)         14296
String  (fresh)          40
String (reused)        2963
attempted-constraints     8
max-open-constraints      1
max-open-metas            5
metas                    54
pointers  (fresh)         0
pointers (reused)         0

   Finished Data.W.
Ticks for Data.Container
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        3722
Integer (reused)       55156
Node  (fresh)          25960
Node (reused)         569075
String  (fresh)          411
String (reused)       128496
attempted-constraints     79
max-open-constraints       3
max-open-metas            13
metas                    733
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Container.
  Checking Data.Container.Any (/home/abel/agda/agda-stdlib/src/Data/Container/Any.agda).
   Checking Data.Container.Combinator (/home/abel/agda/agda-stdlib/src/Data/Container/Combinator.agda).
Ticks for Data.Container.Combinator
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        3005
Integer (reused)       41315
Node  (fresh)          17547
Node (reused)         429409
String  (fresh)          268
String (reused)       108417
attempted-constraints    215
max-open-constraints      13
max-open-metas            23
metas                    783
pointers  (fresh)          0
pointers (reused)          0

   Finished Data.Container.Combinator.
   Checking Relation.Binary.Sigma.Pointwise (/home/abel/agda/agda-stdlib/src/Relation/Binary/Sigma/Pointwise.agda).
Ticks for Relation.Binary.Sigma.Pointwise
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         6857
Integer (reused)       134232
Node  (fresh)           40982
Node (reused)         1359363
String  (fresh)           431
String (reused)        360370
attempted-constraints    1992
max-open-constraints       23
max-open-metas             43
metas                    3576
pointers  (fresh)           0
pointers (reused)           0

   Finished Relation.Binary.Sigma.Pointwise.
Ticks for Data.Container.Any
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         5138
Integer (reused)       120817
Node  (fresh)           41083
Node (reused)         1312241
String  (fresh)           620
String (reused)        306961
attempted-constraints    1615
max-open-constraints       30
max-open-metas             57
metas                    2371
pointers  (fresh)           0
pointers (reused)           0

  Finished Data.Container.Any.
  Checking Data.Container.FreeMonad (/home/abel/agda/agda-stdlib/src/Data/Container/FreeMonad.agda).
Ticks for Data.Container.FreeMonad
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        674
Integer (reused)       7970
Node  (fresh)          6485
Node (reused)         87152
String  (fresh)         207
String (reused)       24359
attempted-constraints     9
max-open-constraints      2
max-open-metas            8
metas                    87
pointers  (fresh)         0
pointers (reused)         0

  Finished Data.Container.FreeMonad.
  Checking Data.Container.Indexed (/home/abel/agda/agda-stdlib/src/Data/Container/Indexed.agda).
   Checking Data.W.Indexed (/home/abel/agda/agda-stdlib/src/Data/W/Indexed.agda).
    Checking Data.Container.Indexed.Core (/home/abel/agda/agda-stdlib/src/Data/Container/Indexed/Core.agda).
Ticks for Data.Container.Indexed.Core
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        614
Integer (reused)       6098
Node  (fresh)          4381
Node (reused)         62265
String  (fresh)         118
String (reused)       18674
attempted-constraints     8
max-open-constraints      1
max-open-metas           10
metas                    98
pointers  (fresh)         0
pointers (reused)         0

    Finished Data.Container.Indexed.Core.
Ticks for Data.W.Indexed
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        672
Integer (reused)       8134
Node  (fresh)          4728
Node (reused)         81291
String  (fresh)         117
String (reused)       22357
attempted-constraints    31
max-open-constraints      5
max-open-metas           12
metas                   132
pointers  (fresh)         0
pointers (reused)         0

   Finished Data.W.Indexed.
   Checking Data.M.Indexed (/home/abel/agda/agda-stdlib/src/Data/M/Indexed.agda).
Ticks for Data.M.Indexed
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        503
Integer (reused)       8902
Node  (fresh)          5248
Node (reused)         90529
String  (fresh)         151
String (reused)       23869
attempted-constraints    16
max-open-constraints      1
max-open-metas           10
metas                    99
pointers  (fresh)         0
pointers (reused)         0

   Finished Data.M.Indexed.
Ticks for Data.Container.Indexed
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         5527
Integer (reused)       142915
Node  (fresh)           41675
Node (reused)         1449402
String  (fresh)           452
String (reused)        401365
attempted-constraints     334
max-open-constraints        6
max-open-metas             33
metas                    2196
pointers  (fresh)           0
pointers (reused)           0

  Finished Data.Container.Indexed.
  Checking Data.Container.Indexed.Combinator (/home/abel/agda/agda-stdlib/src/Data/Container/Indexed/Combinator.agda).
Ticks for Data.Container.Indexed.Combinator
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        4804
Integer (reused)       86394
Node  (fresh)          29254
Node (reused)         905539
String  (fresh)          357
String (reused)       253653
attempted-constraints    540
max-open-constraints      16
max-open-metas            25
metas                   1864
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Container.Indexed.Combinator.
  Checking Data.Container.Indexed.FreeMonad (/home/abel/agda/agda-stdlib/src/Data/Container/Indexed/FreeMonad.agda).
Ticks for Data.Container.Indexed.FreeMonad
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         903
Integer (reused)       42015
Node  (fresh)          13053
Node (reused)         422870
String  (fresh)          279
String (reused)       135920
attempted-constraints     54
max-open-constraints       6
max-open-metas            19
metas                    203
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Container.Indexed.FreeMonad.
  Checking Data.Covec (/home/abel/agda/agda-stdlib/src/Data/Covec.agda).
Ticks for Data.Covec
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2508
Integer (reused)       34150
Node  (fresh)          20163
Node (reused)         374616
String  (fresh)          361
String (reused)        83701
attempted-constraints    130
max-open-constraints       7
max-open-metas            17
metas                    520
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Covec.
  Checking Data.DifferenceNat (/home/abel/agda/agda-stdlib/src/Data/DifferenceNat.agda).
Ticks for Data.DifferenceNat
Double  (fresh)          0
Double (reused)          0
Integer  (fresh)       283
Integer (reused)      1856
Node  (fresh)         2288
Node (reused)        22402
String  (fresh)         95
String (reused)       5746
max-open-constraints     0
max-open-metas           6
metas                   19
pointers  (fresh)        0
pointers (reused)        0

  Finished Data.DifferenceNat.
  Checking Data.DifferenceVec (/home/abel/agda/agda-stdlib/src/Data/DifferenceVec.agda).
Ticks for Data.DifferenceVec
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        883
Integer (reused)       4707
Node  (fresh)          5375
Node (reused)         54224
String  (fresh)         160
String (reused)       12395
attempted-constraints    10
max-open-constraints      5
max-open-metas            8
metas                   153
pointers  (fresh)         0
pointers (reused)         0

  Finished Data.DifferenceVec.
  Checking Data.Fin.Props (/home/abel/agda/agda-stdlib/src/Data/Fin/Props.agda).
Ticks for Data.Fin.Props
Double  (fresh)          0
Double (reused)          0
Integer  (fresh)        57
Integer (reused)       970
Node  (fresh)          605
Node (reused)        12283
String  (fresh)         29
String (reused)       4588
max-open-constraints     0
metas                    0
pointers  (fresh)        0
pointers (reused)        0

  Finished Data.Fin.Props.
  Checking Data.Fin.Subset.Props (/home/abel/agda/agda-stdlib/src/Data/Fin/Subset/Props.agda).
Ticks for Data.Fin.Subset.Props
Double  (fresh)          0
Double (reused)          0
Integer  (fresh)        67
Integer (reused)      1903
Node  (fresh)          863
Node (reused)        20096
String  (fresh)         49
String (reused)       8499
max-open-constraints     0
metas                    0
pointers  (fresh)        0
pointers (reused)        0

  Finished Data.Fin.Subset.Props.
  Checking Data.Fin.Substitution (/home/abel/agda/agda-stdlib/src/Data/Fin/Substitution.agda).
   Checking Data.Star (/home/abel/agda/agda-stdlib/src/Data/Star.agda).
Ticks for Data.Star
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2203
Integer (reused)       16462
Node  (fresh)          12873
Node (reused)         184209
String  (fresh)          197
String (reused)        41014
attempted-constraints    249
max-open-constraints       5
max-open-metas            16
metas                    786
pointers  (fresh)          0
pointers (reused)          0

   Finished Data.Star.
Ticks for Data.Fin.Substitution
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1731
Integer (reused)       41114
Node  (fresh)          13507
Node (reused)         414619
String  (fresh)          221
String (reused)       115481
attempted-constraints     14
max-open-constraints       2
max-open-metas            15
metas                    251
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Fin.Substitution.
  Checking Data.Fin.Substitution.Example (/home/abel/agda/agda-stdlib/src/Data/Fin/Substitution/Example.agda).
   Checking Data.Fin.Substitution.Lemmas (/home/abel/agda/agda-stdlib/src/Data/Fin/Substitution/Lemmas.agda).
Ticks for Data.Fin.Substitution.Lemmas
Double  (fresh)              0
Double (reused)              0
Integer  (fresh)          9193
Integer (reused)       1722741
Node  (fresh)           112645
Node (reused)         17511083
String  (fresh)            433
String (reused)        5670537
attempted-constraints      613
max-open-constraints         6
max-open-metas              37
metas                     3679
pointers  (fresh)            0
pointers (reused)            0

   Finished Data.Fin.Substitution.Lemmas.
Ticks for Data.Fin.Substitution.Example
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1694
Integer (reused)      134127
Node  (fresh)          27345
Node (reused)        1279639
String  (fresh)          335
String (reused)       458461
max-open-constraints       0
max-open-metas            18
metas                    308
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Fin.Substitution.Example.
  Checking Data.Fin.Substitution.List (/home/abel/agda/agda-stdlib/src/Data/Fin/Substitution/List.agda).
   Checking Data.List.Properties (/home/abel/agda/agda-stdlib/src/Data/List/Properties.agda).
    Checking Data.List.All (/home/abel/agda/agda-stdlib/src/Data/List/All.agda).
Ticks for Data.List.All
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1093
Integer (reused)       10744
Node  (fresh)           9223
Node (reused)         117571
String  (fresh)          275
String (reused)        34272
attempted-constraints     49
max-open-constraints       4
max-open-metas            15
metas                    208
pointers  (fresh)          0
pointers (reused)          0

    Finished Data.List.All.
Ticks for Data.List.Properties
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         9932
Integer (reused)       239690
Node  (fresh)           78435
Node (reused)         2540870
String  (fresh)           780
String (reused)        591325
attempted-constraints    1053
max-open-constraints        9
max-open-metas             31
metas                    4155
pointers  (fresh)           0
pointers (reused)           0

   Finished Data.List.Properties.
Ticks for Data.Fin.Substitution.List
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         932
Integer (reused)       88544
Node  (fresh)          22171
Node (reused)         888752
String  (fresh)          321
String (reused)       318709
attempted-constraints     15
max-open-constraints       2
max-open-metas            18
metas                    111
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Fin.Substitution.List.
  Checking Data.Float (/home/abel/agda/agda-stdlib/src/Data/Float.agda).
Ticks for Data.Float
Double  (fresh)          0
Double (reused)          0
Integer  (fresh)       245
Integer (reused)      3025
Node  (fresh)         2607
Node (reused)        31651
String  (fresh)        102
String (reused)       9960
max-open-constraints     0
max-open-metas           4
metas                   14
pointers  (fresh)        0
pointers (reused)        0

  Finished Data.Float.
  Checking Data.Graph.Acyclic (/home/abel/agda/agda-stdlib/src/Data/Graph/Acyclic.agda).
Ticks for Data.Graph.Acyclic
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        3838
Integer (reused)       39322
Node  (fresh)          25488
Node (reused)         406288
String  (fresh)          536
String (reused)       106689
attempted-constraints     52
max-open-constraints       3
max-open-metas            26
metas                    785
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Graph.Acyclic.
  Checking Data.Integer.Divisibility (/home/abel/agda/agda-stdlib/src/Data/Integer/Divisibility.agda).
   Checking Data.Nat.Divisibility (/home/abel/agda/agda-stdlib/src/Data/Nat/Divisibility.agda).
Ticks for Data.Nat.Divisibility
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         3010
Integer (reused)       114164
Node  (fresh)           37182
Node (reused)         1178444
String  (fresh)           621
String (reused)        311021
attempted-constraints      30
max-open-constraints        2
max-open-metas             14
metas                     450
pointers  (fresh)           0
pointers (reused)           0

   Finished Data.Nat.Divisibility.
   Checking Data.Nat.Coprimality (/home/abel/agda/agda-stdlib/src/Data/Nat/Coprimality.agda).
    Checking Data.Nat.Primality (/home/abel/agda/agda-stdlib/src/Data/Nat/Primality.agda).
Ticks for Data.Nat.Primality
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        387
Integer (reused)       6793
Node  (fresh)          5627
Node (reused)         79719
String  (fresh)         209
String (reused)       25710
attempted-constraints     1
max-open-constraints      1
max-open-metas            7
metas                    19
pointers  (fresh)         0
pointers (reused)         0

    Finished Data.Nat.Primality.
    Checking Data.Nat.GCD (/home/abel/agda/agda-stdlib/src/Data/Nat/GCD.agda).
     Checking Induction.Lexicographic (/home/abel/agda/agda-stdlib/src/Induction/Lexicographic.agda).
Ticks for Induction.Lexicographic
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1101
Integer (reused)        9821
Node  (fresh)           7354
Node (reused)         112322
String  (fresh)          186
String (reused)        24396
attempted-constraints     94
max-open-constraints      13
max-open-metas            15
metas                    180
pointers  (fresh)          0
pointers (reused)          0

     Finished Induction.Lexicographic.
     Checking Data.Nat.GCD.Lemmas (/home/abel/agda/agda-stdlib/src/Data/Nat/GCD/Lemmas.agda).
Ticks for Data.Nat.GCD.Lemmas
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         4089
Integer (reused)       223162
Node  (fresh)           25976
Node (reused)         2321360
String  (fresh)           333
String (reused)        630309
attempted-constraints       1
max-open-constraints        1
max-open-metas             26
metas                     759
pointers  (fresh)           0
pointers (reused)           0

     Finished Data.Nat.GCD.Lemmas.
Ticks for Data.Nat.GCD
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2705
Integer (reused)       54864
Node  (fresh)          21470
Node (reused)         562367
String  (fresh)          379
String (reused)       155297
attempted-constraints     37
max-open-constraints       5
max-open-metas            15
metas                    321
pointers  (fresh)          0
pointers (reused)          0

    Finished Data.Nat.GCD.
Ticks for Data.Nat.Coprimality
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2764
Integer (reused)       66252
Node  (fresh)          34816
Node (reused)         692337
String  (fresh)          671
String (reused)       185119
attempted-constraints     42
max-open-constraints       4
max-open-metas            14
metas                    395
pointers  (fresh)          0
pointers (reused)          0

   Finished Data.Nat.Coprimality.
Ticks for Data.Integer.Divisibility
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         614
Integer (reused)       15205
Node  (fresh)          10587
Node (reused)         163918
String  (fresh)          333
String (reused)        49779
attempted-constraints      3
max-open-constraints       1
max-open-metas             7
metas                     34
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Integer.Divisibility.
  Checking Data.List.All.Properties (/home/abel/agda/agda-stdlib/src/Data/List/All/Properties.agda).
Ticks for Data.List.All.Properties
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2884
Integer (reused)       44625
Node  (fresh)          23847
Node (reused)         494201
String  (fresh)          457
String (reused)       137745
attempted-constraints    282
max-open-constraints       7
max-open-metas            27
metas                    985
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.List.All.Properties.
  Checking Data.List.Any.BagAndSetEquality (/home/abel/agda/agda-stdlib/src/Data/List/Any/BagAndSetEquality.agda).
   Checking Data.List.Any.Properties (/home/abel/agda/agda-stdlib/src/Data/List/Any/Properties.agda).
Ticks for Data.List.Any.Properties
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)        12088
Integer (reused)       297490
Node  (fresh)           92868
Node (reused)         3224169
String  (fresh)           970
String (reused)        844678
attempted-constraints    1536
max-open-constraints       25
max-open-metas             51
metas                    4691
pointers  (fresh)           0
pointers (reused)           0

   Finished Data.List.Any.Properties.
Ticks for Data.List.Any.BagAndSetEquality
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         5224
Integer (reused)       163005
Node  (fresh)           54882
Node (reused)         1715564
String  (fresh)           862
String (reused)        454321
attempted-constraints    1524
max-open-constraints       26
max-open-metas             41
metas                    1927
pointers  (fresh)           0
pointers (reused)           0

  Finished Data.List.Any.BagAndSetEquality.
  Checking Data.List.Any.Membership (/home/abel/agda/agda-stdlib/src/Data/List/Any/Membership.agda).
   Checking Relation.Binary.Properties.DecTotalOrder (/home/abel/agda/agda-stdlib/src/Relation/Binary/Properties/DecTotalOrder.agda).
    Checking Relation.Binary.NonStrictToStrict (/home/abel/agda/agda-stdlib/src/Relation/Binary/NonStrictToStrict.agda).
Ticks for Relation.Binary.NonStrictToStrict
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1488
Integer (reused)       38702
Node  (fresh)          17087
Node (reused)         402894
String  (fresh)          243
String (reused)        91133
attempted-constraints    121
max-open-constraints       5
max-open-metas            16
metas                    353
pointers  (fresh)          0
pointers (reused)          0

    Finished Relation.Binary.NonStrictToStrict.
Ticks for Relation.Binary.Properties.DecTotalOrder
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         525
Integer (reused)       36516
Node  (fresh)          10848
Node (reused)         359563
String  (fresh)          130
String (reused)        97969
attempted-constraints      7
max-open-constraints       4
max-open-metas             7
metas                     35
pointers  (fresh)          0
pointers (reused)          0

   Finished Relation.Binary.Properties.DecTotalOrder.
Ticks for Data.List.Any.Membership
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         5419
Integer (reused)       241407
Node  (fresh)           64664
Node (reused)         2513054
String  (fresh)           949
String (reused)        654447
attempted-constraints     498
max-open-constraints       18
max-open-metas             38
metas                    2236
pointers  (fresh)           0
pointers (reused)           0

  Finished Data.List.Any.Membership.
  Checking Data.List.Countdown (/home/abel/agda/agda-stdlib/src/Data/List/Countdown.agda).
Ticks for Data.List.Countdown
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         4108
Integer (reused)       110281
Node  (fresh)           37087
Node (reused)         1139011
String  (fresh)           482
String (reused)        291141
attempted-constraints      57
max-open-constraints        5
max-open-metas             18
metas                     576
pointers  (fresh)           0
pointers (reused)           0

  Finished Data.List.Countdown.
  Checking Data.List.NonEmpty.Properties (/home/abel/agda/agda-stdlib/src/Data/List/NonEmpty/Properties.agda).
Ticks for Data.List.NonEmpty.Properties
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         784
Integer (reused)       21551
Node  (fresh)          10740
Node (reused)         227211
String  (fresh)          278
String (reused)        67004
attempted-constraints     18
max-open-constraints       1
max-open-metas            20
metas                    160
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.List.NonEmpty.Properties.
  Checking Data.List.Reverse (/home/abel/agda/agda-stdlib/src/Data/List/Reverse.agda).
Ticks for Data.List.Reverse
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        740
Integer (reused)      11039
Node  (fresh)          8411
Node (reused)        124370
String  (fresh)         336
String (reused)       37812
max-open-constraints      0
max-open-metas            7
metas                    69
pointers  (fresh)         0
pointers (reused)         0

  Finished Data.List.Reverse.
  Checking Data.Nat.InfinitelyOften (/home/abel/agda/agda-stdlib/src/Data/Nat/InfinitelyOften.agda).
Ticks for Data.Nat.InfinitelyOften
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1529
Integer (reused)       42455
Node  (fresh)          22622
Node (reused)         455306
String  (fresh)          588
String (reused)       120087
attempted-constraints     62
max-open-constraints       6
max-open-metas            25
metas                    302
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Nat.InfinitelyOften.
  Checking Data.Nat.LCM (/home/abel/agda/agda-stdlib/src/Data/Nat/LCM.agda).
Ticks for Data.Nat.LCM
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         2291
Integer (reused)       219885
Node  (fresh)           32823
Node (reused)         2297376
String  (fresh)           633
String (reused)        579436
attempted-constraints      10
max-open-constraints        3
max-open-metas             19
metas                     214
pointers  (fresh)           0
pointers (reused)           0

  Finished Data.Nat.LCM.
  Checking Data.Product.N-ary (/home/abel/agda/agda-stdlib/src/Data/Product/N-ary.agda).
Ticks for Data.Product.N-ary
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         902
Integer (reused)       12613
Node  (fresh)           9081
Node (reused)         139392
String  (fresh)          245
String (reused)        39371
attempted-constraints      9
max-open-constraints       2
max-open-metas             8
metas                    131
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Product.N-ary.
  Checking Data.Rational (/home/abel/agda/agda-stdlib/src/Data/Rational.agda).
Ticks for Data.Rational
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         2760
Integer (reused)       156156
Node  (fresh)           39743
Node (reused)         1586762
String  (fresh)           641
String (reused)        366581
attempted-constraints      94
max-open-constraints        5
max-open-metas             19
metas                     432
pointers  (fresh)           0
pointers (reused)           0

  Finished Data.Rational.
  Checking Data.ReflexiveClosure (/home/abel/agda/agda-stdlib/src/Data/ReflexiveClosure.agda).
   Checking Relation.Binary.Simple (/home/abel/agda/agda-stdlib/src/Relation/Binary/Simple.agda).
Ticks for Relation.Binary.Simple
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         559
Integer (reused)       10400
Node  (fresh)           6765
Node (reused)         108635
String  (fresh)          151
String (reused)        29926
attempted-constraints      6
max-open-constraints       2
max-open-metas             7
metas                     49
pointers  (fresh)          0
pointers (reused)          0

   Finished Relation.Binary.Simple.
Ticks for Data.ReflexiveClosure
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         760
Integer (reused)       11714
Node  (fresh)           7898
Node (reused)         124117
String  (fresh)          171
String (reused)        32361
attempted-constraints     27
max-open-constraints       2
max-open-metas            10
metas                    110
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.ReflexiveClosure.
  Checking Data.Star.BoundedVec (/home/abel/agda/agda-stdlib/src/Data/Star/BoundedVec.agda).
   Checking Data.Star.Nat (/home/abel/agda/agda-stdlib/src/Data/Star/Nat.agda).
Ticks for Data.Star.Nat
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         658
Integer (reused)       13761
Node  (fresh)           8272
Node (reused)         143101
String  (fresh)          195
String (reused)        38913
attempted-constraints      9
max-open-constraints       2
max-open-metas            14
metas                     95
pointers  (fresh)          0
pointers (reused)          0

   Finished Data.Star.Nat.
   Checking Data.Star.Decoration (/home/abel/agda/agda-stdlib/src/Data/Star/Decoration.agda).
Ticks for Data.Star.Decoration
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1673
Integer (reused)       22372
Node  (fresh)          12203
Node (reused)         241271
String  (fresh)          225
String (reused)        63508
attempted-constraints     70
max-open-constraints       4
max-open-metas            17
metas                    510
pointers  (fresh)          0
pointers (reused)          0

   Finished Data.Star.Decoration.
   Checking Data.Star.Pointer (/home/abel/agda/agda-stdlib/src/Data/Star/Pointer.agda).
Ticks for Data.Star.Pointer
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1688
Integer (reused)       26978
Node  (fresh)          13318
Node (reused)         284750
String  (fresh)          259
String (reused)        75542
attempted-constraints     55
max-open-constraints       4
max-open-metas            19
metas                    454
pointers  (fresh)          0
pointers (reused)          0

   Finished Data.Star.Pointer.
   Checking Data.Star.List (/home/abel/agda/agda-stdlib/src/Data/Star/List.agda).
Ticks for Data.Star.List
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        213
Integer (reused)       2373
Node  (fresh)          2075
Node (reused)         26780
String  (fresh)          70
String (reused)        8211
attempted-constraints     5
max-open-constraints      2
max-open-metas           11
metas                    40
pointers  (fresh)         0
pointers (reused)         0

   Finished Data.Star.List.
Ticks for Data.Star.BoundedVec
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         869
Integer (reused)       23810
Node  (fresh)          11018
Node (reused)         244452
String  (fresh)          258
String (reused)        65447
attempted-constraints     19
max-open-constraints       2
max-open-metas            19
metas                    147
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Star.BoundedVec.
  Checking Data.Star.Environment (/home/abel/agda/agda-stdlib/src/Data/Star/Environment.agda).
Ticks for Data.Star.Environment
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        419
Integer (reused)       6173
Node  (fresh)          4314
Node (reused)         67938
String  (fresh)         150
String (reused)       20981
attempted-constraints    12
max-open-constraints      2
max-open-metas           13
metas                    91
pointers  (fresh)         0
pointers (reused)         0

  Finished Data.Star.Environment.
  Checking Data.Star.Fin (/home/abel/agda/agda-stdlib/src/Data/Star/Fin.agda).
Ticks for Data.Star.Fin
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        214
Integer (reused)       3003
Node  (fresh)          2139
Node (reused)         32171
String  (fresh)          78
String (reused)        9390
attempted-constraints    10
max-open-constraints      2
max-open-metas           11
metas                    36
pointers  (fresh)         0
pointers (reused)         0

  Finished Data.Star.Fin.
  Checking Data.Star.Properties (/home/abel/agda/agda-stdlib/src/Data/Star/Properties.agda).
Ticks for Data.Star.Properties
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2109
Integer (reused)       23134
Node  (fresh)          16066
Node (reused)         267361
String  (fresh)          257
String (reused)        64853
attempted-constraints    346
max-open-constraints      10
max-open-metas            22
metas                    870
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Star.Properties.
  Checking Data.Star.Vec (/home/abel/agda/agda-stdlib/src/Data/Star/Vec.agda).
Ticks for Data.Star.Vec
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         911
Integer (reused)       19409
Node  (fresh)          10509
Node (reused)         200015
String  (fresh)          248
String (reused)        55422
attempted-constraints      5
max-open-constraints       2
max-open-metas            12
metas                    111
pointers  (fresh)          0
pointers (reused)          0

  Finished Data.Star.Vec.
  Checking Irrelevance (/home/abel/agda/agda-stdlib/src/Irrelevance.agda).
Ticks for Irrelevance
Double  (fresh)         0
Double (reused)         0
Integer  (fresh)       81
Integer (reused)      179
Node  (fresh)         430
Node (reused)        2185
String  (fresh)        17
String (reused)       337
max-open-constraints    0
max-open-metas          2
metas                   6
pointers  (fresh)       0
pointers (reused)       0

  Finished Irrelevance.
  Checking Reflection (/home/abel/agda/agda-stdlib/src/Reflection.agda).
Ticks for Reflection
Double  (fresh)             0
Double (reused)             0
Integer  (fresh)         8521
Integer (reused)        95944
Node  (fresh)           56437
Node (reused)         1052845
String  (fresh)           566
String (reused)        215365
attempted-constraints     153
max-open-constraints        5
max-open-metas             19
metas                    1432
pointers  (fresh)           0
pointers (reused)           0

  Finished Reflection.
  Checking Relation.Binary.Flip (/home/abel/agda/agda-stdlib/src/Relation/Binary/Flip.agda).
Ticks for Relation.Binary.Flip
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        3215
Integer (reused)       86345
Node  (fresh)          29193
Node (reused)         828539
String  (fresh)          248
String (reused)       187399
attempted-constraints    297
max-open-constraints       2
max-open-metas            13
metas                   1008
pointers  (fresh)          0
pointers (reused)          0

  Finished Relation.Binary.Flip.
  Checking Relation.Binary.List.NonStrictLex (/home/abel/agda/agda-stdlib/src/Relation/Binary/List/NonStrictLex.agda).
Ticks for Relation.Binary.List.NonStrictLex
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2212
Integer (reused)       57915
Node  (fresh)          20374
Node (reused)         566249
String  (fresh)          304
String (reused)       154161
attempted-constraints    107
max-open-constraints       2
max-open-metas            17
metas                    817
pointers  (fresh)          0
pointers (reused)          0

  Finished Relation.Binary.List.NonStrictLex.
  Checking Relation.Binary.OrderMorphism (/home/abel/agda/agda-stdlib/src/Relation/Binary/OrderMorphism.agda).
Ticks for Relation.Binary.OrderMorphism
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         840
Integer (reused)       14104
Node  (fresh)           8117
Node (reused)         146471
String  (fresh)          182
String (reused)        38464
attempted-constraints     35
max-open-constraints       2
max-open-metas            19
metas                    207
pointers  (fresh)          0
pointers (reused)          0

  Finished Relation.Binary.OrderMorphism.
  Checking Relation.Binary.Product.NonStrictLex (/home/abel/agda/agda-stdlib/src/Relation/Binary/Product/NonStrictLex.agda).
   Checking Relation.Binary.Product.StrictLex (/home/abel/agda/agda-stdlib/src/Relation/Binary/Product/StrictLex.agda).
    Checking Relation.Nullary.Sum (/home/abel/agda/agda-stdlib/src/Relation/Nullary/Sum.agda).
Ticks for Relation.Nullary.Sum
Double  (fresh)          0
Double (reused)          0
Integer  (fresh)       328
Integer (reused)      2173
Node  (fresh)         2277
Node (reused)        24663
String  (fresh)         55
String (reused)       6884
max-open-constraints     0
max-open-metas           5
metas                   30
pointers  (fresh)        0
pointers (reused)        0

    Finished Relation.Nullary.Sum.
Ticks for Relation.Binary.Product.StrictLex
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        4164
Integer (reused)       70555
Node  (fresh)          27906
Node (reused)         754845
String  (fresh)          349
String (reused)       179018
attempted-constraints    483
max-open-constraints       7
max-open-metas            21
metas                   1454
pointers  (fresh)          0
pointers (reused)          0

   Finished Relation.Binary.Product.StrictLex.
Ticks for Relation.Binary.Product.NonStrictLex
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2483
Integer (reused)       61630
Node  (fresh)          23038
Node (reused)         622211
String  (fresh)          307
String (reused)       148546
attempted-constraints    266
max-open-constraints       6
max-open-metas            24
metas                    825
pointers  (fresh)          0
pointers (reused)          0

  Finished Relation.Binary.Product.NonStrictLex.
  Checking Relation.Binary.Properties.Poset (/home/abel/agda/agda-stdlib/src/Relation/Binary/Properties/Poset.agda).
Ticks for Relation.Binary.Properties.Poset
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         516
Integer (reused)       26980
Node  (fresh)           9181
Node (reused)         264279
String  (fresh)          128
String (reused)        73493
attempted-constraints      8
max-open-constraints       4
max-open-metas             7
metas                     29
pointers  (fresh)          0
pointers (reused)          0

  Finished Relation.Binary.Properties.Poset.
  Checking Relation.Binary.Properties.Preorder (/home/abel/agda/agda-stdlib/src/Relation/Binary/Properties/Preorder.agda).
Ticks for Relation.Binary.Properties.Preorder
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         520
Integer (reused)       14281
Node  (fresh)           7501
Node (reused)         146906
String  (fresh)          164
String (reused)        40962
attempted-constraints     13
max-open-constraints       3
max-open-metas            18
metas                     52
pointers  (fresh)          0
pointers (reused)          0

  Finished Relation.Binary.Properties.Preorder.
  Checking Relation.Binary.Properties.StrictPartialOrder (/home/abel/agda/agda-stdlib/src/Relation/Binary/Properties/StrictPartialOrder.agda).
   Checking Relation.Binary.StrictToNonStrict (/home/abel/agda/agda-stdlib/src/Relation/Binary/StrictToNonStrict.agda).
Ticks for Relation.Binary.StrictToNonStrict
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        1517
Integer (reused)       25822
Node  (fresh)          15653
Node (reused)         281828
String  (fresh)          239
String (reused)        69320
attempted-constraints     74
max-open-constraints       2
max-open-metas             9
metas                    266
pointers  (fresh)          0
pointers (reused)          0

   Finished Relation.Binary.StrictToNonStrict.
Ticks for Relation.Binary.Properties.StrictPartialOrder
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         542
Integer (reused)       26291
Node  (fresh)           8908
Node (reused)         257566
String  (fresh)          123
String (reused)        72033
attempted-constraints      8
max-open-constraints       4
max-open-metas             7
metas                     39
pointers  (fresh)          0
pointers (reused)          0

  Finished Relation.Binary.Properties.StrictPartialOrder.
  Checking Relation.Binary.Properties.StrictTotalOrder (/home/abel/agda/agda-stdlib/src/Relation/Binary/Properties/StrictTotalOrder.agda).
Ticks for Relation.Binary.Properties.StrictTotalOrder
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         562
Integer (reused)       36226
Node  (fresh)          10994
Node (reused)         360235
String  (fresh)          136
String (reused)        99111
attempted-constraints      8
max-open-constraints       4
max-open-metas             9
metas                     27
pointers  (fresh)          0
pointers (reused)          0

  Finished Relation.Binary.Properties.StrictTotalOrder.
  Checking Relation.Binary.Properties.TotalOrder (/home/abel/agda/agda-stdlib/src/Relation/Binary/Properties/TotalOrder.agda).
Ticks for Relation.Binary.Properties.TotalOrder
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         471
Integer (reused)       15613
Node  (fresh)           7254
Node (reused)         155825
String  (fresh)          128
String (reused)        43852
attempted-constraints      6
max-open-constraints       2
max-open-metas             8
metas                     33
pointers  (fresh)          0
pointers (reused)          0

  Finished Relation.Binary.Properties.TotalOrder.
  Checking Relation.Binary.Props.DecTotalOrder (/home/abel/agda/agda-stdlib/src/Relation/Binary/Props/DecTotalOrder.agda).
Ticks for Relation.Binary.Props.DecTotalOrder
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         437
Integer (reused)       19932
Node  (fresh)           7418
Node (reused)         199119
String  (fresh)          115
String (reused)        56546
attempted-constraints      1
max-open-constraints       1
max-open-metas             7
metas                     10
pointers  (fresh)          0
pointers (reused)          0

  Finished Relation.Binary.Props.DecTotalOrder.
  Checking Relation.Binary.Props.Poset (/home/abel/agda/agda-stdlib/src/Relation/Binary/Props/Poset.agda).
Ticks for Relation.Binary.Props.Poset
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        413
Integer (reused)       8931
Node  (fresh)          5481
Node (reused)         92845
String  (fresh)         111
String (reused)       26766
attempted-constraints     1
max-open-constraints      1
max-open-metas            7
metas                    10
pointers  (fresh)         0
pointers (reused)         0

  Finished Relation.Binary.Props.Poset.
  Checking Relation.Binary.Props.Preorder (/home/abel/agda/agda-stdlib/src/Relation/Binary/Props/Preorder.agda).
Ticks for Relation.Binary.Props.Preorder
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        415
Integer (reused)       8923
Node  (fresh)          5469
Node (reused)         92815
String  (fresh)         112
String (reused)       26765
attempted-constraints     1
max-open-constraints      1
max-open-metas            7
metas                    10
pointers  (fresh)         0
pointers (reused)         0

  Finished Relation.Binary.Props.Preorder.
  Checking Relation.Binary.Props.StrictPartialOrder (/home/abel/agda/agda-stdlib/src/Relation/Binary/Props/StrictPartialOrder.agda).
Ticks for Relation.Binary.Props.StrictPartialOrder
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         434
Integer (reused)       16212
Node  (fresh)           6724
Node (reused)         161498
String  (fresh)          113
String (reused)        46608
attempted-constraints      1
max-open-constraints       1
max-open-metas             7
metas                     10
pointers  (fresh)          0
pointers (reused)          0

  Finished Relation.Binary.Props.StrictPartialOrder.
  Checking Relation.Binary.Props.StrictTotalOrder (/home/abel/agda/agda-stdlib/src/Relation/Binary/Props/StrictTotalOrder.agda).
Ticks for Relation.Binary.Props.StrictTotalOrder
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         449
Integer (reused)       21926
Node  (fresh)           7738
Node (reused)         220382
String  (fresh)          115
String (reused)        62909
attempted-constraints      1
max-open-constraints       1
max-open-metas             7
metas                     10
pointers  (fresh)          0
pointers (reused)          0

  Finished Relation.Binary.Props.StrictTotalOrder.
  Checking Relation.Binary.Props.TotalOrder (/home/abel/agda/agda-stdlib/src/Relation/Binary/Props/TotalOrder.agda).
Ticks for Relation.Binary.Props.TotalOrder
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        412
Integer (reused)       9050
Node  (fresh)          5531
Node (reused)         93976
String  (fresh)         113
String (reused)       27076
attempted-constraints     1
max-open-constraints      1
max-open-metas            7
metas                    10
pointers  (fresh)         0
pointers (reused)         0

  Finished Relation.Binary.Props.TotalOrder.
  Checking Relation.Binary.SetoidReasoning (/home/abel/agda/agda-stdlib/src/Relation/Binary/SetoidReasoning.agda).
Ticks for Relation.Binary.SetoidReasoning
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         777
Integer (reused)       10665
Node  (fresh)           6718
Node (reused)         111895
String  (fresh)          131
String (reused)        31938
attempted-constraints     18
max-open-constraints       1
max-open-metas             5
metas                     75
pointers  (fresh)          0
pointers (reused)          0

  Finished Relation.Binary.SetoidReasoning.
  Checking Relation.Binary.StrictPartialOrderReasoning (/home/abel/agda/agda-stdlib/src/Relation/Binary/StrictPartialOrderReasoning.agda).
Ticks for Relation.Binary.StrictPartialOrderReasoning
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)         443
Integer (reused)       13063
Node  (fresh)           6617
Node (reused)         132085
String  (fresh)          124
String (reused)        37937
attempted-constraints      2
max-open-constraints       2
max-open-metas             7
metas                     13
pointers  (fresh)          0
pointers (reused)          0

  Finished Relation.Binary.StrictPartialOrderReasoning.
  Checking Relation.Nullary.Implication (/home/abel/agda/agda-stdlib/src/Relation/Nullary/Implication.agda).
Ticks for Relation.Nullary.Implication
Double  (fresh)         0
Double (reused)         0
Integer  (fresh)      190
Integer (reused)      867
Node  (fresh)        1171
Node (reused)        9514
String  (fresh)        30
String (reused)      2903
max-open-constraints    0
max-open-metas          4
metas                  14
pointers  (fresh)       0
pointers (reused)       0

  Finished Relation.Nullary.Implication.
  Checking Relation.Nullary.Universe (/home/abel/agda/agda-stdlib/src/Relation/Nullary/Universe.agda).
Ticks for Relation.Nullary.Universe
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2388
Integer (reused)       42616
Node  (fresh)          23608
Node (reused)         460198
String  (fresh)          431
String (reused)       132667
attempted-constraints     51
max-open-constraints       2
max-open-metas            17
metas                    392
pointers  (fresh)          0
pointers (reused)          0

  Finished Relation.Nullary.Universe.
  Checking Size (/home/abel/agda/agda-stdlib/src/Size.agda).
Ticks for Size
Double  (fresh)         0
Double (reused)         0
Integer  (fresh)       88
Integer (reused)      175
Node  (fresh)         274
Node (reused)        2116
String  (fresh)         9
String (reused)       253
max-open-constraints    0
max-open-metas          1
metas                   4
pointers  (fresh)       0
pointers (reused)       0

  Finished Size.
  Checking Universe (/home/abel/agda/agda-stdlib/src/Universe.agda).
Ticks for Universe
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        283
Integer (reused)       2931
Node  (fresh)          2550
Node (reused)         32604
String  (fresh)          71
String (reused)        5409
attempted-constraints     8
max-open-constraints      4
max-open-metas            7
metas                    32
pointers  (fresh)         0
pointers (reused)         0

  Finished Universe.
Ticks for Everything
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2699
Integer (reused)      130382
Node  (fresh)          90858
Node (reused)        1315446
String  (fresh)         2245
String (reused)       443242
max-open-constraints       0
metas                      0
pointers  (fresh)          0
pointers (reused)          0

 Finished Everything.
Ticks for README
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)       1425
Integer (reused)      27049
Node  (fresh)         24051
Node (reused)        282209
String  (fresh)         700
String (reused)       71935
max-open-constraints      0
metas                     0
pointers  (fresh)         0
pointers (reused)         0

Finished README.
Total time                 228,250ms
Parsing                      1,340ms
Parsing.Operators           10,644ms
Import                       4,600ms
Deserialization                 28ms
Scoping                      9,048ms
Typing                      52,155ms
Termination                  1,728ms
Termination.Graph              236ms
Termination.RecCheck           508ms
Termination.Compare            292ms
Positivity                   6,292ms
Injectivity                    768ms
ProjectionLikeness             132ms
Coverage                     1,896ms
Highlighting                 7,172ms
Serialization               99,686ms
Serialization.Sort             936ms
Serialization.BinaryEncode  20,621ms
Serialization.Compress       3,760ms
ModuleName                      24ms

 150,045,371,000 bytes allocated in the heap
  17,538,401,152 bytes copied during GC
     419,898,624 bytes maximum residency (46 sample(s))
       5,744,216 bytes maximum slop
            1163 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1733 colls,     0 par   49.69s   49.97s     0.0288s    0.4426s
  Gen  1        46 colls,     0 par   15.72s   15.74s     0.3422s    0.9108s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  161.51s  (162.97s elapsed)
  GC      time   65.41s  ( 65.71s elapsed)
  EXIT    time    0.02s  (  0.03s elapsed)
  Total   time  226.95s  (228.72s elapsed)

  %GC     time      28.8%  (28.7% elapsed)

  Alloc rate    929,015,474 bytes per MUT second

  Productivity  71.2% of total user, 70.6% of total elapsed


real	3m48.838s
user	3m46.954s
sys	0m1.444s



Will KillRange Signature
------------------------------------------------------------------------

  Checking Size (/home/abel/agda/agda-stdlib/src/Size.agda).
Ticks for Size
Double  (fresh)         0
Double (reused)         0
Integer  (fresh)       88
Integer (reused)      175
Node  (fresh)         285
Node (reused)        1925
String  (fresh)         9
String (reused)       213
max-open-constraints    0
max-open-metas          1
metas                   4
pointers  (fresh)       0
pointers (reused)       0

  Finished Size.
  Checking Universe (/home/abel/agda/agda-stdlib/src/Universe.agda).
Ticks for Universe
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)        283
Integer (reused)       2931
Node  (fresh)          2422
Node (reused)         28547
String  (fresh)          71
String (reused)        4173
attempted-constraints     8
max-open-constraints      4
max-open-metas            7
metas                    32
pointers  (fresh)         0
pointers (reused)         0

  Finished Universe.
Ticks for Everything
Double  (fresh)            0
Double (reused)            0
Integer  (fresh)        2699
Integer (reused)      130382
Node  (fresh)          91091
Node (reused)        1200229
String  (fresh)         2245
String (reused)       369272
max-open-constraints       0
metas                      0
pointers  (fresh)          0
pointers (reused)          0

 Finished Everything.
Ticks for README
Double  (fresh)           0
Double (reused)           0
Integer  (fresh)       1425
Integer (reused)      27049
Node  (fresh)         24081
Node (reused)        259418
String  (fresh)         700
String (reused)       63901
max-open-constraints      0
metas                     0
pointers  (fresh)         0
pointers (reused)         0

Finished README.
Total time                 217,437ms
Parsing                      1,300ms
Parsing.Operators           10,492ms
Import                       3,596ms
Deserialization                  8ms
Scoping                      9,092ms
Typing                      55,399ms
Termination                  1,744ms
Termination.Graph              268ms
Termination.RecCheck           584ms
Termination.Compare            200ms
Positivity                   4,624ms
Injectivity                  1,236ms
ProjectionLikeness             148ms
Coverage                     2,016ms
Highlighting                 8,464ms
Serialization               90,853ms
Serialization.Sort             808ms
Serialization.BinaryEncode  18,277ms
Serialization.Compress       3,636ms
ModuleName                      24ms

 141,368,357,984 bytes allocated in the heap
  16,321,623,848 bytes copied during GC
     598,324,120 bytes maximum residency (39 sample(s))
       7,262,752 bytes maximum slop
            1381 MB total memory in use (17 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      4233 colls,     0 par   47.67s   47.90s     0.0113s    0.4676s
  Gen  1        39 colls,     0 par   23.03s   23.24s     0.5959s    3.6554s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  145.11s  (149.76s elapsed)
  GC      time   70.70s  ( 71.15s elapsed)
  EXIT    time    0.49s  (  0.50s elapsed)
  Total   time  216.30s  (221.41s elapsed)

  %GC     time      32.7%  (32.1% elapsed)

  Alloc rate    974,247,984 bytes per MUT second

  Productivity  67.3% of total user, 65.8% of total elapsed


real	3m41.535s
user	3m36.298s
sys	0m1.768s


Collecting statistics about frequency of nodes (by type) in interface
------------------------------------------------------------------------

 Finished Everything.
Finished README.
Total time                 508,883ms
Parsing                      4,884ms
Parsing.Operators           11,224ms
Import                       5,044ms
Deserialization                 20ms
Scoping                      9,460ms
Typing                      59,891ms
Termination                  1,996ms
Termination.Graph              260ms
Termination.RecCheck           520ms
Termination.Compare            324ms
Positivity                   5,004ms
Injectivity                    904ms
ProjectionLikeness             148ms
Coverage                     2,576ms
Highlighting                 7,436ms
Serialization              367,578ms
Serialization.Sort             768ms
Serialization.BinaryEncode  17,905ms
Serialization.Compress       3,588ms
ModuleName                      28ms

Accumlated statistics
Double  (fresh)                                                    0
Double (reused)                                                    0
Integer  (fresh)                                             461,937
Integer (reused)                                          14,008,517
Node  (fresh)                                              3,729,371
Node (reused)                                            114,550,466
String  (fresh)                                               66,532
String (reused)                                           19,462,807
attempted-constraints                                         24,401
equal terms                                                  147,261
icode ()                                                      27,984
icode (Bool,(Arg Term (Type' Term)))                           1,064
icode (Int,Int)                                                   41
icode (ModuleName,Scope)                                      13,510
icode (ModuleName,Section)                                     1,946
icode (ModuleName,Word64)                                      1,859
icode (Name,LocalVar)                                            184
icode (Name,[AbstractModule])                                 15,626
icode (Name,[AbstractName])                                  164,241
icode (NameSpaceId,NameSpace)                                 54,040
icode (QName,(WithArity CompiledClauses))                      4,865
icode (QName,([Arg Expr Name],(Pattern' Expr)))                    2
icode (QName,Definition)                                      15,783
icode (QName,ModuleName)                                       1,403
icode (Range,MetaInfo)                                       210,240
icode (TermHead,Clause)                                          808
icode (TopLevelModuleName,Integer)                           111,583
icode ([Arg Expr Name],(Pattern' Expr))                            2
icode ([Char],(Builtin ([Char],QName)))                          103
icode ([Char],QName)                                              18
icode Abs (ClauseBodyF Term)                                  80,068
icode Abs (Tele (Dom Term (Type' Term)))                      85,967
icode Abs (Type' Term)                                       130,560
icode Abs Term                                                48,051
icode AbsolutePath                                         6,000,666
icode AbstractModule                                          15,668
icode AbstractName                                           166,100
icode AmbiguousQName                                               4
icode Arg () (Named (Ranged [Char]) Int)                       1,741
icode Arg Expr (Named (Ranged [Char]) (Pattern' Expr))             6
icode Arg Expr Name                                                3
icode Arg Term (Named (Ranged [Char]) Pattern)                88,057
icode Arg Term (Type' Term)                                   18,606
icode Arg Term DisplayTerm                                     3,196
icode Arg Term QName                                             376
icode Arg Term Term                                        1,661,660
icode Arg Term [Char]                                         72,270
icode ArgInfo ()                                               1,741
icode ArgInfo Expr                                                 9
icode ArgInfo Term                                         2,127,109
icode Aspect                                                 210,240
icode Bool                                                   189,227
icode Builtin ([Char],QName)                                     103
icode Case CompiledClauses                                     2,929
icode Char                                                        36
icode Clause                                                  17,542
icode ClauseBodyF Term                                        97,610
icode CompiledClauses                                         19,614
icode CompiledRepresentation                                  15,783
icode CompressedFile                                             227
icode ConHead                                                 93,797
icode CtxId                                                   20,362
icode Definition                                              15,783
icode Defn                                                    15,783
icode Delayed                                                 14,664
icode DisplayForm                                              5,630
icode DisplayTerm                                              9,737
icode Dom Term (Type' Term)                                  216,527
icode Drop Permutation                                           261
icode Elim' Term                                           1,670,134
icode Fixity                                               4,274,166
icode Fixity'                                              4,274,166
icode FunctionInverse' Clause                                 14,664
icode GenPart                                                  4,023
icode HashMap QName Definition                                   227
icode HaskellRepresentation                                       36
icode Hiding                                               2,128,859
icode Induction                                              106,376
icode Int                                                  1,677,573
icode Int32                                               18,021,953
icode Integer                                             14,470,454
icode Interface                                                  227
icode Interval' (Maybe AbsolutePath)                       3,000,333
icode IsAbstract                                              15,757
icode KindOfName                                             166,100
icode Level                                                  533,482
icode LevelAtom                                              411,010
icode Literal                                                  9,549
icode LocalVar                                                   184
icode Map Literal CompiledClauses                              2,929
icode Map ModuleName Scope                                       454
icode Map ModuleName Section                                     227
icode Map Name [AbstractModule]                               54,040
icode Map Name [AbstractName]                                 54,040
icode Map QName (WithArity CompiledClauses)                    2,929
icode Map QName ([Arg Expr Name],(Pattern' Expr))                227
icode Map QName ModuleName                                    13,510
icode Map TermHead Clause                                        478
icode Map [Char] (Builtin ([Char],QName))                        227
icode Maybe (Arg Term (Type' Term))                           17,542
icode Maybe (Bool,(Arg Term (Type' Term)))                     7,056
icode Maybe (Int,Int)                                         14,664
icode Maybe (Ranged [Char])                                   89,804
icode Maybe (TopLevelModuleName,Integer)                     210,240
icode Maybe AbsolutePath                                   6,000,666
icode Maybe Aspect                                           210,240
icode Maybe Bool                                              14,664
icode Maybe Clause                                               382
icode Maybe CompiledClauses                                   17,611
icode Maybe Exp                                               15,783
icode Maybe HaskellExport                                     15,783
icode Maybe HaskellRepresentation                             15,783
icode Maybe Induction                                            121
icode Maybe NameKind                                         115,634
icode Maybe Projection                                        14,664
icode Maybe QName                                             33,030
icode Maybe [Char]                                           226,023
icode MetaInfo                                               210,240
icode ModuleName                                           1,084,747
icode MutualId                                                15,783
icode Name                                                 9,110,302
icode NameId                                               4,611,383
icode NameKind                                               115,634
icode NamePart                                             5,100,727
icode NameSpace                                               54,040
icode NameSpaceId                                             54,040
icode Named (Ranged [Char]) (Pattern' Expr)                        6
icode Named (Ranged [Char]) Int                                1,741
icode Named (Ranged [Char]) Pattern                           88,057
icode Occurrence                                              63,382
icode Open DisplayForm                                         5,630
icode OtherAspect                                                720
icode Pattern                                                 88,057
icode Pattern' Expr                                                8
icode Permutation                                             18,064
icode PlusLevel                                              432,162
icode Polarity                                                63,379
icode Position' (Maybe AbsolutePath)                       6,000,666
icode Precedence                                                 227
icode Projection                                               2,583
icode QName                                                1,389,064
icode Range                                                  210,240
icode Range' (Maybe AbsolutePath)                         13,495,124
icode Ranged [Char]                                           83,565
icode Relevance                                            2,128,859
icode Scope                                                   13,510
icode ScopeInfo                                                  227
icode Section                                                  1,946
icode Set [Char]                                                 227
icode Signature                                                  227
icode Sort                                                   419,697
icode Tele (Dom Term (Type' Term))                           105,576
icode Term                                                 2,567,151
icode TermHead                                                   808
icode TopLevelModuleName                                   6,112,249
icode Type' Term                                             381,597
icode WhyInScope                                             528,033
icode WithArity CompiledClauses                                4,865
icode Word64                                                   2,086
icode [()]                                                     1,741
icode [(Literal,CompiledClauses)]                              2,929
icode [(ModuleName,Scope)]                                       454
icode [(ModuleName,Section)]                                     227
icode [(ModuleName,Word64)]                                      227
icode [(Name,LocalVar)]                                          227
icode [(Name,[AbstractModule])]                               54,040
icode [(Name,[AbstractName])]                                 54,040
icode [(NameSpaceId,NameSpace)]                               13,510
icode [(QName,(WithArity CompiledClauses))]                    2,929
icode [(QName,([Arg Expr Name],(Pattern' Expr)))]                227
icode [(QName,Definition)]                                       227
icode [(QName,ModuleName)]                                    13,510
icode [(Range,MetaInfo)]                                         227
icode [(TermHead,Clause)]                                        478
icode [([Char],(Builtin ([Char],QName)))]                        227
icode [AbstractModule]                                        15,626
icode [AbstractName]                                         164,242
icode [Arg Expr (Named (Ranged [Char]) (Pattern' Expr))]           4
icode [Arg Expr Name]                                              2
icode [Arg Term (Named (Ranged [Char]) Pattern)]              24,598
icode [Arg Term DisplayTerm]                                     807
icode [Arg Term QName]                                           121
icode [Arg Term Term]                                         85,838
icode [Arg Term [Char]]                                       16,285
icode [Char]                                              19,529,339
icode [Clause]                                                14,682
icode [CtxId]                                                  5,630
icode [DisplayTerm]                                              359
icode [Elim' Term]                                         2,113,904
icode [Expr]                                                       9
icode [GenPart]                                            4,274,166
icode [Int]                                                   18,064
icode [Interval' (Maybe AbsolutePath)]                    13,495,124
icode [ModuleName]                                            13,510
icode [NamePart]                                           4,498,919
icode [Name]                                               1,084,747
icode [Occurrence]                                            15,783
icode [Open DisplayForm]                                      15,783
icode [OtherAspect]                                          210,240
icode [PlusLevel]                                            533,482
icode [Polarity]                                              15,783
icode [QName]                                                109,108
icode [RewriteRule]                                           15,783
icode [Term]                                               2,132,739
icode [[Char]]                                             6,112,477
icode [[[Char]]]                                                 227
max-open-constraints                                             806
max-open-metas                                                 3,189
metas                                                        105,898
pointers  (fresh)                                                  0
pointers (reused)                                                  0
unequal terms                                                152,929

 251,644,177,024 bytes allocated in the heap
  21,195,274,144 bytes copied during GC
     566,113,528 bytes maximum residency (50 sample(s))
       7,002,376 bytes maximum slop
            1283 MB total memory in use (16 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      4786 colls,     0 par   78.20s   78.74s     0.0165s    0.4085s
  Gen  1        50 colls,     0 par   40.76s   40.95s     0.8190s    4.0209s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  387.40s  (390.15s elapsed)
  GC      time  118.96s  (119.69s elapsed)
  EXIT    time    0.58s  (  0.58s elapsed)
  Total   time  506.94s  (510.43s elapsed)

  %GC     time      23.5%  (23.4% elapsed)

  Alloc rate    649,571,550 bytes per MUT second

  Productivity  76.5% of total user, 76.0% of total elapsed


real	8m30.563s
user	8m26.944s
sys	0m2.664s



After removing iInsideScope
------------------------------------------------------------------------
  Finished Universe.
 Finished Everything.
Finished README.
Total time                 401,229ms
Parsing                      1,364ms
Parsing.Operators           11,016ms
Import                       4,580ms
Deserialization                 16ms
Scoping                      9,624ms
Typing                      58,499ms
Termination                  2,100ms
Termination.Graph              248ms
Termination.RecCheck           732ms
Termination.Compare            204ms
Positivity                   4,576ms
Injectivity                    904ms
ProjectionLikeness             188ms
Coverage                     2,652ms
Highlighting                 7,692ms
Serialization              274,625ms
Serialization.Sort             464ms
Serialization.BinaryEncode  12,788ms
Serialization.Compress       1,676ms
ModuleName                      24ms

Accumlated statistics
Double  (fresh)                                                   0
Double (reused)                                                   0
Integer  (fresh)                                            411,263
Integer (reused)                                         11,021,103
Node  (fresh)                                             2,072,398
Node (reused)                                            86,053,270
String  (fresh)                                              28,124
String (reused)                                          11,747,768
attempted-constraints                                        24,401
equal terms                                                 147,261
icode ()                                                     27,984
icode (Bool,(Arg Term (Type' Term)))                          1,064
icode (Int,Int)                                                  41
icode (ModuleName,Scope)                                        895
icode (ModuleName,Section)                                    1,946
icode (ModuleName,Word64)                                     1,859
icode (Name,[AbstractModule])                                   441
icode (Name,[AbstractName])                                   6,482
icode (NameSpaceId,NameSpace)                                 3,580
icode (QName,(WithArity CompiledClauses))                     4,865
icode (QName,([Arg Expr Name],(Pattern' Expr)))                   2
icode (QName,Definition)                                     15,783
icode (Range,MetaInfo)                                      210,240
icode (TermHead,Clause)                                         808
icode (TopLevelModuleName,Integer)                          111,583
icode ([Arg Expr Name],(Pattern' Expr))                           2
icode ([Char],(Builtin ([Char],QName)))                         103
icode ([Char],QName)                                             18
icode Abs (ClauseBodyF Term)                                 80,068
icode Abs (Tele (Dom Term (Type' Term)))                     85,967
icode Abs (Type' Term)                                      130,560
icode Abs Term                                               48,051
icode AbsolutePath                                        3,129,812
icode AbstractModule                                            441
icode AbstractName                                            6,597
icode AmbiguousQName                                              4
icode Arg () (Named (Ranged [Char]) Int)                        933
icode Arg Expr (Named (Ranged [Char]) (Pattern' Expr))            6
icode Arg Expr Name                                               3
icode Arg Term (Named (Ranged [Char]) Pattern)               88,057
icode Arg Term (Type' Term)                                  18,606
icode Arg Term DisplayTerm                                    3,196
icode Arg Term QName                                            376
icode Arg Term Term                                       1,661,660
icode Arg Term [Char]                                        72,270
icode ArgInfo ()                                                933
icode ArgInfo Expr                                                9
icode ArgInfo Term                                        2,127,109
icode Aspect                                                210,240
icode Bool                                                  176,612
icode Builtin ([Char],QName)                                    103
icode Case CompiledClauses                                    2,929
icode Char                                                       36
icode Clause                                                 17,542
icode ClauseBodyF Term                                       97,610
icode CompiledClauses                                        19,614
icode CompiledRepresentation                                 15,783
icode CompressedFile                                            227
icode ConHead                                                93,797
icode CtxId                                                  20,362
icode Definition                                             15,783
icode Defn                                                   15,783
icode Delayed                                                14,664
icode DisplayForm                                             5,630
icode DisplayTerm                                             9,737
icode Dom Term (Type' Term)                                 216,527
icode Drop Permutation                                          261
icode Elim' Term                                          1,670,134
icode Fixity                                              3,397,352
icode Fixity'                                             3,397,352
icode FunctionInverse' Clause                                14,664
icode GenPart                                                 1,843
icode HashMap QName Definition                                  227
icode HaskellRepresentation                                      36
icode Hiding                                              2,128,051
icode Induction                                             106,376
icode Int                                                 1,676,455
icode Int32                                               9,409,391
icode Integer                                            11,432,366
icode Interface                                                 227
icode Interval' (Maybe AbsolutePath)                      1,564,906
icode IsAbstract                                             15,757
icode KindOfName                                              6,597
icode Level                                                 533,482
icode LevelAtom                                             411,010
icode Literal                                                 9,549
icode Map Literal CompiledClauses                             2,929
icode Map ModuleName Scope                                      454
icode Map ModuleName Section                                    227
icode Map Name [AbstractModule]                               3,580
icode Map Name [AbstractName]                                 3,580
icode Map QName (WithArity CompiledClauses)                   2,929
icode Map QName ([Arg Expr Name],(Pattern' Expr))               227
icode Map QName ModuleName                                      895
icode Map TermHead Clause                                       478
icode Map [Char] (Builtin ([Char],QName))                       227
icode Maybe (Arg Term (Type' Term))                          17,542
icode Maybe (Bool,(Arg Term (Type' Term)))                    7,056
icode Maybe (Int,Int)                                        14,664
icode Maybe (Ranged [Char])                                  88,996
icode Maybe (TopLevelModuleName,Integer)                    210,240
icode Maybe AbsolutePath                                  3,129,812
icode Maybe Aspect                                          210,240
icode Maybe Bool                                             14,664
icode Maybe Clause                                              382
icode Maybe CompiledClauses                                  17,611
icode Maybe Exp                                              15,783
icode Maybe HaskellExport                                    15,783
icode Maybe HaskellRepresentation                            15,783
icode Maybe Induction                                           121
icode Maybe NameKind                                        115,634
icode Maybe Projection                                       14,664
icode Maybe QName                                            33,030
icode Maybe [Char]                                          226,023
icode MetaInfo                                              210,240
icode ModuleName                                            855,382
icode MutualId                                               15,783
icode Name                                                6,814,256
icode NameId                                              3,530,746
icode NameKind                                              115,634
icode NamePart                                            3,718,531
icode NameSpace                                               3,580
icode NameSpaceId                                             3,580
icode Named (Ranged [Char]) (Pattern' Expr)                       6
icode Named (Ranged [Char]) Int                                 933
icode Named (Ranged [Char]) Pattern                          88,057
icode Occurrence                                             63,382
icode Open DisplayForm                                        5,630
icode OtherAspect                                               720
icode Pattern                                                88,057
icode Pattern' Expr                                               8
icode Permutation                                            18,064
icode PlusLevel                                             432,162
icode Polarity                                               63,379
icode Position' (Maybe AbsolutePath)                      3,129,812
icode Precedence                                                227
icode Projection                                              2,583
icode QName                                                 860,271
icode Range                                                 210,240
icode Range' (Maybe AbsolutePath)                        10,322,264
icode Ranged [Char]                                          83,565
icode Relevance                                           2,128,051
icode Scope                                                     895
icode ScopeInfo                                                 227
icode Section                                                 1,946
icode Set [Char]                                                227
icode Signature                                                 227
icode Sort                                                  419,697
icode Tele (Dom Term (Type' Term))                          105,576
icode Term                                                2,567,151
icode TermHead                                                  808
icode TopLevelModuleName                                  3,241,395
icode Type' Term                                            381,597
icode WhyInScope                                             19,034
icode WithArity CompiledClauses                               4,865
icode Word64                                                  2,086
icode [()]                                                      933
icode [(Literal,CompiledClauses)]                             2,929
icode [(ModuleName,Scope)]                                      454
icode [(ModuleName,Section)]                                    227
icode [(ModuleName,Word64)]                                     227
icode [(Name,LocalVar)]                                         227
icode [(Name,[AbstractModule])]                               3,580
icode [(Name,[AbstractName])]                                 3,580
icode [(NameSpaceId,NameSpace)]                                 895
icode [(QName,(WithArity CompiledClauses))]                   2,929
icode [(QName,([Arg Expr Name],(Pattern' Expr)))]               227
icode [(QName,Definition)]                                      227
icode [(QName,ModuleName)]                                      895
icode [(Range,MetaInfo)]                                        227
icode [(TermHead,Clause)]                                       478
icode [([Char],(Builtin ([Char],QName)))]                       227
icode [AbstractModule]                                          441
icode [AbstractName]                                          6,482
icode [Arg Expr (Named (Ranged [Char]) (Pattern' Expr))]          4
icode [Arg Expr Name]                                             2
icode [Arg Term (Named (Ranged [Char]) Pattern)]             24,598
icode [Arg Term DisplayTerm]                                    807
icode [Arg Term QName]                                          121
icode [Arg Term Term]                                        85,838
icode [Arg Term [Char]]                                      16,285
icode [Char]                                             11,775,892
icode [Clause]                                               14,682
icode [CtxId]                                                 5,630
icode [DisplayTerm]                                             359
icode [Elim' Term]                                        2,113,904
icode [Expr]                                                      9
icode [GenPart]                                           3,397,352
icode [Int]                                                  18,064
icode [Interval' (Maybe AbsolutePath)]                   10,322,264
icode [ModuleName]                                              895
icode [NamePart]                                          3,283,510
icode [Name]                                                855,382
icode [Occurrence]                                           15,783
icode [Open DisplayForm]                                     15,783
icode [OtherAspect]                                         210,240
icode [PlusLevel]                                           533,482
icode [Polarity]                                             15,783
icode [QName]                                               109,108
icode [RewriteRule]                                          15,783
icode [Term]                                              2,132,739
icode [[Char]]                                            3,241,623
icode [[[Char]]]                                                227
max-open-constraints                                            806
max-open-metas                                                3,189
metas                                                       105,898
pointers  (fresh)                                                 0
pointers (reused)                                                 0
unequal terms                                               152,929

 210,959,534,512 bytes allocated in the heap
  15,619,327,216 bytes copied during GC
     626,502,040 bytes maximum residency (33 sample(s))
       7,020,960 bytes maximum slop
            1308 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     11630 colls,     0 par   58.04s   58.38s     0.0050s    0.4102s
  Gen  1        33 colls,     0 par   33.53s   33.74s     1.0223s    4.4044s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  307.68s  (309.94s elapsed)
  GC      time   91.57s  ( 92.12s elapsed)
  EXIT    time    0.38s  (  0.38s elapsed)
  Total   time  399.64s  (402.45s elapsed)

  %GC     time      22.9%  (22.9% elapsed)

  Alloc rate    685,638,701 bytes per MUT second

  Productivity  77.1% of total user, 76.5% of total elapsed


real	6m42.581s
user	6m39.645s
sys	0m2.112s


Without iInsideScope and statistics:
------------------------------------------------------------------------

 Finished Everything.
Finished README.
Total time                 190,035ms
Parsing                      1,252ms
Parsing.Operators           11,200ms
Import                       2,804ms
Deserialization                  4ms
Scoping                      9,832ms
Typing                      51,915ms
Termination                  1,792ms
Termination.Graph              236ms
Termination.RecCheck           564ms
Termination.Compare            228ms
Positivity                   8,520ms
Injectivity                    832ms
ProjectionLikeness             164ms
Coverage                     2,036ms
Highlighting                 6,840ms
Serialization               81,013ms
Serialization.Sort             412ms
Serialization.BinaryEncode   8,024ms
Serialization.Compress       1,576ms
ModuleName                      24ms

 126,348,361,928 bytes allocated in the heap
  13,047,982,960 bytes copied during GC
     657,615,728 bytes maximum residency (31 sample(s))
       7,384,192 bytes maximum slop
            1312 MB total memory in use (16 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      6495 colls,     0 par   37.36s   37.70s     0.0058s    0.4181s
  Gen  1        31 colls,     0 par   21.67s   21.80s     0.7034s    4.1436s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  129.57s  (134.19s elapsed)
  GC      time   59.03s  ( 59.51s elapsed)
  EXIT    time    0.53s  (  0.53s elapsed)
  Total   time  189.14s  (194.24s elapsed)

  %GC     time      31.2%  (30.6% elapsed)

  Alloc rate    975,120,061 bytes per MUT second

  Productivity  68.8% of total user, 67.0% of total elapsed


real	3m14.364s
user	3m9.136s
sys	0m1.560s

saves 27 seconds!


Using IntMap in Highlighting.Generate
------------------------------------------------------------------------

Finished README.
Total time                 188,195ms
Parsing                      1,284ms
Parsing.Operators           10,836ms
Import                       2,684ms
Deserialization                 52ms
Scoping                      9,276ms
Typing                      51,855ms
Termination                  1,832ms
Termination.Graph              284ms
Termination.RecCheck           492ms
Termination.Compare            236ms
Positivity                   4,224ms
Injectivity                    760ms
ProjectionLikeness             156ms
Coverage                     2,096ms
Highlighting                 6,776ms
Serialization               80,377ms
Serialization.Sort             376ms
Serialization.BinaryEncode  11,316ms
Serialization.Compress       1,656ms
ModuleName                      20ms

 125,739,897,680 bytes allocated in the heap
  12,720,528,000 bytes copied during GC
     593,079,696 bytes maximum residency (29 sample(s))
       6,475,968 bytes maximum slop
            1306 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      4883 colls,     0 par   36.93s   37.27s     0.0076s    0.3663s
  Gen  1        29 colls,     0 par   20.95s   21.08s     0.7271s    3.7767s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  128.84s  (132.03s elapsed)
  GC      time   57.88s  ( 58.35s elapsed)
  EXIT    time    0.45s  (  0.45s elapsed)
  Total   time  187.18s  (190.84s elapsed)

  %GC     time      30.9%  (30.6% elapsed)

  Alloc rate    975,968,155 bytes per MUT second

  Productivity  69.1% of total user, 67.7% of total elapsed


real	3m10.966s
user	3m7.176s
sys	0m1.592s




Store no highlighting information in the state (so serialize none)
------------------------------------------------------------------------

  Finished Everything.
Finished README.
Total time                 160,870ms
Parsing                      1,296ms
Parsing.Operators           10,852ms
Import                       2,400ms
Deserialization                 24ms
Scoping                      9,040ms
Typing                      54,207ms
Termination                  1,724ms
Termination.Graph              224ms
Termination.RecCheck           500ms
Termination.Compare            232ms
Positivity                   7,764ms
Injectivity                    764ms
ProjectionLikeness             180ms
Coverage                     2,176ms
Highlighting                 6,552ms
Serialization               51,647ms
Serialization.Sort             296ms
Serialization.BinaryEncode   7,136ms
Serialization.Compress       2,496ms
ModuleName                      24ms

 119,598,861,496 bytes allocated in the heap
   9,196,836,160 bytes copied during GC
     567,800,168 bytes maximum residency (25 sample(s))
       4,268,824 bytes maximum slop
            1276 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1295 colls,     0 par   29.12s   29.34s     0.0227s    0.3632s
  Gen  1        25 colls,     0 par   14.37s   14.50s     0.5800s    3.6106s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  116.00s  (117.35s elapsed)
  GC      time   43.49s  ( 43.84s elapsed)
  EXIT    time    0.33s  (  0.33s elapsed)
  Total   time  159.83s  (161.53s elapsed)

  %GC     time      27.2%  (27.1% elapsed)

  Alloc rate    1,030,995,746 bytes per MUT second

  Productivity  72.8% of total user, 72.0% of total elapsed


real	2m41.657s
user	2m39.826s
sys	0m1.496s


Statistics with iHighlighting
------------------------------------------------------------------------

 Finished Everything.
Finished README.
Total time                 394,140ms
Parsing                      1,288ms
Parsing.Operators           11,268ms
Import                       4,624ms
Deserialization                 28ms
Scoping                      9,328ms
Typing                      57,123ms
Termination                  2,200ms
Termination.Graph              228ms
Termination.RecCheck           504ms
Termination.Compare            612ms
Positivity                   6,064ms
Injectivity                    956ms
ProjectionLikeness             160ms
Coverage                     2,256ms
Highlighting                 8,344ms
Serialization              268,836ms
Serialization.Sort             612ms
Serialization.BinaryEncode   8,916ms
Serialization.Compress       1,640ms
ModuleName                      24ms

Accumlated statistics
Double  (fresh)                                                   0
Double (reused)                                                   0
Integer  (fresh)                                             31,635
Integer (reused)                                         10,868,668
Node  (fresh)                                             2,077,839
Node (reused)                                            86,047,829
String  (fresh)                                              28,124
String (reused)                                          11,747,768
attempted-constraints                                        24,401
equal terms                                                 147,261
icode ()                                                     27,984
icode (Bool,(Arg Term (Type' Term)))                          1,064
icode (Int,Int)                                                  41
icode (ModuleName,Scope)                                        895
icode (ModuleName,Section)                                    1,946
icode (ModuleName,Word64)                                     1,859
icode (Name,[AbstractModule])                                   441
icode (Name,[AbstractName])                                   6,482
icode (NameSpaceId,NameSpace)                                 3,580
icode (QName,(WithArity CompiledClauses))                     4,865
icode (QName,([Arg Expr Name],(Pattern' Expr)))                   2
icode (QName,Definition)                                     15,783
icode (Range,Aspects)                                       210,240
icode (TermHead,Clause)                                         808
icode (TopLevelModuleName,Int)                              111,583
icode ([Arg Expr Name],(Pattern' Expr))                           2
icode ([Char],(Builtin ([Char],QName)))                         103
icode ([Char],QName)                                             18
icode Abs (ClauseBodyF Term)                                 80,068
icode Abs (Tele (Dom Term (Type' Term)))                     85,967
icode Abs (Type' Term)                                      130,560
icode Abs Term                                               48,051
icode AbsolutePath                                        3,129,812
icode AbstractModule                                            441
icode AbstractName                                            6,597
icode AmbiguousQName                                              4
icode Arg () (Named (Ranged [Char]) Int)                        933
icode Arg Expr (Named (Ranged [Char]) (Pattern' Expr))            6
icode Arg Expr Name                                               3
icode Arg Term (Named (Ranged [Char]) Pattern)               88,057
icode Arg Term (Type' Term)                                  18,606
icode Arg Term DisplayTerm                                    3,196
icode Arg Term QName                                            376
icode Arg Term Term                                       1,661,660
icode Arg Term [Char]                                        72,270
icode ArgInfo ()                                                933
icode ArgInfo Expr                                                9
icode ArgInfo Term                                        2,127,109
icode Aspect                                                210,240
icode Aspects                                               210,240
icode Bool                                                  176,612
icode Builtin ([Char],QName)                                    103
icode Case CompiledClauses                                    2,929
icode Char                                                       36
icode Clause                                                 17,542
icode ClauseBodyF Term                                       97,610
icode CompiledClauses                                        19,614
icode CompiledRepresentation                                 15,783
icode CompressedFile                                            227
icode ConHead                                                93,797
icode CtxId                                                  20,362
icode Definition                                             15,783
icode Defn                                                   15,783
icode Delayed                                                14,664
icode DisplayForm                                             5,630
icode DisplayTerm                                             9,737
icode Dom Term (Type' Term)                                 216,527
icode Drop Permutation                                          261
icode Elim' Term                                          1,670,134
icode Fixity                                              3,397,352
icode Fixity'                                             3,397,352
icode FunctionInverse' Clause                                14,664
icode GenPart                                                 1,843
icode HashMap QName Definition                                  227
icode HaskellRepresentation                                      36
icode Hiding                                              2,128,051
icode Induction                                             106,376
icode Int                                                 2,208,518
icode Int32                                               9,409,391
icode Integer                                            10,900,303
icode Interface                                                 227
icode Interval' (Maybe AbsolutePath)                      1,564,906
icode IsAbstract                                             15,757
icode KindOfName                                              6,597
icode Level                                                 533,482
icode LevelAtom                                             411,010
icode Literal                                                 9,549
icode Map Literal CompiledClauses                             2,929
icode Map ModuleName Scope                                      454
icode Map ModuleName Section                                    227
icode Map Name [AbstractModule]                               3,580
icode Map Name [AbstractName]                                 3,580
icode Map QName (WithArity CompiledClauses)                   2,929
icode Map QName ([Arg Expr Name],(Pattern' Expr))               227
icode Map QName ModuleName                                      895
icode Map TermHead Clause                                       478
icode Map [Char] (Builtin ([Char],QName))                       227
icode Maybe (Arg Term (Type' Term))                          17,542
icode Maybe (Bool,(Arg Term (Type' Term)))                    7,056
icode Maybe (Int,Int)                                        14,664
icode Maybe (Ranged [Char])                                  88,996
icode Maybe (TopLevelModuleName,Int)                        210,240
icode Maybe AbsolutePath                                  3,129,812
icode Maybe Aspect                                          210,240
icode Maybe Bool                                             14,664
icode Maybe Clause                                              382
icode Maybe CompiledClauses                                  17,611
icode Maybe Exp                                              15,783
icode Maybe HaskellExport                                    15,783
icode Maybe HaskellRepresentation                            15,783
icode Maybe Induction                                           121
icode Maybe NameKind                                        115,634
icode Maybe Projection                                       14,664
icode Maybe QName                                            33,030
icode Maybe [Char]                                          226,023
icode ModuleName                                            855,382
icode MutualId                                               15,783
icode Name                                                6,814,256
icode NameId                                              3,530,746
icode NameKind                                              115,634
icode NamePart                                            3,718,531
icode NameSpace                                               3,580
icode NameSpaceId                                             3,580
icode Named (Ranged [Char]) (Pattern' Expr)                       6
icode Named (Ranged [Char]) Int                                 933
icode Named (Ranged [Char]) Pattern                          88,057
icode Occurrence                                             63,382
icode Open DisplayForm                                        5,630
icode OtherAspect                                               720
icode Pattern                                                88,057
icode Pattern' Expr                                               8
icode Permutation                                            18,064
icode PlusLevel                                             432,162
icode Polarity                                               63,379
icode Position' (Maybe AbsolutePath)                      3,129,812
icode Precedence                                                227
icode Projection                                              2,583
icode QName                                                 860,271
icode Range                                                 210,240
icode Range' (Maybe AbsolutePath)                        10,322,264
icode Ranged [Char]                                          83,565
icode Relevance                                           2,128,051
icode Scope                                                     895
icode ScopeInfo                                                 227
icode Section                                                 1,946
icode Set [Char]                                                227
icode Signature                                                 227
icode Sort                                                  419,697
icode Tele (Dom Term (Type' Term))                          105,576
icode Term                                                2,567,151
icode TermHead                                                  808
icode TopLevelModuleName                                  3,241,395
icode Type' Term                                            381,597
icode WhyInScope                                             19,034
icode WithArity CompiledClauses                               4,865
icode Word64                                                  2,086
icode [()]                                                      933
icode [(Literal,CompiledClauses)]                             2,929
icode [(ModuleName,Scope)]                                      454
icode [(ModuleName,Section)]                                    227
icode [(ModuleName,Word64)]                                     227
icode [(Name,LocalVar)]                                         227
icode [(Name,[AbstractModule])]                               3,580
icode [(Name,[AbstractName])]                                 3,580
icode [(NameSpaceId,NameSpace)]                                 895
icode [(QName,(WithArity CompiledClauses))]                   2,929
icode [(QName,([Arg Expr Name],(Pattern' Expr)))]               227
icode [(QName,Definition)]                                      227
icode [(QName,ModuleName)]                                      895
icode [(Range,Aspects)]                                         227
icode [(TermHead,Clause)]                                       478
icode [([Char],(Builtin ([Char],QName)))]                       227
icode [AbstractModule]                                          441
icode [AbstractName]                                          6,482
icode [Arg Expr (Named (Ranged [Char]) (Pattern' Expr))]          4
icode [Arg Expr Name]                                             2
icode [Arg Term (Named (Ranged [Char]) Pattern)]             24,598
icode [Arg Term DisplayTerm]                                    807
icode [Arg Term QName]                                          121
icode [Arg Term Term]                                        85,838
icode [Arg Term [Char]]                                      16,285
icode [Char]                                             11,775,892
icode [Clause]                                               14,682
icode [CtxId]                                                 5,630
icode [DisplayTerm]                                             359
icode [Elim' Term]                                        2,113,904
icode [Expr]                                                      9
icode [GenPart]                                           3,397,352
icode [Int]                                                  18,064
icode [Interval' (Maybe AbsolutePath)]                   10,322,264
icode [ModuleName]                                              895
icode [NamePart]                                          3,283,510
icode [Name]                                                855,382
icode [Occurrence]                                           15,783
icode [Open DisplayForm]                                     15,783
icode [OtherAspect]                                         210,240
icode [PlusLevel]                                           533,482
icode [Polarity]                                             15,783
icode [QName]                                               109,108
icode [RewriteRule]                                          15,783
icode [Term]                                              2,132,739
icode [[Char]]                                            3,241,623
icode [[[Char]]]                                                227
max-open-constraints                                            806
max-open-metas                                                3,189
metas                                                       105,898
pointers  (fresh)                                                 0
pointers (reused)                                                 0
unequal terms                                               152,929

 210,285,326,632 bytes allocated in the heap
  15,139,962,656 bytes copied during GC
     611,198,088 bytes maximum residency (35 sample(s))
       6,807,784 bytes maximum slop
            1323 MB total memory in use (17 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      6198 colls,     0 par   56.84s   57.25s     0.0092s    0.4291s
  Gen  1        35 colls,     0 par   28.59s   28.79s     0.8226s    4.2355s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  306.94s  (312.96s elapsed)
  GC      time   85.43s  ( 86.04s elapsed)
  EXIT    time    0.58s  (  0.57s elapsed)
  Total   time  392.96s  (399.58s elapsed)

  %GC     time      21.7%  (21.5% elapsed)

  Alloc rate    685,095,231 bytes per MUT second

  Productivity  78.3% of total user, 77.0% of total elapsed


real	6m39.728s
user	6m32.957s
sys	0m1.920s
abel@agda:~/agda$


Statistics without iHighlighting
------------------------------------------------------------------------

 Finished Everything.
Finished README.
Total time                 358,934ms
Parsing                      1,408ms
Parsing.Operators           11,376ms
Import                       4,860ms
Deserialization                  4ms
Scoping                      9,452ms
Typing                      59,287ms
Termination                  2,284ms
Termination.Graph              252ms
Termination.RecCheck           572ms
Termination.Compare            336ms
Positivity                   5,800ms
Injectivity                    780ms
ProjectionLikeness             164ms
Coverage                     2,152ms
Highlighting                 6,812ms
Serialization              234,378ms
Serialization.Sort             372ms
Serialization.BinaryEncode   7,588ms
Serialization.Compress       1,764ms
ModuleName                      24ms

Accumlated statistics
Double  (fresh)                                                   0
Double (reused)                                                   0
Integer  (fresh)                                             31,635
Integer (reused)                                         10,868,668
Node  (fresh)                                             1,738,969
Node (reused)                                            84,765,001
String  (fresh)                                              28,115
String (reused)                                          11,449,684
attempted-constraints                                        24,401
equal terms                                                 147,261
icode ()                                                     27,984
icode (Bool,(Arg Term (Type' Term)))                          1,064
icode (Int,Int)                                                  41
icode (ModuleName,Scope)                                        895
icode (ModuleName,Section)                                    1,946
icode (ModuleName,Word64)                                     1,859
icode (Name,[AbstractModule])                                   441
icode (Name,[AbstractName])                                   6,482
icode (NameSpaceId,NameSpace)                                 3,580
icode (QName,(WithArity CompiledClauses))                     4,865
icode (QName,([Arg Expr Name],(Pattern' Expr)))                   2
icode (QName,Definition)                                     15,783
icode (Range,Aspects)                                        94,277
icode (TermHead,Clause)                                         808
icode ([Arg Expr Name],(Pattern' Expr))                           2
icode ([Char],(Builtin ([Char],QName)))                         103
icode ([Char],QName)                                             18
icode Abs (ClauseBodyF Term)                                 80,068
icode Abs (Tele (Dom Term (Type' Term)))                     85,967
icode Abs (Type' Term)                                      130,560
icode Abs Term                                               48,051
icode AbsolutePath                                        3,129,812
icode AbstractModule                                            441
icode AbstractName                                            6,597
icode AmbiguousQName                                              4
icode Arg () (Named (Ranged [Char]) Int)                        933
icode Arg Expr (Named (Ranged [Char]) (Pattern' Expr))            6
icode Arg Expr Name                                               3
icode Arg Term (Named (Ranged [Char]) Pattern)               88,057
icode Arg Term (Type' Term)                                  18,606
icode Arg Term DisplayTerm                                    3,196
icode Arg Term QName                                            376
icode Arg Term Term                                       1,661,660
icode Arg Term [Char]                                        72,270
icode ArgInfo ()                                                933
icode ArgInfo Expr                                                9
icode ArgInfo Term                                        2,127,109
icode Aspect                                                 94,277
icode Aspects                                                94,277
icode Bool                                                   60,978
icode Builtin ([Char],QName)                                    103
icode Case CompiledClauses                                    2,929
icode Char                                                       36
icode Clause                                                 17,542
icode ClauseBodyF Term                                       97,610
icode CompiledClauses                                        19,614
icode CompiledRepresentation                                 15,783
icode CompressedFile                                            227
icode ConHead                                                93,797
icode CtxId                                                  20,362
icode Definition                                             15,783
icode Defn                                                   15,783
icode Delayed                                                14,664
icode DisplayForm                                             5,630
icode DisplayTerm                                             9,737
icode Dom Term (Type' Term)                                 216,527
icode Drop Permutation                                          261
icode Elim' Term                                          1,670,134
icode Fixity                                              3,397,352
icode Fixity'                                             3,397,352
icode FunctionInverse' Clause                                14,664
icode GenPart                                                 1,843
icode HashMap QName Definition                                  227
icode HaskellRepresentation                                      36
icode Hiding                                              2,128,051
icode Induction                                              94,753
icode Int                                                 1,865,009
icode Int32                                               9,409,391
icode Integer                                            10,900,303
icode Interface                                                 227
icode Interval' (Maybe AbsolutePath)                      1,564,906
icode IsAbstract                                             15,757
icode KindOfName                                              6,597
icode Level                                                 533,482
icode LevelAtom                                             411,010
icode Literal                                                 9,549
icode Map Literal CompiledClauses                             2,929
icode Map ModuleName Scope                                      454
icode Map ModuleName Section                                    227
icode Map Name [AbstractModule]                               3,580
icode Map Name [AbstractName]                                 3,580
icode Map QName (WithArity CompiledClauses)                   2,929
icode Map QName ([Arg Expr Name],(Pattern' Expr))               227
icode Map QName ModuleName                                      895
icode Map TermHead Clause                                       478
icode Map [Char] (Builtin ([Char],QName))                       227
icode Maybe (Arg Term (Type' Term))                          17,542
icode Maybe (Bool,(Arg Term (Type' Term)))                    7,056
icode Maybe (Int,Int)                                        14,664
icode Maybe (Ranged [Char])                                  88,996
icode Maybe (TopLevelModuleName,Int)                         94,277
icode Maybe AbsolutePath                                  3,129,812
icode Maybe Aspect                                           94,277
icode Maybe Bool                                             14,664
icode Maybe Clause                                              382
icode Maybe CompiledClauses                                  17,611
icode Maybe Exp                                              15,783
icode Maybe HaskellExport                                    15,783
icode Maybe HaskellRepresentation                            15,783
icode Maybe Induction                                           121
icode Maybe Projection                                       14,664
icode Maybe QName                                            33,030
icode Maybe [Char]                                          110,060
icode ModuleName                                            855,382
icode MutualId                                               15,783
icode Name                                                6,814,256
icode NameId                                              3,530,746
icode NamePart                                            3,718,531
icode NameSpace                                               3,580
icode NameSpaceId                                             3,580
icode Named (Ranged [Char]) (Pattern' Expr)                       6
icode Named (Ranged [Char]) Int                                 933
icode Named (Ranged [Char]) Pattern                          88,057
icode Occurrence                                             63,382
icode Open DisplayForm                                        5,630
icode Pattern                                                88,057
icode Pattern' Expr                                               8
icode Permutation                                            18,064
icode PlusLevel                                             432,162
icode Polarity                                               63,379
icode Position' (Maybe AbsolutePath)                      3,129,812
icode Precedence                                                227
icode Projection                                              2,583
icode QName                                                 860,271
icode Range                                                  94,277
icode Range' (Maybe AbsolutePath)                        10,322,264
icode Ranged [Char]                                          83,565
icode Relevance                                           2,128,051
icode Scope                                                     895
icode ScopeInfo                                                 227
icode Section                                                 1,946
icode Set [Char]                                                227
icode Signature                                                 227
icode Sort                                                  419,697
icode Tele (Dom Term (Type' Term))                          105,576
icode Term                                                2,567,151
icode TermHead                                                  808
icode TopLevelModuleName                                  3,129,812
icode Type' Term                                            381,597
icode WhyInScope                                             19,034
icode WithArity CompiledClauses                               4,865
icode Word64                                                  2,086
icode [()]                                                      933
icode [(Literal,CompiledClauses)]                             2,929
icode [(ModuleName,Scope)]                                      454
icode [(ModuleName,Section)]                                    227
icode [(ModuleName,Word64)]                                     227
icode [(Name,LocalVar)]                                         227
icode [(Name,[AbstractModule])]                               3,580
icode [(Name,[AbstractName])]                                 3,580
icode [(NameSpaceId,NameSpace)]                                 895
icode [(QName,(WithArity CompiledClauses))]                   2,929
icode [(QName,([Arg Expr Name],(Pattern' Expr)))]               227
icode [(QName,Definition)]                                      227
icode [(QName,ModuleName)]                                      895
icode [(Range,Aspects)]                                         227
icode [(TermHead,Clause)]                                       478
icode [([Char],(Builtin ([Char],QName)))]                       227
icode [AbstractModule]                                          441
icode [AbstractName]                                          6,482
icode [Arg Expr (Named (Ranged [Char]) (Pattern' Expr))]          4
icode [Arg Expr Name]                                             2
icode [Arg Term (Named (Ranged [Char]) Pattern)]             24,598
icode [Arg Term DisplayTerm]                                    807
icode [Arg Term QName]                                          121
icode [Arg Term Term]                                        85,838
icode [Arg Term [Char]]                                      16,285
icode [Char]                                             11,477,799
icode [Clause]                                               14,682
icode [CtxId]                                                 5,630
icode [DisplayTerm]                                             359
icode [Elim' Term]                                        2,113,904
icode [Expr]                                                      9
icode [GenPart]                                           3,397,352
icode [Int]                                                  18,064
icode [Interval' (Maybe AbsolutePath)]                   10,322,264
icode [ModuleName]                                              895
icode [NamePart]                                          3,283,510
icode [Name]                                                855,382
icode [Occurrence]                                           15,783
icode [Open DisplayForm]                                     15,783
icode [OtherAspect]                                          94,277
icode [PlusLevel]                                           533,482
icode [Polarity]                                             15,783
icode [QName]                                               109,108
icode [RewriteRule]                                          15,783
icode [Term]                                              2,132,739
icode [[Char]]                                            3,130,040
icode [[[Char]]]                                                227
max-open-constraints                                            806
max-open-metas                                                3,189
metas                                                       105,898
pointers  (fresh)                                                 0
pointers (reused)                                                 0
unequal terms                                               152,929

 202,532,440,400 bytes allocated in the heap
  11,529,793,296 bytes copied during GC
     563,215,312 bytes maximum residency (26 sample(s))
       5,623,232 bytes maximum slop
            1297 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      2193 colls,     0 par   49.63s   49.89s     0.0228s    0.4222s
  Gen  1        26 colls,     0 par   17.24s   17.45s     0.6711s    4.0100s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  290.41s  (292.19s elapsed)
  GC      time   66.87s  ( 67.34s elapsed)
  EXIT    time    0.71s  (  0.71s elapsed)
  Total   time  357.99s  (360.25s elapsed)

  %GC     time      18.7%  (18.7% elapsed)

  Alloc rate    697,411,037 bytes per MUT second

  Productivity  81.3% of total user, 80.8% of total elapsed


real	6m0.388s
user	5m57.994s
sys	0m1.796s



2014-10-20  On master: without iInsideScope but with iHighlighting
------------------------------------------------------------------------

 Finished Everything.
Finished README.
Total time                 398,476ms
Parsing                      1,396ms
Parsing.Operators           11,200ms
Import                       4,996ms
Deserialization                 24ms
Scoping                      9,456ms
Typing                      54,883ms
Termination                  2,020ms
Termination.Graph              292ms
Termination.RecCheck           532ms
Termination.Compare            228ms
Positivity                   5,508ms
Injectivity                    812ms
ProjectionLikeness             140ms
Coverage                     2,656ms
Highlighting                10,772ms
Serialization              260,852ms
Serialization.Sort             576ms
Serialization.BinaryEncode  22,185ms
Serialization.Compress       2,032ms
ModuleName                      24ms

Accumlated statistics
Double  (fresh)                                                   0
Double (reused)                                                   0
Integer  (fresh)                                             31,686
Integer (reused)                                         10,877,950
Node  (fresh)                                             2,081,245
Node (reused)                                            86,112,880
String  (fresh)                                              28,183
String (reused)                                          11,756,366
attempted-constraints                                        24,420
equal terms                                                 147,392
icode ()                                                     27,986
icode (Bool,(Arg Term (Type' Term)))                          1,065
icode (Int,Int)                                                  41
icode (ModuleName,Scope)                                        900
icode (ModuleName,Section)                                    1,949
icode (ModuleName,Word64)                                     1,869
icode (Name,[AbstractModule])                                   442
icode (Name,[AbstractName])                                   6,505
icode (NameSpaceId,NameSpace)                                 3,600
icode (QName,(WithArity CompiledClauses))                     4,877
icode (QName,([Arg Expr Name],(Pattern' Expr)))                   2
icode (QName,Definition)                                     15,801
icode (Range,Aspects)                                       210,745
icode (TermHead,Clause)                                         811
icode (TopLevelModuleName,Int)                              111,831
icode ([Arg Expr Name],(Pattern' Expr))                           2
icode ([Char],(Builtin ([Char],QName)))                         109
icode ([Char],QName)                                             22
icode Abs (ClauseBodyF Term)                                 80,134
icode Abs (Tele (Dom Term (Type' Term)))                     86,023
icode Abs (Type' Term)                                      130,617
icode Abs Term                                               48,063
icode AbsolutePath                                        3,131,386
icode AbstractModule                                            442
icode AbstractName                                            6,620
icode AmbiguousQName                                              4
icode Arg () (Named (Ranged [Char]) Int)                        933
icode Arg Expr (Named (Ranged [Char]) (Pattern' Expr))            6
icode Arg Expr Name                                               3
icode Arg Term (Named (Ranged [Char]) Pattern)               88,139
icode Arg Term (Type' Term)                                  18,626
icode Arg Term DisplayTerm                                    3,196
icode Arg Term QName                                            376
icode Arg Term Term                                       1,662,357
icode Arg Term [Char]                                        72,313
icode ArgInfo ()                                                933
icode ArgInfo Expr                                                9
icode ArgInfo Term                                        2,128,094
icode Aspect                                                210,745
icode Aspects                                               210,745
icode Bool                                                  176,915
icode Builtin ([Char],QName)                                    109
icode Case CompiledClauses                                    2,937
icode Char                                                       36
icode Clause                                                 17,561
icode ClauseBodyF Term                                       97,695
icode CompiledClauses                                        19,638
icode CompiledRepresentation                                 15,801
icode CompressedFile                                            229
icode ConHead                                                93,856
icode CtxId                                                  20,362
icode Definition                                             15,801
icode Defn                                                   15,801
icode Delayed                                                14,676
icode DisplayForm                                             5,630
icode DisplayTerm                                             9,737
icode Dom Term (Type' Term)                                 216,640
icode Drop Permutation                                          262
icode Elim' Term                                          1,670,759
icode Fixity                                              3,400,446
icode Fixity'                                             3,400,446
icode FunctionInverse' Clause                                14,676
icode GenPart                                                 1,843
icode HashMap QName Definition                                  229
icode HaskellRepresentation                                      36
icode Hiding                                              2,129,036
icode Induction                                             106,462
icode Int                                                 2,210,220
icode Int32                                               9,414,155
icode Integer                                            10,909,636
icode Interface                                                 229
icode Interval' (Maybe AbsolutePath)                      1,565,693
icode IsAbstract                                             15,775
icode KindOfName                                              6,620
icode Level                                                 533,792
icode LevelAtom                                             411,046
icode Literal                                                 9,549
icode Map Literal CompiledClauses                             2,937
icode Map ModuleName Scope                                      458
icode Map ModuleName Section                                    229
icode Map Name [AbstractModule]                               3,600
icode Map Name [AbstractName]                                 3,600
icode Map QName (WithArity CompiledClauses)                   2,937
icode Map QName ([Arg Expr Name],(Pattern' Expr))               229
icode Map QName ModuleName                                      900
icode Map TermHead Clause                                       481
icode Map [Char] (Builtin ([Char],QName))                       229
icode Maybe (Arg Term (Type' Term))                          17,561
icode Maybe (Bool,(Arg Term (Type' Term)))                    7,072
icode Maybe (Int,Int)                                        14,676
icode Maybe (Ranged [Char])                                  89,078
icode Maybe (TopLevelModuleName,Int)                        210,745
icode Maybe AbsolutePath                                  3,131,386
icode Maybe Aspect                                          210,745
icode Maybe Bool                                             14,676
icode Maybe Clause                                              383
icode Maybe CompiledClauses                                  17,635
icode Maybe Exp                                              15,801
icode Maybe HaskellExport                                    15,801
icode Maybe HaskellRepresentation                            15,801
icode Maybe Induction                                           121
icode Maybe NameKind                                        115,883
icode Maybe Projection                                       14,676
icode Maybe QName                                            33,060
icode Maybe [Char]                                          226,546
icode ModuleName                                            856,038
icode MutualId                                               15,801
icode Name                                                6,820,470
icode NameId                                              3,533,840
icode NameKind                                              115,883
icode NamePart                                            3,721,931
icode NameSpace                                               3,600
icode NameSpaceId                                             3,600
icode Named (Ranged [Char]) (Pattern' Expr)                       6
icode Named (Ranged [Char]) Int                                 933
icode Named (Ranged [Char]) Pattern                          88,139
icode Occurrence                                             63,423
icode Open DisplayForm                                        5,630
icode OtherAspect                                               720
icode Pattern                                                88,139
icode Pattern' Expr                                               8
icode Permutation                                            18,085
icode PlusLevel                                             432,213
icode Polarity                                               63,420
icode Position' (Maybe AbsolutePath)                      3,131,386
icode Precedence                                                229
icode Projection                                              2,583
icode QName                                                 860,897
icode Range                                                 210,745
icode Range' (Maybe AbsolutePath)                        10,331,737
icode Ranged [Char]                                          83,711
icode Relevance                                           2,129,036
icode Scope                                                     900
icode ScopeInfo                                                 229
icode Section                                                 1,949
icode Set [Char]                                                229
icode Signature                                                 229
icode Sort                                                  419,921
icode Tele (Dom Term (Type' Term))                          105,654
icode Term                                                2,568,151
icode TermHead                                                  811
icode TopLevelModuleName                                  3,243,217
icode Type' Term                                            381,805
icode WhyInScope                                             19,060
icode WithArity CompiledClauses                               4,877
icode Word64                                                  2,098
icode [()]                                                      933
icode [(Literal,CompiledClauses)]                             2,937
icode [(ModuleName,Scope)]                                      458
icode [(ModuleName,Section)]                                    229
icode [(ModuleName,Word64)]                                     229
icode [(Name,LocalVar)]                                         229
icode [(Name,[AbstractModule])]                               3,600
icode [(Name,[AbstractName])]                                 3,600
icode [(NameSpaceId,NameSpace)]                                 900
icode [(QName,(WithArity CompiledClauses))]                   2,937
icode [(QName,([Arg Expr Name],(Pattern' Expr)))]               229
icode [(QName,Definition)]                                      229
icode [(QName,ModuleName)]                                      900
icode [(Range,Aspects)]                                         229
icode [(TermHead,Clause)]                                       481
icode [([Char],(Builtin ([Char],QName)))]                       229
icode [AbstractModule]                                          442
icode [AbstractName]                                          6,505
icode [Arg Expr (Named (Ranged [Char]) (Pattern' Expr))]          4
icode [Arg Expr Name]                                             2
icode [Arg Term (Named (Ranged [Char]) Pattern)]             24,633
icode [Arg Term DisplayTerm]                                    807
icode [Arg Term QName]                                          121
icode [Arg Term Term]                                        85,880
icode [Arg Term [Char]]                                      16,301
icode [Char]                                             11,784,549
icode [Clause]                                               14,698
icode [CtxId]                                                 5,630
icode [DisplayTerm]                                             359
icode [Elim' Term]                                        2,114,690
icode [Expr]                                                      9
icode [GenPart]                                           3,400,446
icode [Int]                                                  18,085
icode [Interval' (Maybe AbsolutePath)]                   10,331,737
icode [ModuleName]                                              900
icode [NamePart]                                          3,286,630
icode [Name]                                                856,038
icode [Occurrence]                                           15,801
icode [Open DisplayForm]                                     15,801
icode [OtherAspect]                                         210,745
icode [PlusLevel]                                           533,792
icode [Polarity]                                             15,801
icode [QName]                                               109,181
icode [RewriteRule]                                          15,801
icode [Term]                                              2,133,724
icode [[Char]]                                            3,243,446
icode [[[Char]]]                                                229
max-open-constraints                                            806
max-open-metas                                                3,192
metas                                                       106,069
pointers  (fresh)                                                 0
pointers (reused)                                                 0
unequal terms                                               153,084

 210,558,703,632 bytes allocated in the heap
  15,072,887,360 bytes copied during GC
     612,880,832 bytes maximum residency (34 sample(s))
       7,340,400 bytes maximum slop
            1337 MB total memory in use (16 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      4858 colls,     0 par   55.53s   56.01s     0.0115s    0.4145s
  Gen  1        34 colls,     0 par   31.69s   31.91s     0.9387s    4.1898s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  309.20s  (311.50s elapsed)
  GC      time   87.22s  ( 87.93s elapsed)
  EXIT    time    0.57s  (  0.57s elapsed)
  Total   time  397.00s  (400.01s elapsed)

  %GC     time      22.0%  (22.0% elapsed)

  Alloc rate    680,980,511 bytes per MUT second

  Productivity  78.0% of total user, 77.4% of total elapsed

396.99user 2.20system 6:40.14elapsed 99%CPU (0avgtext+0avgdata 5542640maxresident)k
24inputs+27752outputs (0major+354131minor)pagefaults 0swaps


2014-11-04  Deactivated constructor disambiguation for highlighting
-------------------------------------------------------------------

Finished README.
Total time                 195,012ms
Parsing                      1,408ms
Parsing.Operators           14,216ms
Import                       3,036ms
Deserialization                 20ms
Scoping                     10,824ms
Typing                      61,303ms
Termination                  2,840ms
Termination.Graph              268ms
Termination.RecCheck         1,304ms
Termination.Compare            460ms
Positivity                   4,048ms
Injectivity                    948ms
ProjectionLikeness             252ms
Coverage                     2,252ms
Highlighting                 1,020ms
Serialization               76,144ms
Serialization.Sort             376ms
Serialization.BinaryEncode  11,928ms
Serialization.Compress       1,768ms
ModuleName                      28ms

 122,046,609,728 bytes allocated in the heap
  11,866,444,856 bytes copied during GC
     638,121,896 bytes maximum residency (30 sample(s))
       7,214,280 bytes maximum slop
            1286 MB total memory in use (15 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      4493 colls,     0 par   36.75s   36.90s     0.0082s    0.4175s
  Gen  1        30 colls,     0 par   27.11s   27.26s     0.9086s    4.4603s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  130.01s  (131.21s elapsed)
  GC      time   63.86s  ( 64.16s elapsed)
  EXIT    time    0.58s  (  0.58s elapsed)
  Total   time  194.45s  (195.96s elapsed)

  %GC     time      32.8%  (32.7% elapsed)

  Alloc rate    938,732,397 bytes per MUT second

  Productivity  67.2% of total user, 66.6% of total elapsed


real	3m16.133s
user	3m14.452s
sys	0m1.304s


2014-11-04  Do constructor disambiguation during type checking
--------------------------------------------------------------

 Finished Everything.
Finished README.
Total time                 194,856ms
Parsing                      1,376ms
Parsing.Operators           13,664ms
Import                       3,068ms
Deserialization                 24ms
Scoping                     11,068ms
Typing                      57,659ms
Termination                  2,556ms
Termination.Graph              224ms
Termination.RecCheck         1,104ms
Termination.Compare            328ms
Positivity                   8,072ms
Injectivity                    932ms
ProjectionLikeness             168ms
Coverage                     2,300ms
Highlighting                   988ms
Serialization               80,113ms
Serialization.Sort             412ms
Serialization.BinaryEncode   8,120ms
Serialization.Compress       1,808ms
ModuleName                      28ms

 122,078,411,856 bytes allocated in the heap
  11,990,849,520 bytes copied during GC
     638,488,592 bytes maximum residency (30 sample(s))
       7,516,072 bytes maximum slop
            1282 MB total memory in use (15 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      4973 colls,     0 par   36.93s   37.24s     0.0075s    0.4159s
  Gen  1        30 colls,     0 par   26.54s   26.75s     0.8917s    4.3250s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  129.86s  (131.45s elapsed)
  GC      time   63.47s  ( 63.99s elapsed)
  EXIT    time    0.60s  (  0.60s elapsed)
  Total   time  193.94s  (196.05s elapsed)

  %GC     time      32.7%  (32.6% elapsed)

  Alloc rate    940,076,286 bytes per MUT second

  Productivity  67.3% of total user, 66.5% of total elapsed


real	3m16.196s
user	3m13.936s
sys	0m1.664s


Without   t <- instantiateFull t  in TypeChecking.Rules.Def
------------------------------------------------------------------------

Finished README.
Total time                 195,536ms
Parsing                      1,404ms
Parsing.Operators           14,024ms
Import                       3,092ms
Deserialization                 24ms
Scoping                     10,480ms
Typing                      53,051ms
Termination                  2,776ms
Termination.Graph              368ms
Termination.RecCheck         1,312ms
Termination.Compare            268ms
Positivity                   8,212ms
Injectivity                    904ms
ProjectionLikeness             208ms
Coverage                     2,148ms
Highlighting                 1,024ms
Serialization               81,289ms
Serialization.Sort             376ms
Serialization.BinaryEncode  11,764ms
Serialization.Compress       1,820ms
ModuleName                      28ms

 122,090,910,456 bytes allocated in the heap
  11,908,810,632 bytes copied during GC
     640,081,224 bytes maximum residency (30 sample(s))
       7,314,104 bytes maximum slop
            1279 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      4642 colls,     0 par   36.86s   37.24s     0.0080s    0.4179s
  Gen  1        30 colls,     0 par   27.10s   27.29s     0.9097s    4.4415s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  130.08s  (132.19s elapsed)
  GC      time   63.96s  ( 64.53s elapsed)
  EXIT    time    0.59s  (  0.59s elapsed)
  Total   time  194.63s  (197.32s elapsed)

  %GC     time      32.9%  (32.7% elapsed)

  Alloc rate    938,611,040 bytes per MUT second

  Productivity  67.1% of total user, 66.2% of total elapsed


real	3m17.461s
user	3m14.632s
sys	0m1.632s


2014-11-10 master, with ghc-7.6
------------------------------------------------------------------------

Finished README.
Total time                 283,057ms
Parsing                      1,488ms
Parsing.Operators           13,904ms
Import                       2,772ms
Deserialization                 40ms
Scoping                     11,112ms
Typing                     130,844ms
Termination                  2,236ms
Termination.Graph              256ms
Termination.RecCheck           524ms
Termination.Compare            396ms
Positivity                   7,008ms
Injectivity                  4,760ms
ProjectionLikeness             600ms
Coverage                     5,464ms
Highlighting                 1,048ms
Serialization               89,657ms
Serialization.Sort             384ms
Serialization.BinaryEncode   6,868ms
Serialization.Compress       1,356ms
ModuleName                      28ms

 125,708,437,080 bytes allocated in the heap
  12,879,084,368 bytes copied during GC
     568,489,336 bytes maximum residency (32 sample(s))
       5,913,480 bytes maximum slop
            1261 MB total memory in use (15 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1131 colls,     0 par   36.69s   36.90s     0.0326s    0.3218s
  Gen  1        32 colls,     0 par   20.29s   20.43s     0.6386s    3.9345s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  224.53s  (231.58s elapsed)
  GC      time   56.98s  ( 57.33s elapsed)
  EXIT    time    0.50s  (  0.50s elapsed)
  Total   time  282.02s  (289.42s elapsed)

  %GC     time      20.2%  (19.8% elapsed)

  Alloc rate    559,883,593 bytes per MUT second

  Productivity  79.8% of total user, 77.8% of total elapsed


No problem with master on ghc-7.8!
------------------------------------------------------------------------

Finished README.
Total time                 183,075ms
Parsing                      1,336ms
Parsing.Operators           10,696ms
Import                       3,280ms
Deserialization                 12ms
Scoping                      9,312ms
Typing                      64,964ms
Termination                  2,116ms
Termination.Graph              264ms
Termination.RecCheck           492ms
Termination.Compare            320ms
Positivity                   7,120ms
Injectivity                    992ms
ProjectionLikeness             304ms
Coverage                     2,384ms
Highlighting                   836ms
Serialization               66,792ms
Serialization.Sort             400ms
Serialization.BinaryEncode   7,536ms
Serialization.Compress       1,800ms
ModuleName                      20ms

 122,286,747,520 bytes allocated in the heap
  14,580,664,344 bytes copied during GC
     559,218,144 bytes maximum residency (34 sample(s))
       4,922,168 bytes maximum slop
            1328 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1331 colls,     0 par   37.19s   37.57s     0.0282s    0.3455s
  Gen  1        34 colls,     0 par   15.93s   16.12s     0.4741s    3.4936s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  128.35s  (132.49s elapsed)
  GC      time   53.12s  ( 53.69s elapsed)
  EXIT    time    0.48s  (  0.48s elapsed)
  Total   time  181.96s  (186.68s elapsed)

  %GC     time      29.2%  (28.8% elapsed)

  Alloc rate    952,744,950 bytes per MUT second

  Productivity  70.8% of total user, 69.0% of total elapsed

181.96user 1.73system 3:06.81elapsed 98%CPU (0avgtext+0avgdata 5504912maxresident)k
22240inputs+28280outputs (0major+351768minor)pagefaults 0swaps

maint with ghc-7.8
------------------------------------------------------------------------

Finished README.
Total time                 189,179ms
Parsing                      1,328ms
Parsing.Operators           11,624ms
Import                       2,468ms
Deserialization                 16ms
Scoping                     12,280ms
Typing                      51,831ms
Termination                  2,812ms
Termination.Graph              216ms
Termination.RecCheck         1,440ms
Termination.Compare            292ms
Positivity                   4,628ms
Injectivity                    776ms
ProjectionLikeness             172ms
Coverage                     2,068ms
Highlighting                   836ms
Serialization               82,417ms
Serialization.Sort             424ms
Serialization.BinaryEncode  11,492ms
Serialization.Compress       1,748ms
ModuleName                      20ms

 118,079,069,576 bytes allocated in the heap
  12,125,797,416 bytes copied during GC
     643,116,728 bytes maximum residency (31 sample(s))
       5,074,584 bytes maximum slop
            1296 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      3187 colls,     0 par   36.81s   37.17s     0.0117s    0.4279s
  Gen  1        31 colls,     0 par   25.43s   25.58s     0.8250s    4.1056s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  125.66s  (126.77s elapsed)
  GC      time   62.24s  ( 62.74s elapsed)
  EXIT    time    0.40s  (  0.40s elapsed)
  Total   time  188.31s  (189.92s elapsed)

  %GC     time      33.1%  (33.0% elapsed)

  Alloc rate    939,642,132 bytes per MUT second

  Productivity  66.9% of total user, 66.4% of total elapsed


real	3m10.064s
user	3m8.308s
sys	0m1.412s





2016-06-26 agda-master 2.6.0 ghc-7.8.4
========================================================================

Finished README.
Total                        94,221ms
Miscellaneous                 4,902ms
Parsing                         624ms
Parsing.Operators             7,515ms
Import                        1,955ms
Deserialization                  20ms
Scoping                       3,016ms
Scoping.InverseScopeLookup      576ms
Typing                        9,029ms
Typing.OccursCheck            2,875ms
Typing.CheckLHS              21,046ms
Typing.CheckLHS.UnifyIndices    920ms
Termination                     533ms
Termination.Graph               341ms
Termination.RecCheck            231ms
Termination.Compare             161ms
Positivity                    2,073ms
Injectivity                     465ms
ProjectionLikeness               93ms
Coverage                        448ms
Highlighting                    635ms
Serialization                26,229ms
Serialization.BuildInterface  1,517ms
Serialization.Sort              296ms
Serialization.BinaryEncode    5,972ms
Serialization.Compress          973ms
DeadCode                      1,760ms
ModuleName                        3ms

 117,456,330,328 bytes allocated in the heap
  15,633,531,704 bytes copied during GC
     439,263,904 bytes maximum residency (41 sample(s))
       3,020,488 bytes maximum slop
            1129 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1625 colls,     0 par   20.81s   20.92s     0.0129s    0.1599s
  Gen  1        41 colls,     0 par    7.16s    7.18s     0.1751s    0.4843s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time   65.61s  ( 66.40s elapsed)
  GC      time   27.98s  ( 28.10s elapsed)
  EXIT    time    0.01s  (  0.02s elapsed)
  Total   time   93.61s  ( 94.53s elapsed)

  %GC     time      29.9%  (29.7% elapsed)

  Alloc rate    1,790,178,276 bytes per MUT second

  Productivity  70.1% of total user, 69.4% of total elapsed


real	1m34.579s
user	1m33.614s
sys	0m0.700s