[Agda] profiling

[Ulf Norell]

For cost centers you need to manually edit the generated Haskell code and
recompile it with ghc.
But those two lines should correspond to *functions* not modules, and you
should be able to find
them in the big tree view to see where they are called from. Mapping the
name of a generated
Haskell function to the Agda name can be a bit fiddly, but it is given in
the generated Haskell code.

/ Ulf

On Wed, Feb 3, 2021 at 5:47 PM <mechvel at scico.botik.ru> wrote:

> On 2021-02-03 13:37, Ulf Norell wrote:
> > I suggested installing ieee754 with profiling enabled. I didn't say
> > anything about setting up a
> >  .cabal file for your project (although, that is certainly a thing
> > that one can do).
>
>
> Now, the story is as follows.
>
> I install  Agda-2.6.1.1  (+ MAlonzo, ghc-8.8.3)
> and run
>    > agda -c $agdaLibOpt --ghc-flag=-prof  KTest.agda
>
> It reports
> ...
>   MAlonzo/RTE.hs:9:1: error: ...
>   Perhaps you haven't installed the profiling libraries for
>   package ‘ieee754-0.8.0’?
>
> I run
>    > cabal v1-install ieee754 --enable-library-profiling
>
> It reports "Already installed ... To reinstall use --reinstall ...".
> I run
>    > cabal v1-install ieee754 --enable-library-profiling --reinstall
>                               --force-reinstalls
>
> - because only --reinstall occurs not sufficient to reinstall.
> Then it starts to work!
> It reinstalls Agda (because it depends on ieee754).
> Then
>    > agda -c $agdaLibOpt --ghc-flag=-prof  KTest.agda
>
> also re-compiles the Agda standard library, then  KTest  is made.
> I run
>    > KTest +RTS -p -RTS
>
> This creates KTest.prof.
> There it is said that all the cost is taken by
>    MAlonzo.Code.KTest  <entire-module>
> "
> ...
> CAF MAlonzo.Code.KTest  <entire-module> ... 0  100.0 100.0 100.0 100.0
> ...
> ".
> This gives nothing to me.
> I need to find a responsible function in the Foo library
> (written in Agda) which KTest imports.
>
> Then I add  --ghc-flag=-fprof-auto  to the `agda -c'  command.
>
> Now  KTest.prof  reports of thousands of functions and modules.
> Its two head lines show
>
>    MAlonzo.RTE                MAlonzo/RTE.hs:59:1-13           8.0  0.0
>         MAlonzo/Code/Data/Nat/Properties.hs:(146,1)-(151,39)   6.0 18.2
>
> So that  MAlonzo/RTE.hs          takes  8% of time,
>           Data/Nat/Properties.hs  takes  6% of time,
> and each of the rest takes not more than 6%.
>
> I cannot detect from this what function in Foo is responsible for that
> the "optimized" program in Agda runs 50 times slower than the naive one.
>
> But I recall that for my Haskell programs I used the _cost centers_
> by setting  {-# SCC <name> -#}  to the suspected places in my Haskell
> program, and this was much more helpful than `-auto-all'.
>
> Setting {-# SCC <name> #-} to the .agda file probably will not be
> parsed.
>
> In what way cost centers can be used with Agda?
>
> Thanks,
>
> ------
> Sergei
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210203/fbc4786f/attachment.html>