[Agda] profiling

[mechvel at scico.botik.ru]

On 2021-02-04 00:06, Ulf Norell wrote:
> 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.


So, first to apply
     > agda -c $agdaLibOpt KTest.agda

Then go to MAlonzo/Code/...<where MM.hs resides that has suspected 
calls>,
and set cost centers to  MM.hs.
Then  `agda -c'  should not be applied because it would overwrite MM.hs.
Instead I probably need to run

   > cd  <where KTest.hs resides>                          (?)
   > ghc --make KTest  <profilig options>
                       <ghc options used by Agda after applying `agda 
-c'>
Right?
And what are        <ghc options used by Agda after applying `agda -c'>
?
where to see them?

Thanks,

--
СМ



> 
> 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