[Agda] Severe performance regression on master

Andreas Abel abela at chalmers.se
Mon Nov 10 23:46:03 CET 2014


Thanks for the hint!

As it turned out, the performance regression does not happen on ghc-7.8, 
only on ghc-7.6.

Reported "Total time" of std-lib test

              maint     master
ghc-7.6.3    195s      283s
ghc-7.8.3    189s      183s

Agda-master on ghc-7.6 is (in this case) >50% slower than the ghc-7.8 
compiled version.

I tried to find an explanation, in the ghc-7.8.1 release notes, but got 
nothing conclusive.

Cheers,
Andreas

On 05.11.2014 19:20, Joachim Breitner wrote:
> Hi,
>
> Am Mittwoch, den 05.11.2014, 18:28 +0100 schrieb Andreas Abel:
>> [Concerns Agda developers only:]
>>
>> Type-checking the standard library with master since recently takes
>> twice as long than on maint, according to the benchmark.
>>
>> master:
>> ...
>> Typing                     130,272ms
>> ...
>>
>> maint:
>> ...
>> Typing                      61,291ms
>> ...
>>
>> If you pushed modifications to the type checker onto master recently,
>> please benchmark Agda before and after your patch.
>>
>> Cheers,
>> Andreas
>>
>> P.S.:  As a general guideline, when you run the testsuite before your
>> push, also check for performance regressions!
>
> for GHC, we recently started to set up a performance measurement tool:
> http://ghcspeed-nomeata.rhcloud.com/
>
> It’s not perfect, but it is off-the-shelve software at least, so if you
> have a volunteer that knows a bit of python and django, and a quiet
> machine, you can set this up as well.
>
> Greetings,
> Joachim
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/


More information about the Agda mailing list