[Agda] Redundant imports

[Martin Escardo]

On 25/04/18 13:03, guillaume.allais at ens-lyon.org wrote:
> I think you have to either use `--warning` or `-W` but `--W` won't work.

Ah, sorry. :-)

That does the trick. It is very slow, as you say, but it is very useful. 
Thank you very much.

Martin


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

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