<div dir="ltr">In the output of -v profile each line represents a disjoint activity. If you sum<div>the numbers in the first column you should end up with the total time spent.</div><div>Some activities a broken down into subactivities (like Typing) in which case</div><div>the total time for all Typing.* activities are shown in parenthesis after the</div><div>Typing entry.</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Apr 18, 2017 at 1:10 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:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Mon, 2017-04-17 at 23:11 +0200, Andreas Abel wrote:<br>
> This says you spent 267 seconds on checking right-hand-sides of<br>
> equations (or type signatures, I suppose).  [I do not remember having<br>
> introduced this benchmark subcategory of Typing.]<br>
<br>
</span>What is the relation between the processes of  Serialization and<br>
Typing.CheckRHS ?<br>
What intersection do they have? Does the former include the latter?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
> On 17.04.2017 22:07, Sergei Meshveliani wrote:<br>
> > Dear Agda developers,<br>
> ><br>
> > I continue investigating the type check cost of various parts in my<br>
> > project.<br>
> > And for certain module  Integer2.agda,  the option  -v profile:7<br>
> > shows something new:<br>
> ><br>
> >     Typing.CheckRHS    267,464ms<br>
> ><br>
> > This occurs the greatest part in Total for this module<br>
> > (while in other considered modules the main part was Serialization and<br>
> > Serialization).<br>
> > Can you, please comment this?<br>
> ><br>
> > Thanks,<br>
> ><br>
> > ------<br>
> > Sergei<br>
> ><br>
> > ______________________________<wbr>_________________<br>
> > Agda mailing list<br>
> > <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> > <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
> ><br>
><br>
><br>
<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>