[Agda] syntax highlighting in darcs agda-mode

[Nils Anders Danielsson]

On 2009-12-11 12:03, Andrea Vezzosi wrote:
> Though it seems that C-c C-l typechecks the current file again even if
> it didn't change since the .agdai was produced

No (unless some imported module has changed). It can take some time to
load all the imported modules, though. Check the output in the *ghci*
buffer to see what happens.

> It felt considerably worse with Agda-2.2.5 to me, so i tested both
> against version 0.2 of the standard library, using agda-executable.
>
> Agda-2.2.4 completed the typechecking of Everything from scratch
> requiring less than 700MB of memory, while Agda-2.2.5 coudln't finish
> in under 2GB (a large part seems to be used by lists).

Version 0.2 of the library does not type check with Agda 2.2.5. What
exactly did you test?

Quite a few changes have gone into the next version of Agda (see the
release notes), and I don't know what has caused this increase in memory
use. Ulf, do your benchmarks provide any relevant information?

By the way, does the performance of Agda improve if you restrict the
maximum heap size using, say, +RTS -M1.5G?

> In either case i'd like to help, could you give me some directions on
> what to look at in the code or documentation?

I'd start by profiling the code.

--
/NAD