[Agda] profiling

[guillaume allais]

Hi Sergei,

If you look at the `agda -c` trace, you'll notice the call to ghc after the
"Compiling XXX.YYY" lines and before the "[n of NNN]" ones.

This is what I got by running a dummy compilation job:

Calling: ghc -O -Werror -i[DIRECTORY] [DIRECTORY/MAlonzo/Code/FILE.hs] 
--make -fwarn-incomplete-patterns -fno-warn-overlapping-patterns

Best,


On 03/02/2021 21:41, mechvel at scico.botik.ru wrote:
> CAUTION: This email originated outside the University. Check before 
> clicking links or attachments.
>
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7Cb3e109804248493ac54c08d8c88c8575%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637479853152179960%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=w10lYKcYPHKDOxv%2FTnP4UM3GIVMQOtm8vrJeXw6%2FgoQ%3D&reserved=0 
>