Agda profiling

[scott-fleischman]

Sergei posted on the Agda mailing list some comments on profiling. It might be worthwhile to play around with it to see where Agda is spending its time in our code.

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
-----------------------------

[scott-fleischman]

Now that the instance arguments were removed and it type checks in Agda 2.4.2.3, here is the profile for Romans.

Finished Text.Greek.SBLGNT.Rom.
Total                      148,212ms
Miscellaneous                   60ms
Parsing                        479ms
Parsing.Operators            7,835ms
Import                          22ms
Deserialization              2,423ms
Scoping                     50,466ms
Typing                      73,764ms
Termination                      6ms
Termination.RecCheck           228ms
Positivity                     187ms
Injectivity                      0ms
ProjectionLikeness               0ms
Coverage                         0ms
Highlighting                   233ms
Serialization               10,328ms
Serialization.Sort             102ms
Serialization.BinaryEncode   1,575ms
Serialization.Compress          62ms
ModuleName                     436ms

[scott-fleischman]

All of SBLGNT:

Finished Text.Greek.SBLGNT.
Total                      4,722,508ms
Miscellaneous                    110ms
Parsing                        8,514ms
Parsing.Operators            206,023ms
Import                           106ms
Deserialization                2,576ms
Scoping                    1,840,119ms
Typing                     2,398,107ms
Termination                      147ms
Termination.RecCheck           4,660ms
Positivity                     3,623ms
Injectivity                        4ms
ProjectionLikeness                 2ms
Coverage                          19ms
Highlighting                   7,299ms
Serialization                221,431ms
Serialization.Sort             2,025ms
Serialization.BinaryEncode    26,749ms
Serialization.Compress           980ms
ModuleName                         7ms

[scott-fleischman]

4,722,508 ms / (1000 ms / s) / (60 s / min) / (60 min / hour) => 1.3118 hour

[scott-fleischman]

This thread indicates that splitting the Agda code into smaller pieces helps improve type checking time.