[Agda] Agda options

[Sergei Meshveliani]

Dear Agda developers,

I have the following notes and questions about the Agda type checking
options
(for Agda 2.6.0-85c6255).


1. 
I use the option  -v profile:7 

which I copy from certain old letter by Wolfram.
And it reports a profiling (shown below). 

On the other hand, I look at the text produced by the command

       agda --help

, and do not find there any occurrence of the word `profil'.

Where the profiling option is referenced?


2. 
The --help list shows the options  with-K, without-K.
Which one is the default?

I have read certain explanation about the K axiom. It says that K means
uniqueness of any identity proof.
Suppose that one programs

  f : (x y : Carrier) → x ≈ y → Carrier

for any Setoid.  Does  with-K  option mean that the type checker
presumes that it holds the property 

  (x y : Carrier) → x ≈ y → x ≡ y  
?


3. 
I am trying to profile type checking on my application program.
Agda type-checks many modules before coming to  Foo.agda.
And  Foo.agda  has nothing besides importing modules and opening a
certain parametric module with giving it a parameter instance.

First all modules before  Foo.agda  are type-checked.
Then I command 

  > agda $agdaLibOpt -v profile:7 +RTS -K90m -M8G -RTS  Foo.agda

And it reports

------------------------------------------------------------------
Loading M1 
Loading M2 
... 
Loading  FactorizationRing.FtRing
(/home/mechvel/agda/tosave/bugs/tcPerf-mar28-2017/FactorizationRing/FtRing.agdai).

Finished Foo.
Total                        143,264ms           
Miscellaneous                    300ms           
Serialization                 67,128ms (75,508ms)
Serialization.BuildInterface   4,648ms           
Serialization.BinaryEncode     3,148ms           
Serialization.Sort               332ms           
Serialization.Compress           252ms           
Deserialization               51,819ms           
DeadCode                       8,212ms           
Typing                         7,296ms           
Scoping                           64ms     (84ms)
Scoping.InverseScopeLookup        20ms           
Import                            44ms           
-------------------------------------------------------------------

"Loading  FactorizationRing.FtRing" 
means that this module is only being loaded but not type-checked. 
Right?

About  Foo.agda,  it does not report Loading nor "checking".
And I expect that the time segment between the report of  
"Loading  FactorizationRing.FtRing"  and before appearing of 
"Finished Foo"  is the time taken by type-checking  Foo.agda.
Right?

3.1.
The `time' command shows that this process lasts about  144 sec.

So, I guess that in the line 
                        "Total       143,264ms"           

comma parts thousands, so that this means 143 seconds and 264
milliseconds.
Right?

3.2. 
What is Serialization and Deserialization (in short) ?
What does it mean the second number (in parentheses) in the line of
Serialization?

Having the above profiling, how can we derive the time spent to 
"Loading" ready modules before starting to type-check Foo.agda ?
(I observe that it is about 50 seconds).

Thanks,

------
Sergei