[Agda] Severe performance regression on master

[Andreas Abel]

[Concerns Agda developers only:]

Type-checking the standard library with master since recently takes 
twice as long than on maint, according to the benchmark.

master:
...
Typing                     130,272ms
...

maint:
...
Typing                      61,291ms
...

If you pushed modifications to the type checker onto master recently, 
please benchmark Agda before and after your patch.

Cheers,
Andreas

P.S.:  As a general guideline, when you run the testsuite before your 
push, also check for performance regressions!


Full benchmark:

master:

Finished README.
Total time                 274,253ms
Parsing                      1,456ms
Parsing.Operators           13,780ms
Import                       2,804ms
Deserialization                 28ms
Scoping                     11,004ms
Typing                     130,272ms
Termination                  2,396ms
Termination.Graph              284ms
Termination.RecCheck           580ms
Termination.Compare            348ms
Positivity                   6,768ms
Injectivity                  4,680ms
ProjectionLikeness             640ms
Coverage                     5,208ms
Highlighting                 1,004ms
Serialization               81,169ms
Serialization.Sort             380ms
Serialization.BinaryEncode   7,832ms
Serialization.Compress       1,420ms
ModuleName                      28ms

  125,261,417,400 bytes allocated in the heap
   14,379,446,184 bytes copied during GC
      557,075,392 bytes maximum residency (33 sample(s))
        5,177,328 bytes maximum slop
             1324 MB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max 
pause
   Gen  0      1338 colls,     0 par   36.32s   36.64s     0.0274s 
0.3105s
   Gen  1        33 colls,     0 par   16.16s   16.39s     0.4966s 
3.8368s

   INIT    time    0.00s  (  0.00s elapsed)
   MUT     time  220.37s  (224.57s elapsed)
   GC      time   52.48s  ( 53.03s elapsed)
   EXIT    time    0.51s  (  0.51s elapsed)
   Total   time  273.37s  (278.11s elapsed)

   %GC     time      19.2%  (19.1% elapsed)

   Alloc rate    568,404,331 bytes per MUT second

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


maint:

Finished README.
Total time                 195,328ms
Parsing                      1,380ms
Parsing.Operators           13,212ms
Import                       3,112ms
Deserialization                 32ms
Scoping                     11,404ms
Typing                      61,291ms
Termination                  2,616ms
Termination.Graph              232ms
Termination.RecCheck         1,184ms
Termination.Compare            384ms
Positivity                   4,516ms
Injectivity                    972ms
ProjectionLikeness             152ms
Coverage                     2,368ms
Highlighting                   980ms
Serialization               80,393ms
Serialization.Sort             396ms
Serialization.BinaryEncode   8,124ms
Serialization.Compress       1,864ms
ModuleName                      28ms

  122,071,178,752 bytes allocated in the heap
   11,989,478,520 bytes copied during GC
      638,489,040 bytes maximum residency (30 sample(s))
        7,504,976 bytes maximum slop
             1282 MB total memory in use (15 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max 
pause
   Gen  0      4976 colls,     0 par   37.22s   37.51s     0.0075s 
0.4176s
   Gen  1        30 colls,     0 par   26.55s   26.74s     0.8913s 
4.3293s

   INIT    time    0.00s  (  0.00s elapsed)
   MUT     time  130.12s  (131.46s elapsed)
   GC      time   63.77s  ( 64.25s elapsed)
   EXIT    time    0.60s  (  0.60s elapsed)
   Total   time  194.50s  (196.32s elapsed)

   %GC     time      32.8%  (32.7% elapsed)

   Alloc rate    938,113,371 bytes per MUT second

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



-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/