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

[Andrea Vezzosi]

Do you still have the version without abstract? I'd like to try with
my lazy-unfolding patch

On Tue, Aug 18, 2015 at 4:36 PM, Nils Anders Danielsson <nad at cse.gu.se> wrote:
> 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
>
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev