[Agda] Improving reload performance in emacs mode

[Ulf Norell]

On Mon, Nov 24, 2008 at 4:14 PM, Kasper Brink <kjbrink at students.cs.uu.nl>wrote:

> Hi all,
>
> Agda's interactive emacs mode is really nice to work with, but reloading
> the current file (C-c C-x C-l) can be quite slow. On my machine (an old
> laptop), reloading part of a multi-module program that imports several
> standard library modules can take half a minute or more. Profiling the
> standalone typechecker shows that most of the time is spent decoding the
> interface files that are read from disk. This is done by decoding functions
> in module Agda.Typechecking.Serialise; they are apparently carefully
> designed to maximise sharing in the typechecker's internal structures, and
> are probably not easy to speed up.
>
> However, it seems a shame to repeat this work on every reload, even if the
> interfaces haven't changed. I've patched Agda to maintain a cache of
> previously decoded interfaces that is preserved across reloads (details
> below for those interested). This does not do anything for the initial
> loading of a file, but it speeds up subsequent reloads significantly.  The
> implementation can certainly be improved, but the patch does not seem to
> break anything, and hopefully it shows that caching interfaces is a fairly
> easy way to improve the reloading performance. It would be nice if
> something like this could be implemented in the official repository,
> especially for those of us with slow hardware!
>

Excellent work! I will have a look and add the patches to the official
repository sometime during the week. I'm flying to the Agda meeting in Japan
tomorrow so expect it around Thursday-Friday.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081124/afc3daaa/attachment.html