[Agda] syntax highlighting in darcs agda-mode

[Andrea Vezzosi]

On Thu, Dec 3, 2009 at 3:10 PM, Nils Anders Danielsson
<nad at cs.nott.ac.uk> wrote:
> 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.

Ah, i thought it wasn't cached at all.
Though it seems that C-c C-l typechecks the current file again even if
it didn't change since the .agdai was produced, it'd be nice if it was
smarter about avoiding recomputation.

>> 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?

Yes, i'm in 64-bit mode, i realize that's not really wise considering
GHC's memory model..

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

I thought so but i actually didn't, so i guess my problem is
completing the typechecking first.

>> 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.

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).

I wouldn't expect the additional highlighting information to use so
much more memory to compute or store, so to me it looks like there
might be some new "leak", or maybe just something that makes the loss
of sharing more problematic.

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

Thanks,
  Andrea Vezzosi.

> 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
>
>