Termination checker to blame for bad performance [Re: [Agda] long type checking times in the development version]

[Andreas Abel]

Currently the termination checker is very inefficient, so you can work 
around this with --no-termination-check.

Having a couple mutually recursive functions with 10 arguments each 
(hidden ones count) already blasts the termination checker.

It has been on my todo list for a couple of weeks to fix this, but I do 
not get to it...

Cheers,
Andreas

On 13.03.2014 01:14, Martin Escardo wrote:
> I was getting ok resource consumption by the development version of
> Agda, such as 3sec in a project, with 1GB more than enough, in a core i5
> machine.
>
> However, my student Chuangjie Xu, in the same project, with a core i7
> machine with more memory than my machine (and I with another core i5
> machine), was getting an infinitely long time, with an unresponsive
> machine after a couple of seconds.
>
> We were both working under ubuntu.
>
> I (saved the old version and) reinstalled the development version from
> scratch, and my 3sec time moved to a couple of minutes (but managed to
> complete) in the core i5 machine with 4GB of ram.
>
> Then I copied an old darc version of the development version I had in
> one computer (seems to be of 27 Dec 2013) to all of our slow Agda
> machines, and did "make install" (preceded by clean-up suitable steps).
> This gave fast (=few seconds) times with low memory consumption in all
> machines.
>
> I can provide sample Agda files if needed. But, before that (1) has the
> development version since 27 Dec had any radical change that could cause
> that, (2) could the installation environment possibly have a radical
> impact on efficiency?
>
> Thanks,
> Martin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


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

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

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