[Agda] Redundant imports

[Guillaume Allais]

Hi Martin,

I don't really remember how it works but looking at the code,
there seems to be a warning level for useless imports (the
analysis was extremely slow so it seems I disabled it by
default and that's probably one of the reasons why I did not
try to merge it in Agda stable).

https://github.com/agda/agda/commit/f45e8e0850e8e5d5a42f65c46275beeb112df4d8#diff-71ae678c257eb560c9d6e9fb881133c4R108

I think that if you were to put `{-# OPTIONS -Wuseless-imports #-}`
at the top of your file, it should work.

Hope it helps!

Cheers,
--
gallais

On 25/04/18 10:04, Martin Escardo wrote:
> Thanks. I compiled this branch. But how do I use this feature? I just
> tried to load a module in emacs, with deliberately unneeded imports,
> and nothing is reported. Or do I need to invoke a command for this
> check? M.
>
> On 24/04/18 09:54, nad at cse.gu.se wrote:
>> On 2018-04-23 21:55, Martín Hötzel Escardó wrote:
>>> I have reorganized a large code base by splitting and merging modules,
>>> and moving things from one module to another, and I fear I am left
>>> with very many redundant imports. Is there any way to detect them
>>> automatically?
>>
>> Guillame Allais has been working on something like this on a separate
>> branch:
>>
>>    https://github.com/agda/agda/issues/2503
>>
>


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180425/db974c73/attachment.sig>