[Agda] profiling

[mechvel at scico.botik.ru]

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