[Agda-dev] One more point for my false-golfing score

[Nils Anders Danielsson]

On 2015-07-01 21:29, Wolfram Kahl wrote:
> I think the question is: Can we remove ``abstract''?
>
> Are there any use cases where it actually still makes a significant difference?
>
> WHen I abandoned ``abstract'', it just gave me gains in type-checking time
> in the order of 1% to 2% on my RATH-Agda code base of the time,
> and I started needing some of the proofs anyways.
> For one to two percent typechecking time, I think it is not worth the extra complexity.

I tried removing abstract from the following development:

   http://www.cse.chalmers.se/~nad/repos/equality/

With abstract in place:

$ time agda -v0 --ignore-interfaces Equivalence.agda +RTS -s
    8,635,704,032 bytes allocated in the heap
    9,337,200,064 bytes copied during GC
      190,867,416 bytes maximum residency (56 sample(s))
        1,626,636 bytes maximum slop
              473 MB total memory in use (0 MB lost due to fragmentation)

                                      Tot time (elapsed)  Avg pause  Max pause
   Gen  0     49379 colls,     0 par   16.276s  16.102s     0.0003s    0.0028s
   Gen  1        56 colls,     0 par   11.340s  11.555s     0.2063s    0.5579s

   INIT    time    0.000s  (  0.000s elapsed)
   MUT     time   25.836s  ( 26.136s elapsed)
   GC      time   27.616s  ( 27.657s elapsed)
   EXIT    time    0.000s  (  0.026s elapsed)
   Total   time   53.456s  ( 53.819s elapsed)

   %GC     time      51.7%  (51.4% elapsed)

   Alloc rate    334,250,814 bytes per MUT second

   Productivity  48.3% of total user, 48.0% of total elapsed


real    0m53.828s
user    0m53.456s
sys     0m0.436s

Without abstract:

$ time agda -v0 --ignore-interfaces Equivalence.agda +RTS -s
agda: out of memory (requested 2097152 bytes)

real    3m51.112s
user    3m49.504s
sys     0m1.876s

-- 
/NAD