[Agda] Performance improvements (Agda devel)

[Wolfram Kahl]

On Sat, Jun 22, 2013 at 08:27:20PM +0200, Andreas Abel wrote:
> if you have some large terms in you developments and have not pulled 
> Agda recently, it might be worth trying.  I have implemented some 
> performance improvements that are probably noticeable if you use records 
> a lot.  The relevant patches concern "issue 854".
> 
> James reported a reduction of memory consumption from 12GB to 3GB for 
> one of his developments.
> 
> In case you see similar improvements, please reply to this message.

Wonderful!

On three test runs for which I have recent data
(the second is a suffix of the first):

             BEFORE:    Agda-2.3.3.2 (2013-03-24)
        Alloc       MaxRes(Samples)    Total  
2,172,067,616,184  5,815,796,880(48)  3549.76s
  362,024,671,040  5,401,771,680(21)   754.85s
7,516,986,546,168  8,428,119,312(54)  8761.11s


              AFTER:   Agda-2.3.3.5 (2013-06-22)
      Alloc              MaxRes(Samples)  Total
1,754,047,703,504  5,423,841,888(47)  2998.62s
  250,513,599,816  4,839,014,776(21)   594.95s
3,220,489,812,720  5,697,783,096(31)  3550.02s

All of these are run with:
  time agda +RTS -S -K256M -H11G -M11G -RTS ...

The comparison is not absolutely precise
since the new version had more work to do on the first run,
and the current state of the third run was actually
already pushing the limits of what works in 11G,
so the comparison above lets the old version look a bit better
than it is...


Thank you very much!


Wolfram