Discussion:
[Agda] Redundant imports
Martín Hötzel Escardó
2018-04-23 19:55:03 UTC
Permalink
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? This is important to try speed up "reloading" in
interactive mode. (Although already this refactoring has improved this bit.)

Thanks,
Martin
Nils Anders Danielsson
2018-04-24 08:54:06 UTC
Permalink
Post by Martín Hötzel Escardó
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
--
/NAD
Guillaume Allais
2018-04-25 11:40:04 UTC
Permalink
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
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.
Post by Nils Anders Danielsson
Post by Martín Hötzel Escardó
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
   https://github.com/agda/agda/issues/2503
Martin Escardo
2018-04-25 11:53:07 UTC
Permalink
Post by 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.
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
Post by Guillaume Allais
Hope it helps!
Cheers,
--
gallais
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.
Post by Nils Anders Danielsson
Post by Martín Hötzel Escardó
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
   https://github.com/agda/agda/issues/2503
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
Guillaume Allais
2018-04-25 12:03:12 UTC
Permalink
I think you have to either use `--warning` or `-W` but `--W` won't work.
Post by Martin Escardo
Post by 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.
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
Post by Guillaume Allais
Hope it helps!
Cheers,
--
gallais
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.
Post by Nils Anders Danielsson
Post by Martín Hötzel Escardó
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
    https://github.com/agda/agda/issues/2503
Martin Escardo
2018-04-25 12:23:14 UTC
Permalink
Post by Guillaume Allais
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
Post by Guillaume Allais
Post by Martin Escardo
Post by 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.
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
Post by Guillaume Allais
Hope it helps!
Cheers,
--
gallais
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.
Post by Nils Anders Danielsson
Post by Martín Hötzel Escardó
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
    https://github.com/agda/agda/issues/2503
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
Sergei Meshveliani
2018-04-24 09:59:50 UTC
Permalink
I also suffer of redundant import.
Even a slight code change often leads to redundant import.

------
Sergei
Post by Martín Hötzel Escardó
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? This is important to try speed up "reloading" in
interactive mode. (Although already this refactoring has improved this bit.)
Thanks,
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Loading...