[Agda] long type checking times in the development version

Martin Escardo m.escardo at cs.bham.ac.uk
Thu Mar 13 01:14:37 CET 2014


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


More information about the Agda mailing list