[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