[Agda] profiling

[Sergei Meshveliani]

People,

In the Bug tracker #1533 I see the call

   agda -i. -i <certain directory>  -v prifile:7 Main.agda

I guess that 
1) this is for profiling of something related to  Main.agda  
   (provided in my report Agda source),
2) `prifile' is a typo for `profile'.

I have the following questions.

Where `profile' is documented? 
I do not see it in  agda --help,  nor in the on-line manual.

What does it mean `:7' ?

I command  
  > agda $agdaLibOpt -v profile:7 Main.agda

, and indeed it prints a certain statistic. 
It produces Main.agdai, but not the executable Main, and all the
rest .agdai files were ready before.
So I think that this is a certain profiling for the type-check of
Main.agda.
Right?

The statistic (on my machine) is
------------------------------
Finished Main.
Total                      50,843ms
Miscellaneous                 232ms
Parsing                         4ms
Parsing.Operators               0ms
Import                         44ms
Deserialization            12,572ms
Scoping                       188ms
Typing                      1,024ms
Termination                     0ms
Termination.RecCheck            0ms
Positivity                      0ms
Injectivity                     0ms
ProjectionLikeness              0ms
Coverage                        0ms
Highlighting                    0ms
Serialization              35,570ms
Serialization.Sort             72ms
Serialization.BinaryEncode  1,040ms
Serialization.Compress         92ms
ModuleName                      4ms
-----------------------------

What does it mean Serialization ?

The process takes in reality about  51 sec., which I think, corresponds
to the line
            Total  50,843ms.

About 1/10 of all the time it was printing the messages of the kind 

    Skipping  <a module which .agdai is ready before> 

The last such was 
 Skipping AssociatedClasses
(/home/mechvel/doconA/0.04/reports/may31-2015/AssociatedClasses.agdai).

Then, after 40 seconds, it appears

  Finished Main.

So, first 10 seconds it has spent to considering imports among the
ready .agdai  modulles (?).
But this is not written in the statistic (?).

The comment #12 on the issue 1533 is 

  Optimizing the serialization of A.QName, I now get:
  []
  Total     27,164ms
  []

(instead of 69,829).

Does this mean that the current  _development version_  is more than
2.5 times faster on type-checking Main.agda than  Agda 2.4.2.3 
?


If I delete all the  .agdai  files and apply 

     > agda $agdaLibOpt -v profile:7 Main.agda

,  Agda 2.4.2.3 prints the statistic of
----------------------------------------
Finished Main.
Total                      185,931ms
Miscellaneous                  280ms
Parsing                        384ms
Parsing.Operators            7,424ms
Import                          32ms
Deserialization              2,900ms
Scoping                      5,496ms
Typing                      17,617ms
Termination                  1,236ms
Termination.Graph              432ms
Termination.RecCheck           508ms
Termination.Compare            492ms
Positivity                   8,976ms
Injectivity                    104ms
ProjectionLikeness              48ms
Coverage                       444ms
Highlighting                   236ms
Serialization              128,876ms
Serialization.Sort             688ms
Serialization.BinaryEncode   9,092ms
Serialization.Compress         652ms
ModuleName                      12ms
--------------------------------------------

What particular features the code of the 1533 report has that causes a
great type-check expense?

It has many complex records, with a high nesting level, sometimes with a
considerable code beyond the `field' part.
1) I do not see how to avoid deep record nesting.
2) I can move a non-field code to separate modules, but doubt that this
   could help essentially.
3) If type check is 2-3 times speed up (probably, the space for type
check also becomes 2-3 times smaller), then this is a big deal, it will
be easier to debug an application.

In my real application, some modules take more than 30 minutes to
type-check.

Thank you in advance for explanation,

------
Sergei