[Agda] unused values

Sergei Meshveliani mechvel at botik.ru
Thu Sep 17 15:49:46 CEST 2015


Dear Agda developers,

I point to another reason of why  
  reporting of unused values and unused import

will be helpful.

When reducing a large program example for the purpose of debugging,
pieces of the code are being commented out. Each comment-out makes some
values and some import unused. Automating the search of these newly 
unused things will reduce greatly the process of the example reduction.

For example, currently I have a certain code to reduce for a report. 
It needed 6 Gb to type-check. I have spent 8 hours of a stupid work to
reduce this space to 4 Gb, and need to reduce this to  1 Gb.  And I do
not reduce unused values, so far, because it takes an effort to find
them.

Regards,

------
Sergei



More information about the Agda mailing list