[Agda] Redundant imports

[Guillaume Allais]

I think you have to either use `--warning` or `-W` but `--W` won't work.

On 25/04/18 13:53, Martin Escardo wrote:
>
>
> On 25/04/18 12:40, guillaume.allais at ens-lyon.org wrote:
>> 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.
>
> Ah, thanks. The problem is that I have 70 files, and I don't want to
> add this non-standard option in all of them. I tried "agda --W
> useless-imports everything.lagda" but this is not recognized from the
> command line.
>
> (I am trying to clean a number of files that I am going to use for
> teaching in May, and one nice thing to do would be to get rid of the
> useless imports.)
>
> Martin
>
>
>>
>> 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/d26e9960/attachment.sig>