agda-unused: Check for unused code in an Agda project.

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

A tool to check for unused code in an Agda project.


[Skip to Readme]

Properties

Versions 0.1.0, 0.2.0, 0.2.0
Change log CHANGELOG.md
Dependencies aeson (>=1.4.7 && <1.6), Agda (==2.6.1.*), agda-unused, base (>=4.13 && <4.15), containers (>=0.6.2 && <0.7), directory (>=1.3.6 && <1.4), filepath (>=1.4.2 && <1.5), mtl (>=2.2.2 && <2.3), optparse-applicative (>=0.15.1 && <0.17), text (>=1.2.4 && <1.3) [details]
License MIT
Author
Maintainer Matt Superdock <msuperdock@gmail.com>
Category Dependent types
Source repo head: git clone https://github.com/msuperdock/agda-unused.git
Uploaded by msuperdock at 2021-05-05T02:29:27Z

Modules

[Index]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for agda-unused-0.2.0

[back to package description]

agda-unused

agda-unused checks for unused code in an Agda project, including:

agda-unused takes a filepath representing an Agda code file and checks for unused code in that file and its dependencies. By default, agda-unused does not check public items that could be imported elsewhere. But with the --global flag, agda-unused treats the given file as a description of the public interface of the project, and additionally checks for unused files and unused public items in dependencies. (See below for more on the --global flag.)

Supported Agda versions: >= 2.6.1 && < 2.6.2

Example

File ~/Test.agda:

module Test where

open import Agda.Builtin.Bool
  using (Bool; false; true)
open import Agda.Builtin.Unit

_∧_
  : Bool
  → Bool
  → Bool
false ∧ x
  = false
_ ∧ y
  = y

Command:

$ agda-unused Test.agda

Output:

/home/user/Test.agda:4,23-27
  unused imported item ‘true’
/home/user/Test.agda:5,1-30
  unused import ‘Agda.Builtin.Unit’
/home/user/Test.agda:11,9-10
  unused variable ‘x’

Usage

agda-unused - check for unused code in an Agda project

Usage: agda-unused FILE [-g|--global] [-j|--json]
  Check for unused code in FILE

Available options:
  -h,--help                Show this help text
  -g,--global              Check project globally
  -j,--json                Format output as JSON
  -i,--include-path DIR    Look for imports in DIR
  -l,--library LIB         Use library LIB
  --library-file FILE      Use FILE instead of the standard libraries file
  --no-libraries           Don't use any library files
  --no-default-libraries   Don't use default libraries

Global

If the --global flag is given, all declarations in the given file must be imports. The set of imported items is treated as the public interface of the project; these items will not be marked unused. The public items in dependencies of the given module may be marked unused, unlike the default behavior. We also check for unused files.

To perform a global check on an Agda project, first create a file that imports exactly the intended public interface of your project. For example:

File All.agda:

module All where

import A
  using (f)
import B
  hiding (g)
import C

Command:

$ agda-unused All.agda --global

JSON

If the --json flag is given, the output is a JSON object with two fields:

The "none" type indicates that there is no unused code.

Approach

We make a single pass through the given Agda module and its dependencies:

This means, for example, if we have three definitions (say f, g, h), each depending on the previous one, where h is not a root, then f and g are considered used, while h is considered unused. If we remove h and run agda-unsed again, it will now report that g is unused. This behavior is different from Haskell's built-in tool, which would report that all three identifiers are unused on the first run.

Limitations

We work with Agda's concrete syntax. This is a necessary choice, since Agda's abstract syntax doesn't distinguish between qualified and (opened) unqualified names, which would make it impossible to determine whether certain open statements are unused. However, using concrete syntax comes with several drawbacks:

Additionally, we currently do not support the following Agda features:

agda-unused will produce an error if your code uses these language features.