[Agda] Haskell cost centers?

Wolfram Kahl kahl at cas.mcmaster.ca
Fri Apr 15 23:22:10 CEST 2016


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?

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!


Wolfram



More information about the Agda mailing list