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.1.0, 0.2.0
Change log CHANGELOG.md
Dependencies aeson (>=1.4.7 && <1.5), Agda (==2.6.1.*), agda-unused, base (>=4.13.0 && <4.14), containers (>=0.6.2 && <0.7), directory (>=1.3.6 && <1.4), filepath (>=1.4.2 && <1.5), megaparsec (>=8.0.0 && <8.1), mtl (>=2.2.2 && <2.3), optparse-applicative (>=0.15.1 && <0.16), 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 2020-10-28T02:18:12Z

Modules

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for agda-unused-0.1.0

[back to package description]

agda-unused

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

agda-unused can be run globally on a full project, or locally on a file and its dependencies. Running agda-unused globally requires an .agda-roots file in the project root directory, which specifies the "roots" of the project. The "roots" of a project are identifiers that are considered used even if not used within the project itself. You might think of the .agda-roots file as a specification of the public interface of your project.

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

Roots

Running agda-unused globally requires an .agda-roots file in the project root directory. The .agda-roots format consists of:

All given module names not in parentheses are checked, along with their dependencies. The given identifiers are considered roots; they will not be marked unused. Qualified identifiers refer to identifiers defined within inner modules. If no identifiers are given for a module, all publicly accessible identifiers are considered roots.

All given module names in parentheses are ignored when checking for unused files. Such modules may still be checked if imported by another module.

Example .agda-roots file:

Main
- main

Pythagorean.Core
- isTriple
- allTriples

(Pythagorean.Examples)

Pythagorean.Theorems

Pythagorean.Utils
- Print.prettyNat

Spacing and indentation are irrelevant.

Usage

Usage: agda-unused [-r|--root ROOT] [-l|--local FILE]
  Check for unused code in project with root directory ROOT

Available options:
  -h,--help                Show this help text
  -r,--root ROOT           Path of project root directory
  -l,--local FILE          Path of file to check locally
  -j,--json                Format output as JSON 

The project root directory is determined as follows:

Approach

We make a single pass through each relevant Agda file:

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.

For a global check, we check each file appearing in .agda-roots and its dependencies. For a local check, we check just the given file and its dependencies, ignoring all publicly accessible definitions.

JSON

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

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

Limitations

We currently do not support the following Agda features:

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