<div dir="ltr"><div>For cost centers you need to manually edit the generated Haskell code and recompile it with ghc.</div><div>But those two lines should correspond to *functions* not modules, and you should be able to find</div><div>them in the big tree view to see where they are called from. Mapping the name of a generated</div><div>Haskell function to the Agda name can be a bit fiddly, but it is given in the generated Haskell code.<br></div><br><div>/ Ulf<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Feb 3, 2021 at 5:47 PM <<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 2021-02-03 13:37, Ulf Norell wrote:<br>
> I suggested installing ieee754 with profiling enabled. I didn't say<br>
> anything about setting up a<br>
>  .cabal file for your project (although, that is certainly a thing<br>
> that one can do).<br>
<br>
<br>
Now, the story is as follows.<br>
<br>
I install  Agda-2.6.1.1  (+ MAlonzo, ghc-8.8.3)<br>
and run<br>
   > agda -c $agdaLibOpt --ghc-flag=-prof  KTest.agda<br>
<br>
It reports<br>
...<br>
  MAlonzo/RTE.hs:9:1: error: ...<br>
  Perhaps you haven't installed the profiling libraries for<br>
  package ‘ieee754-0.8.0’?<br>
<br>
I run<br>
   > cabal v1-install ieee754 --enable-library-profiling<br>
<br>
It reports "Already installed ... To reinstall use --reinstall ...".<br>
I run<br>
   > cabal v1-install ieee754 --enable-library-profiling --reinstall<br>
                              --force-reinstalls<br>
<br>
- because only --reinstall occurs not sufficient to reinstall.<br>
Then it starts to work!<br>
It reinstalls Agda (because it depends on ieee754).<br>
Then<br>
   > agda -c $agdaLibOpt --ghc-flag=-prof  KTest.agda<br>
<br>
also re-compiles the Agda standard library, then  KTest  is made.<br>
I run<br>
   > KTest +RTS -p -RTS<br>
<br>
This creates KTest.prof.<br>
There it is said that all the cost is taken by<br>
   MAlonzo.Code.KTest  <entire-module><br>
"<br>
...<br>
CAF MAlonzo.Code.KTest  <entire-module> ... 0  100.0 100.0 100.0 100.0<br>
...<br>
".<br>
This gives nothing to me.<br>
I need to find a responsible function in the Foo library<br>
(written in Agda) which KTest imports.<br>
<br>
Then I add  --ghc-flag=-fprof-auto  to the `agda -c'  command.<br>
<br>
Now  KTest.prof  reports of thousands of functions and modules.<br>
Its two head lines show<br>
<br>
   MAlonzo.RTE                MAlonzo/RTE.hs:59:1-13           8.0  0.0<br>
        MAlonzo/Code/Data/Nat/Properties.hs:(146,1)-(151,39)   6.0 18.2<br>
<br>
So that  MAlonzo/RTE.hs          takes  8% of time,<br>
          Data/Nat/Properties.hs  takes  6% of time,<br>
and each of the rest takes not more than 6%.<br>
<br>
I cannot detect from this what function in Foo is responsible for that<br>
the "optimized" program in Agda runs 50 times slower than the naive one.<br>
<br>
But I recall that for my Haskell programs I used the _cost centers_<br>
by setting  {-# SCC <name> -#}  to the suspected places in my Haskell<br>
program, and this was much more helpful than `-auto-all'.<br>
<br>
Setting {-# SCC <name> #-} to the .agda file probably will not be <br>
parsed.<br>
<br>
In what way cost centers can be used with Agda?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
</blockquote></div>