[Agda] Redundant imports

[Martin Escardo]

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
>>>
>>
> 
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe