[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