<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Mar 29, 2017 at 9:54 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br>
1.<br>
I use the option -v profile:7<br>
<br>Where the profiling option is referenced?<br></blockquote><div><br></div><div>They're not, as far as I know. You can give -v profile.modules:10</div><div>or -v profile.definitions:10 to get a breakdown of the type checking</div><div>time per module or definition.</div><div><br></div><div>There's also -v profile.interactive:10 which will time Emacs mode commands</div><div>like C-c C-n.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">2.<br>
The --help list shows the options with-K, without-K.<br>
Which one is the default?<br></blockquote><div><br></div><div>--with-K</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">I have read certain explanation about the K axiom. It says that K means<br>
uniqueness of any identity proof.<br>
Suppose that one programs<br>
<br>
f : (x y : Carrier) → x ≈ y → Carrier<br>
<br>
for any Setoid. Does with-K option mean that the type checker<br>
presumes that it holds the property<br>
<br>
(x y : Carrier) → x ≈ y → x ≡ y<br>
?<br></blockquote><div><br></div><div>No. Very much simplified, --without-K means you cannot pattern match</div><div>a proof of x ≡ x against refl.</div><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">3.<br>
I am trying to profile type checking on my application program.<br>
Agda type-checks many modules before coming to Foo.agda.<br>
And Foo.agda has nothing besides importing modules and opening a<br>
certain parametric module with giving it a parameter instance.<br>
<br>
First all modules before Foo.agda are type-checked.<br>
Then I command<br>
<br>
> agda $agdaLibOpt -v profile:7 +RTS -K90m -M8G -RTS Foo.agda<br>
<br>
And it reports<br>
<br>
------------------------------<wbr>------------------------------<wbr>------<br>
Loading M1<br>
Loading M2<br>
...<br>
Loading FactorizationRing.FtRing<br>
(/home/mechvel/agda/tosave/<wbr>bugs/tcPerf-mar28-2017/<wbr>FactorizationRing/FtRing.<wbr>agdai).<br>
<br>
Finished Foo.<br>
Total 143,264ms<br>
Miscellaneous 300ms<br>
Serialization 67,128ms (75,508ms)<br>
Serialization.BuildInterface 4,648ms<br>
Serialization.BinaryEncode 3,148ms<br>
Serialization.Sort 332ms<br>
Serialization.Compress 252ms<br>
Deserialization 51,819ms<br>
DeadCode 8,212ms<br>
Typing 7,296ms<br>
Scoping 64ms (84ms)<br>
Scoping.InverseScopeLookup 20ms<br>
Import 44ms<br>
------------------------------<wbr>------------------------------<wbr>-------<br>
<br>
"Loading FactorizationRing.FtRing"<br>
means that this module is only being loaded but not type-checked.<br>
Right?<br></blockquote><div><br></div><div>Yes.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">About Foo.agda, it does not report Loading nor "checking".<br>
And I expect that the time segment between the report of<br>
"Loading FactorizationRing.FtRing" and before appearing of<br>
"Finished Foo" is the time taken by type-checking Foo.agda.<br>
Right?<br></blockquote><div><br></div><div>Right. It does say "Checking Foo" at the top. It loads the other modules</div><div>as it finds the import statements during scope checking, so there</div><div>might be some scope checking time before the last "Loading", but</div><div>no type checking.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">3.1.<br>
The `time' command shows that this process lasts about 144 sec.<br>
<br>
So, I guess that in the line<br>
"Total 143,264ms"<br>
<br>
comma parts thousands, so that this means 143 seconds and 264<br>
milliseconds.<br>
Right?<br></blockquote><div><br></div><div>Yes.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<br>
3.2.<br>
What is Serialization and Deserialization (in short) ?<br>
What does it mean the second number (in parentheses) in the line of<br>
Serialization?<br></blockquote><div><br></div><div>Serialization is the writing of interface files for type checked modules and</div><div>Deserialization is the reading of such interface files (the 'Loading' bit).</div><div>The number in parenthesis is including all subentries</div><div>(Serialization.BuildInterfaces, ...).</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Having the above profiling, how can we derive the time spent to<br>
"Loading" ready modules before starting to type-check Foo.agda ?<br>
(I observe that it is about 50 seconds).<br></blockquote><div><br></div><div>Deserialization 51,819ms<br></div><div><br></div><div>/ Ulf</div></div></div></div>