[Agda-dev] Performance problem due to module aliases

[Nicolas Pouillard]

I have been bitten by this before. I had a 20 line module in crypto-agda eating all memory.

I'm glad to see such a test case. I'm looking forward for this issue to be resolved.

On 09/13/2015 01:01 PM, Andreas Abel wrote:
> Module aliases
>
>    module M = N args
>
> can be surprisingly costly.  Here is a 50 line program that takes more
> than 5 minutes to pass Agda, producing a 26M interface file.  It
> consists of 10 module declarations and 27 module aliases.  Nothing
> fancy, really.
>
>    https://github.com/agda/agda/issues/1646
>

-- 
Best regards,
-- NP