[Agda] Haskell cost centers?

[Aaron Stump]

Thanks for the fast reply, Wolfram.

On 04/15/2016 04:22 PM, Wolfram Kahl wrote:
> On Fri, Apr 15, 2016 at 04:11:29PM -0500, Aaron Stump wrote:
>> I am trying to profile some Agda code (which I am having Agda compile to
>> Haskell) using Haskell's profiling mechanisms, and I am wondering if
>> there is a way to indicate Haskell cost centers in Agda source code.  I
>> can ask Agda to pass Haskell the flags -p and -fprof-auto, which is
>> great, but the code I am trying to profile includes some parts that are
>> getting rather blown up by the Agda-to-Haskell compilation, and so the
>> profiling execution time is very slow and profiling output is very hard
>> to read.  I believe this is because too many cost centers are getting
>> created by Haskell's -fprof-auto (but I am hardly an expert on that).
>> If I could assign my own cost centers, I am hoping that would help make
>> it easier to sort through all the information to see what is going on.
> Are you using agda-ghc-names (mentioned in the ChangeLog / Release notes)
> to back-translate your .prof files?
I did not know about that.  I fear it may not help too much in this 
case, because the main problem is that Agda is compiling a 687-line 
.agda file to a 17190-line .hs file, generating a lot of intermediate 
expressions.  This is leading to a large .prof file (19111 lines), that 
would be hard to comprehend even if the identifiers were mapped back to 
Agda identifiers.
>
> Some of what I find going on is that there is insufficient inlining
> and sharing.
>
> Some time ago I filed Issue 1895
>
>    https://github.com/agda/agda/issues/1895
>
> , and yesterday, Ulf wrote:
>
>   | This might make a nice code sprint for next week.
>
> So let's hope somebody finds this an attractive target!
I would certainly appreciate it, and for people who are trying to use 
Agda for writing executable programs, this will improve the tooling and 
the integration with Haskell significantly.

Cheers,
Aaron
>
>
> Wolfram
>