[Agda-dev] Performance problem due to module aliases

Andreas Abel abela at chalmers.se
Sun Sep 13 13:01:02 CEST 2015


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

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/


More information about the Agda-dev mailing list