[Agda] Wish List

Vag Vagoff vag.vagoff at gmail.com
Tue Sep 22 18:05:27 CEST 2009


 
>
>         Compiler or typechecker? There are known performance problems
>         with the typechecker, but I thought the compiler | was
>         reasonably efficient.
>          
>
Difference between times of compiling and typechecking indistinguishable.

In Emacs,
5 seconds if compiling/typechecking one module repeatedly,
9-10 seconds if compiling/typechecking one module after working on 
another module.

In command line,
compilation always takes 5 seconds, typechecking always takes 3 seconds.
But after switching from Thunderbird mail agent, for example, it takes 
11 seconds to compile.
Typecheckin still takes 3 seconds after any switching.

Seems like page cache trashing!



More information about the Agda mailing list