[Agda] syntax highlighting in darcs agda-mode

[Nils Anders Danielsson]

On 2009-12-03 02:42, Andrea Vezzosi wrote:
> I've switched to the darcs version of agda and i noticed that it
> doesn't produce the .el files with the syntax hilighting anymore, so
> now you've to first load the file to get it.

Yes. The highlighting info is cached in the .agdai files.

> This is not much of a problem for my own sources, but i used to
> navigate the standard library by opening Everything.agda and following
> the module names with M-., now i'd have to load all the standard
> library everytime and that requires more than 1.4GB of memory, at
> which point i decide to kill it and grep.

Loading up README.agda "only" requires 855MiB on my machine (according
to top). I wonder why your configuration requires so much more memory.
Are you running your machine in 64-bit mode?

(I assume that you have already type-checked all the library modules
once before. If not, then the memory consumption may be higher.)

> Is this change in behaviour permanent?

I have no immediate plans to change the behaviour. It would be possible
to load only the highlighting info from the .agdai file, but I would
prefer if the underlying problem was fixed. Anyone is welcome to provide
a patch, though.

> are there plans to reduce the memory use?

There is a long-standing problem with loss of sharing in Agda's
implementation. I suspect that the memory use would be a lot lower if
sharing was preserved by the type checker.

In case anyone is interested I measured the total size of the library's
.agdai files: ∼12MiB. This turns into ∼60MiB after decompression, and a
lot more after it has been converted into internal Agda data structures.

--
/NAD