Command-line options

Agda accepts the following options on the command line. Where noted, these options can also serve as pragma options, i.e., be supplied in a file via the {-# OPTIONS ... #-} pragma or in the flags section of an .agda-lib file.

Setup and information

Some options cause Agda to perform tasks at startup like mandatory setup or printing some information. These options are not exclusive, they can be used with other options, albeit this seldom makes sense. They are not executed in the order given on the command line, but in the fixed order listed in the following:

--setup: Added in version 2.8.0.

Extract Agda’s data files (primitive library, emacs mode etc.) to the data directory (see --print-data-dir).

--version, -V

Show version number and cabal flags used in this build of Agda.

Overwrites --numeric-version.

--numeric-version

Show just the version number.

Overwrites --version.

--help[={TOPIC}], -?[{TOPIC}]

Show basically this help, or more help about TOPIC. Available topics:

emacs-mode: Explain the option --emacs-mode.
error: List the names of Agda’s errors.
warning: List warning groups and individual warnings and their default status. Instruct how to toggle benign warnings.

Overwrites itself, i.e., only the last of several --help options is effective.

--print-options: Added in version 2.9.0.

Print a simple list of all options, suitable for implementing bash completion.

--build-library: Added in version 2.8.0.

Expects an .agda-lib file in the current directory (or in a parent directory) and type-checks all Agda files found in the include directories of the library or in subdirectories thereof.

--print-app-dir: Added in version 2.6.4.1.

Outputs the (AGDA_DIR) directory containing Agda’s application configuration files, such as the defaults and libraries files, as described in Library Management.

--print-data-dir

Added in version 2.6.4.1.

Outputs the root of the directory structure holding Agda’s data files such as core libraries, style files for the backends, etc.

Since 2.8.0, the data directory is determined as follows:

The default data directory is defined at build time, either as the standard data directory defined by Cabal, or, if the use-xdg-data-home Cabal flag is enabled, as $XDG_DATA_HOME/agda/$AGDA_VERSION.
The data directory can be set at runtime using the Mikan_datadir environment variable and defaults to the default data directory. It can be printed with this flag.

--emacs-mode={COMMAND}

Added in version 2.8.0.

Administer the Agda Emacs mode, a task previously managed by the agda-mode executable.

Available commands:

setup: Install the Emacs mode into .emacs.
compile: Compile the Elisp files of the Emacs mode.
locate: Print the path to the Emacs mode.

More information in Section Emacs.

This option can be given several times to perform several commands.

General options

--interaction: For use with the Emacs mode (no need to invoke yourself).

--parallel[=N], -j[N]

Added in version 2.9.0.

Type check in parallel. N is optional, and controls the number of threads to use for checking. If N is omitted, or explicitly set to 0, the number of processors is used. The default, -j1, means type checking is sequential. Parallelism has module granularity.

Parallel type checking trades space for time, with (generally) a decrease in wall-clock time larger than the corresponding increase in total memory usage. Type-checking of a module can not start until all of its dependencies have been checked, so wider dependency graphs will see more speedup than taller dependency graphs.

Using too many cores can make the space-time tradeoff worse. The appropriate number will depend on the specifics of the project being checked.

A reasonable number to start with is -j8.

--interaction-json: Added in version 2.6.1.

For use with other editors such as Atom (no need to invoke yourself).

--interaction-exit-on-error

Added in version 2.6.3.

Makes Agda exit with a non-zero exit code if --interaction or --interaction-json are used and a type error is encountered. The option also makes Agda exit with exit code 113 if Agda fails to parse a command.

This option might for instance be used if Agda is controlled from a script.

--trace-imports[=(0|1|2|3)]

Added in version 2.6.4.

Configure printing of messages when an imported module is accessed during type-checking.

`0`	Do not print any messages about checking a module.
`1`	Print only Checking … when an access to an uncompiled module occurs. This is the default behavior if `--trace-imports` is not specified.
`2`	Use the effect of `1`, but also print Finished … when a compilation of an uncompiled module is finished. This is the behavior if `--trace-imports` is specified without a value.
`3`	Use the effect of `2`, but also print Loading … when a compiled module (interface) is accessed during the type-checking.

--colour[=(auto|always|never)], --color[=(auto|always|never)]

Added in version 2.6.4: Configure whether or not Agda’s standard output diagnostics should use ANSI terminal colours for syntax highlighting (e.g. error messages, warnings).

`always`	Always print diagnostic in colour.
`auto`	Automatically determine whether or not it is safe for standard output to include colours. Colours will be used when writing directly to a terminal device on Linux and macOS. This is the default value.
`never`	Never print output in colour.

The American spelling, --color, is also accepted.

Note: Currently, the colour scheme for terminal output can not be configured. If the colours are not legible on your terminal, please use --colour=never for now.

--only-scope-checking: Added in version 2.5.3.

Only scope-check the top-level module, do not type-check it (see Quicker generation without typechecking).

--transliterate

Added in version 2.6.3.

When writing to stdout or stderr Agda will (hopefully) replace code points that are not supported by the current locale or code page by something else, perhaps question marks.

This option is not supported when --interaction or --interaction-json are used, because when those options are used Agda uses UTF-8 when writing to stdout (and when reading from stdin).

Literate programming

--literate-markdown-only-agda-blocks

Added in version 2.9.0.

In literate Markdown (.lagda.md) and Typst (.lagda.typ) files, only treat code blocks explicitly marked with ````agda as Agda code. Unmarked code blocks (``) are treated as verbatim text and are not type-checked.

See Only agda code blocks for more details.

--no-literate-markdown-only-agda-blocks: Added in version 2.9.0.

Treat also unmarked code blocks as Agda code in literate Markdown and Typst files (default).

Compilation

--no-main

Do not treat the requested/current module as the main module of a program when compiling.

Pragma option since 2.5.3.

--main: Added in version 2.6.4.

Default, opposite of --no-main.

Generating highlighted source code

--dependency-graph={FILE}: Added in version 2.3.0.

Generate a Dot file FILE with a module dependency graph.

--dependency-graph-include={LIBRARY}

Added in version 2.6.3.

Include modules from the given library in the dependency graph. This option can be used multiple times to include modules from several libraries. If this option is not used at all, then all modules are included. (Note that the module given on the command line might not be included.)

A module M is considered to be in the library L if L is the name of an .agda-lib file associated to M (even if M’s file cannot be found via the include paths given in the .agda-lib file).

--html: Added in version 2.2.0.

Generate HTML files with highlighted source code (see Generating HTML for description and further options).

--latex: Added in version 2.3.2.

Generate LaTeX with highlighted source code (see Generating LaTeX for description and further options).

--vim: Generate Vim highlighting files.

Imports and libraries

(see Library Management)

--ignore-all-interfaces: Added in version 2.6.0.

Don’t read any interface files, including builtin and primitive modules; only use this if you know what you are doing!

--ignore-interfaces: Don’t read interface files (re-type check everything, except for builtin and primitive modules).

--no-write-interfaces: Added in version 2.9.0.

Don’t write out interface files after type-checking a module.

--include-path={DIR}, -i {DIR}: Look for imports in DIR. This option can be given multiple times.

--library={DIR}, -l {LIB}: Added in version 2.5.1.

Use library LIB.

--library-file={FILE}: Added in version 2.5.1.

Use FILE instead of the standard libraries file.

--defaults-file={FILE}: Added in version Mikan.

Use FILE instead of the standard defaults file.

--no-default-libraries: Added in version 2.5.1.

Don’t use default library files.

--no-libraries: Added in version 2.5.2.

Don’t use any library files.

Command-line and pragma options

The following options can also be given in Agda files using the OPTIONS pragma.

Performance

--auto-inline: Added in version 2.6.2.

Turn on automatic compile-time inlining. See The INLINE and NOINLINE pragmas for more information.

--no-auto-inline: Added in version 2.5.4.

Disable automatic compile-time inlining (default). Only definitions marked INLINE will be inlined. Default since 2.6.2.

--caching, --no-caching

Added in version 2.5.4.

Enable or disable caching of typechecking.

Default: --caching.

--call-by-name: Added in version 2.6.2.

Disable call-by-need evaluation in the Agda Abstract Machine.

--no-call-by-name: Added in version 2.6.4.

Default, opposite of --call-by-name.

--no-fast-reduce: Added in version 2.6.0.

Disable reduction using the Agda Abstract Machine.

--fast-reduce: Added in version 2.6.4.

Default, opposite of --no-fast-reduce.

--no-forcing: Added in version 2.2.10.

Disable the forcing optimisation. Since Agda 2.6.1 it is a pragma option.

--forcing: Added in version 2.6.4.

Default, opposite of --no-forcing.

--no-projection-like

Added in version 2.6.1.

Turn off the analysis whether a type signature likens that of a projection.

Projection-likeness is an optimization that reduces the size of terms by dropping parameter-like reconstructible function arguments. Thus, it is advisable to leave this optimization on, the flag is meant for debugging Agda.

See also the NOT_PROJECTION_LIKE pragma.

--projection-like: Added in version 2.6.4.

Default, opposite of --no-projection-like.

Printing and debugging

--no-unicode: Added in version 2.5.4.

Do not use unicode characters to print terms.

--unicode: Added in version 2.6.4.

Default, opposite of --no-unicode.

--show-identity-substitutions: Added in version 2.6.2.

Show all arguments of metavariables when pretty-printing a term, even if they amount to just applying all the variables in the context.

--no-show-identity-substitutions: Added in version 2.6.4.

Default, opposite of --show-identity-substitutions.

--show-implicit: Show implicit arguments when printing.

--no-show-implicit: Added in version 2.6.4.

Default, opposite of --show-implicit.

--show-irrelevant: Added in version 2.3.2.

Show arguments of sort Prop when printing.

--no-show-irrelevant: Added in version 2.6.4.

Default, opposite of --show-irrelevant.

--verbose={N}, -v {N}: Set verbosity level to N. This only has an effect if Agda was installed with the debug Cabal flag. See Debugging for more information.

--profile={PROF}

Added in version 2.6.3.

Turn on profiling option PROF. Available options are

`internal`	Measure time taken by various parts of the system (type checking, serialization, etc)
`modules`	Measure time spent on individual (Agda) modules
`definitions`	Measure time spent on individual (Agda) definitions
`sharing`	Measure things related to sharing
`serialize`	Collect detailed statistics about serialization
`constraints`	Collect statistics about constraint solving
`metas`	Count number of created metavariables
`interactive`	Measure time of interactive commands
`conversion`	Count number of times various steps of the conversion algorithm are used (reduction, eta-expansion, syntactic equality, etc)

Only one of internal, modules, and definitions can be turned on at a time. You can also give --profile=all to turn on all profiling options (choosing internal over modules and definitions, use --profile=modules --profile=all to pick modules instead).

Copatterns and projections

--copatterns, --no-copatterns

Added in version 2.4.0.

Enable or disable definitions by copattern matching (see Copatterns).

Default: --copatterns (since 2.4.2.4).

--postfix-projections: Added in version 2.5.2.

Make postfix projection notation the default. On by default since 2.7.0.

--no-postfix-projections: Added in version 2.6.4.

Opposite of --postfix-projections.

Experimental features

--allow-exec: Added in version 2.6.2.

Enable system calls during type checking (see Reflection).

--no-allow-exec: Added in version 2.6.4.

Default, opposite of --allow-exec.

--lossy-unification, --no-lossy-unification: Added in version 2.6.2.

Enable a constraint-solving heuristic akin to first-order unification, see Lossy Unification. Implies --no-require-unique-meta-solutions.

--no-lossy-unification: Added in version 2.6.4.

Default, opposite of --lossy-unification.

--require-unique-meta-solutions, --no-require-unique-meta-solutions

Added in version 2.7.0.

When turned off, type checking is allowed to use heuristics to solve meta variables that do not necessarily guarantee unique solutions. In particular, it can make use of INJECTIVE_FOR_INFERENCE pragmas.

--no-require-unique-meta-solutions is implied by the --lossy-unification flag.

Default: --require-unique-meta-solutions

--prop, --no-prop

Added in version 2.6.0.

Enable or disable declaration and use of definitionally proof-irrelevant propositions (see proof-irrelevant propositions).

Default: --no-prop. In this case, Prop is since 2.6.4 not in scope by default (--import-sorts).

Errors and warnings

--allow-incomplete-matches: Added in version 2.6.1.

Succeed and create interface file regardless of incomplete pattern-matching definitions. See also the NON_COVERING pragma.

--no-allow-incomplete-matches: Added in version 2.6.4.

Default, opposite of --allow-incomplete-matches.

--allow-unsolved-metas: Succeed and create interface file regardless of unsolved meta variables (see Metavariables).

--no-allow-unsolved-metas: Added in version 2.6.4.

Default, opposite of --allow-unsolved-metas.

--no-positivity-check: Do not warn about not strictly positive data types (see Positivity Checking).

--positivity-check: Added in version 2.6.4.

Default, opposite of --no-positivity-check.

--no-termination-check: Do not warn about possibly nonterminating code (see Termination Checking).

--termination-check: Added in version 2.6.4.

Default, opposite of --no-termination-check.

--warning={GROUP|FLAG}, -W {GROUP|FLAG}: Added in version 2.5.3.

Set warning group or flag (see Warnings).

Pattern matching and equality

--exact-split, --no-exact-split

Added in version 2.5.1.

Require [do not require] all clauses in a definition to hold as definitional equalities unless marked CATCHALL (see Case trees).

Default: --no-exact-split.

--hidden-argument-puns, --no-hidden-argument-puns

Added in version 2.6.4.

Enable [disable] hidden argument puns.

Default: --no-hidden-argument-puns.

--no-eta-equality: Added in version 2.5.1.

Default records to no-eta-equality (see Eta-expansion).

--eta-equality: Added in version 2.6.4.

Default, opposite of --no-eta-equality.

--occurrence-analysis, --no-occurrence-analysis

Added in version 2.9.0.

Turns on or off automated occurrence analysis for functions. See Occurrence analysis.

Default: --occurrence-analysis.

--no-pattern-matching: Added in version 2.4.0.

Disable pattern matching completely.

--pattern-matching: Added in version 2.6.4.

Default, opposite of --no-pattern-matching.

--keep-pattern-variables

Added in version 2.6.1.

Prevent interactive case splitting from replacing variables with dot patterns (see Dot patterns).

Default since 2.7.0.

--no-keep-pattern-variables: Added in version 2.6.4.

Opposite of --keep-pattern-variables.

--infer-absurd-clauses, --no-infer-absurd-clauses

Added in version 2.6.4.

--no-infer-absurd-clauses prevents interactive case splitting and coverage checking from automatically filtering out absurd clauses. This means that these absurd clauses have to be written out in the Agda text. Try this option if you experience type checking performance degradation with omitted absurd clauses.

Default: --infer-absurd-clauses.

Recursion

--termination-depth={N}

Added in version 2.2.8.

Allow termination checker to count decrease/increase upto N, see Termination Checking.

Defaults to 3 since 2.9.0.

Sorts and universes

--level-universe, --no-level-universe

Added in version 2.6.4.

Makes Level live in its own universe LevelUniv and disallows having levels depend on terms that are not levels themselves. When this option is turned off, LevelUniv still exists, but reduces to Type (see level-universe).

Note: While compatible with the --cubical option, this option is currently not compatible with cubical builtin files.

Default: --no-level-universe.

Search depth and instances

--instance-search-depth={N}: Added in version 2.5.2.

Set instance search depth to N (default: 500; see Instance Arguments).

--inversion-max-depth={N}: Added in version 2.5.4.

Set maximum depth for pattern match inversion to N (default: 50). Should only be needed in pathological cases.

--backtracking-instance-search, --no-backtracking-instance-search

Added in version 2.7.0.

Consider [do not consider] recursive instance arguments during pruning of instance candidates, see Backtracking

Default: --no-backtracking-instance-search.

This option used to be called --overlapping-instances.

--qualified-instances, --no-qualified-instances

Added in version 2.6.2.

Consider [do not consider] instances that are (only) in scope under a qualified name.

Default: --qualified-instances.

--experimental-lazy-instances, --no-experimental-lazy-instances

Added in version 2.8.0.

Opt into the experimental, faster implementation of instance search. This is presently optional since it may potentially introduce regressions in code which relies on the order of constraint solving.

Default: --no-experimental-lazy-instances.

The --experimental-lazy-instances behaviour will be made the default and this flag will be removed in the future.

Other features

--double-check: Enable double-checking of all terms using the internal typechecker. Off by default.

--no-double-check: Added in version 2.6.2.

Opposite of --double-check. On by default.

--keep-covering-clauses: Added in version 2.6.3.

Save function clauses computed by the coverage checker to the interface file. Required by some external backends.

--no-keep-covering-clauses: Added in version 2.6.4.

Opposite of --keep-covering-clauses, default.

--no-print-pattern-synonyms: Added in version 2.5.4.

Always expand Pattern Synonyms during printing. With this option enabled you can use pattern synonyms freely, but Agda will not use any pattern synonyms when printing goal types or error messages, or when generating patterns for case splits.

--print-pattern-synonyms: Added in version 2.6.4.

Default, opposite of --no-print-pattern-synonyms.

--safe: Added in version 2.3.0.

Disable postulates and unsafe OPTIONS pragmas. Further reading: Safe Agda.

--no-import-sorts: Added in version 2.6.2.

Disable the implicit statement open import Agda.Primitive using (Type; ...) at the start of each top-level Agda module.

--import-sorts

Added in version 2.6.4.

Default, opposite of --no-import-sorts.

Brings Type, Typeω, SSet and SSetω into scope, and if --prop is active, also Prop.

--no-load-primitives

Added in version 2.6.3.

Do not load the primitive modules (Agda.Primitive, Agda.Primitive.Cubical) when type-checking this program. This is useful if you want to declare Agda’s very magical primitives in a Literate Agda file of your choice.

If you are using this option, it is your responsibility to ensure that all of the BUILTIN things defined in those modules are loaded. Agda will not work otherwise.

Implies --no-import-sorts.

Incompatible with --safe.

--load-primitives: Added in version 2.6.4.

Default, opposite of --no-load-primitives.

--save-metas, --no-save-metas

Added in version 2.6.3.

Save [or do not save] meta-variables in .agdai files. Not saving means that all meta-variable solutions are inlined into the interface. Currently, even if --save-metas is used, very few meta-variables are actually saved, and this option is more like an anticipation of possible future optimizations.

Default: --no-save-metas.

--lossy-unification: Added in version 2.6.4.

Enable lossy unification, see Lossy Unification.

--quote-metas: Added in version 2.9.0.

Allow typechecking to quote terms that contain metas, see Quote Metas.

--no-quote-metas

Added in version 2.9.0.

Block typechecking when attempting to quote terms that contain metas.

Opposite of --quote-metas, default.

Warnings

The -W or --warning option can be used to disable or enable different warnings. The flag -W error (or --warning=error) can be used to turn all warnings into errors, while -W noerror turns this off again.

A group of warnings can be enabled by -W {GROUP}, where GROUP is one of the following:

all: All of the existing warnings.

warn: Default warning level.

ignore: Ignore all warnings.

The command agda --help=warning provides information about which warnings are turned on by default.

Benign warnings

Individual non-fatal warnings can be turned on and off by -W {NAME} and -W no{NAME} respectively. The list containing any warning NAME can be produced by agda --help=warning:

AbsurdPatternRequiresAbsentRHS

Added in version 2.8.0.

(Previously named AbsurdPatternRequiresNoRHS.)

RHS given despite an absurd pattern in the LHS.

BuiltinDeclaresIdentifier: Added in version 2.7.0.

A BUILTIN pragma that declares an identifier, but has been given an existing one.

AsPatternShadowsConstructorOrPatternSynonym: Added in version 2.6.2.

@-patterns that shadow constructors or pattern synonyms.

CantGeneralizeOverSorts: Added in version 2.6.0.

Attempts to generalize over sort metas in variable declaration.

ClashesViaRenaming: Added in version 2.6.1.

Clashes introduced by renaming.

ConflictingPragmaOptions: Added in version 2.7.0.

Conflicting pragma options. For instance, both --this and --no-that when --this implies --that.

CoverageNoExactSplit: Added in version 2.5.3.

Failed exact split checks.

DeprecationWarning: Added in version 2.5.3.

Deprecated features.

DefinitionBeforeDeclaration: Added in version 2.9.0.

Definitions that occur in mutual blocks before their declarations.

DuplicateFields: Added in version 2.6.4.

record expression with duplicate field names.

DuplicateRecordDirective: Added in version 2.7.0.

Conflicting directives in a record declaration.

DuplicateUsing: Added in version 2.6.2.

Repeated names in using directive.

EmptyAbstract: Added in version 2.5.4.

Empty abstract blocks.

EmptyConstructor: Added in version 2.6.2.

Empty data _ where blocks.

EmptyField: Added in version 2.6.1.

Empty field blocks.

EmptyGeneralize: Added in version 2.6.0.

Empty variable blocks.

EmptyInstance: Added in version 2.5.4.

Empty instance blocks.

EmptyMacro: Added in version 2.5.4.

Empty macro blocks.

EmptyMutual: Added in version 2.5.4.

Empty mutual blocks.

EmptyPolarityPragma: Added in version 2.8.0.

POLARITY pragmas not giving any polarities.

EmptyPostulate: Added in version 2.5.4.

Empty postulate blocks.

EmptyPrimitive: Added in version 2.6.0.

Empty primitive blocks.

EmptyPrivate: Added in version 2.5.4.

Empty private blocks.

EmptyWhere: Added in version 2.6.2.

Empty where blocks.

FaceConstraintCannotBeHidden: Added in version 2.6.4.

Face constraint patterns that are given as implicit arguments.

FaceConstraintCannotBeNamed: Added in version 2.6.4.

Face constraint patterns that are given as named arguments.

FixityInRenamingModule: Added in version 2.6.1.

Fixity annotations in renaming directives for a module.

HiddenGeneralize: Added in version 2.6.3.

Hidden identifiers in variable blocks.

IllegalDeclarationInDataDefinition: Added in version 2.6.4.

Declarations inside of a data definition that are not constructor type signatures.

IllformedAsClause: Added in version 2.6.0.

Illformed as-clauses in import statements.

InlineNoExactSplit: Added in version 2.6.4.

Failed exact splits after inlining a constructor, see The INLINE and NOINLINE pragmas.

InstanceNoOutputTypeName: Added in version 2.6.0.

Instance arguments whose type does not end in a named or variable type; such are never considered by instance search.

InstanceArgWithExplicitArg: Added in version 2.6.0.

Instance arguments with explicit arguments; such are never considered by instance search.

InstanceWithExplicitArg: Added in version 2.6.0.

Instance declarations with explicit arguments; such are never considered by instance search.

InteractionMetaBoundaries: Added in version 2.6.4.

Interaction meta variables that have unsolved boundary constraints.

InvalidCatchallPragma: Added in version 2.5.4.

CATCHALL pragmas before a non-function clause.

InvalidCharacterLiteral: Added in version 2.6.4.

Illegal character literals such as surrogate code points.

InvalidConstructorBlock: Added in version 2.6.2.

constructor blocks outside of interleaved mutual blocks.

InvalidCoverageCheckPragma: Added in version 2.6.1.

NON_COVERING pragmas before non-function or mutual blocks.

InvalidDataOrRecDefParameter: Added in version 2.9.0.

A data/record D parameters where definition where the parameters do not match up with the previously given signature or contain more than just names with hiding information.

InvalidNoPositivityCheckPragma: Added in version 2.5.4.

NO_POSITIVITY_CHECK pragmas before something that is neither a data nor record declaration nor a mutual block.

InvalidNoUniverseCheckPragma: Added in version 2.6.0.

NO_UNIVERSE_CHECK pragmas before declarations other than data or record declarations.

InvalidTacticAttribute: Added in version 2.9.0.

@(tactic …) attributes where they are not supported.

InvalidTerminationCheckPragma: Added in version 2.5.4.

Termination checking pragmas before non-function or mutual blocks.

InversionDepthReached: Added in version 2.5.4.

Inversions of pattern-matching failed due to exhausted inversion depth.

LibUnknownField: Added in version 2.6.0.

Unknown fields in library files.

MisplacedAttributes: Added in version 2.8.0.

Attributes where they cannot appear.

MissingTypeSignatureForOpaque: Added in version 2.7.0.

abstract or opaque definitions that lack a type signature.

ModuleDoesntExport: Added in version 2.6.0.

Names mentioned in an import statement which are not exported by the module in question.

NoMain: Added in version 2.7.0.

Invoking the compiler on a module without a main function. See also --no-main.

NotAffectedByOpaque: Added in version 2.6.4.

Declarations that should not be inside opaque blocks.

NotInScope: Added in version 2.6.1.

Out of scope names.

OldBuiltin: Added in version 2.5.2.

Deprecated BUILTIN pragmas.

OpenImportAbstract: Added in version 2.8.0.

open or import statements in abstract blocks.

OpenImportPrivate: Added in version 2.8.0.

open or import statements in private blocks.

OptionRenamed: Added in version 2.6.3.

Renamed options.

PatternShadowsConstructor: Added in version 2.6.4.

Pattern variables that shadow constructors.

PolarityPragmasButNotPostulates: Added in version 2.5.4.

Polarity pragmas for non-postulates.

PragmaCompileWrongName: Added in version 2.8.0.

COMPILE pragmas referring to identifiers that are neither definitions nor constructors.

PragmaExpectsDefinedSymbol: Added in version 2.8.0.

Pragmas referring to identifiers that are not defined symbols.

PragmaExpectsUnambiguousConstructorOrFunction: Added in version 2.8.0.

Pragmas referring to identifiers that are not unambiguous constructors or functions.

PragmaExpectsUnambiguousProjectionOrFunction: Added in version 2.8.0.

Pragmas referring to identifiers that are not unambiguous projections or functions.

PragmaNoTerminationCheck: Added in version 2.6.0.

NO_TERMINATION_CHECK pragmas; such are deprecated.

InvalidDisplayForm: Added in version 2.8.0.

An illegal DISPLAY form; it will be ignored.

RewritesNothing: Added in version 2.8.0.

rewrite clauses that do not fire.

ShadowingInTelescope: Added in version 2.6.1.

Repeated variable name in telescope.

ShouldBeEtaRecordPattern: Added in version 2.9.0.

Irrefutable record pattern without eta.

TooManyArgumentsToSort: Added in version 2.8.0.

E.g. Type used with more than one argument.

TooManyFields: Added in version 2.6.4.

Record expression with invalid field names.

TooManyPolarities: Added in version 2.8.0.

POLARITY pragma with too many polarities given.

UnfoldingWrongName: Added in version 2.8.0.

Names in an unfolding clause that are not unambiguous definitions.

UnfoldTransparentName: Added in version 2.6.4.

Non-opaque names mentioned in an unfolding clause.

UnknownAttribute: Added in version 2.8.0.

Unknown attributes.

UnknownFixityInMixfixDecl: Added in version 2.5.4.

Mixfix names without an associated fixity declaration.

UnknownPolarity: Added in version 2.8.0.

Unknown polarities.

UnreachableClauses: Added in version 2.5.3.

Unreachable function clauses.

UnsupportedAttribute: Added in version 2.6.2.

Unsupported attributes.

UnsupportedIndexedMatch: Added in version 2.6.3.

Failures to compute full equivalence when splitting on indexed family.

UnusedImports

Added in version 2.9.0.

Warn about openings of modules that do not bring identifiers into scope that are subsequently used. If the open comes with an explicit using or renaming directive, warn about individual unused identifiers (typically those mentioned in the directive). There is no warning about public openings. In the presence of option:–no-qualified-instances, there are also no warnings about unused instances brought into scope.

This warning is off by default.

UnusedImports=all

Added in version 2.9.0.

Same as UnusedImports, but warn about each unused identifier also when no using or renaming directive is given.

Option -WnoUnusedImports disables both UnusedImports and UnusedImports=all.

UnusedVariablesInDisplayForm: Added in version 2.8.0.

DISPLAY forms that bind variables they do not use.

UselessAbstract: Added in version 2.5.4.

abstract blocks where they have no effect.

UselessHiding: Added in version 2.6.2.

Names in hiding directive that are anyway not imported.

UselessInline: Added in version 2.5.3.

INLINE pragmas where they have no effect.

UselessImport: Added in version 2.9.0.

import statements that do not bring anything into scope.

UselessInstance: Added in version 2.5.4.

instance blocks where they have no effect.

UselessMacro: Added in version 2.7.0.

macro blocks where they have no effect.

UselessOpaque: Added in version 2.6.4.

opaque blocks that have no effect.

UselessPatternDeclarationForRecord: Added in version 2.6.2.

pattern directives where they have no effect.

UselessPragma: Added in version 2.6.4.

Pragmas that get ignored.

UselessPrivate: Added in version 2.5.4.

private blocks where they have no effect.

UselessPublic: Added in version 2.5.3.

public directives where they have no effect.

UselessTactic: Added in version 2.8.0.

@tactic attributes in non-hidden and instance arguments.

UserWarning: Added in version 2.5.4.

User-defined warnings added using one of the WARNING_ON_* pragmas.

WarningProblem: Added in version 2.7.0.

Problem encountered with option -W, like an unknown warning or the attempt to switch off a non-benign warning.

WithClauseProjectionFixityMismatch: Added in version 2.8.0.

Projection fixity different in with-clause compared to its parent clause.

WrongInstanceDeclaration: Added in version 2.6.0.

Terms marked as eligible for instance search whose type does not end with a name.

CustomBackendWarning: Added in version 2.7.0.

Warnings from custom backends.

Error warnings

Some warnings are fatal; those are errors Agda first ignores but eventually raises. Such error warnings are always on, they cannot be toggled by -W.

AbstractInLetBindings: Added in version 2.8.0.

Let bindings can not be made abstract.

CoinductiveEtaRecord: Added in version 2.7.0.

Declaring a record type as both coinductive and having eta-equality.

CoInfectiveImport: Added in version 2.6.0.

Importing a file not using e.g. --safe from one which does.

ConstructorDoesNotFitInData: Added in version 2.7.0.

Constructor with arguments in a universe higher than the one of its data type.

CoverageIssue: Added in version 2.5.3.

Failed coverage checks.

HiddenNotInArgumentPosition: Added in version 2.8.0.

Hidden arguments { x } can only appear as arguments to functions, not as expressions by themselves.

InfectiveImport: Added in version 2.6.0.

Importing a file using e.g. --prop into one which does not.

InstanceNotInArgumentPosition: Added in version 2.8.0.

Instance arguments ⦃ x ⦄ can only appear as arguments to functions, not as expressions by themselves.

MacroInLetBindings: Added in version 2.8.0.

Macros can not be let-bound.

MismatchedBrackets: Added in version 2.9.0.

An idiom bracket opened with unicode (resp. ASCII) syntax must also be closed with unicode (resp. ASCII) syntax.

MissingDataDeclaration: Added in version 2.8.0.

Constructor definitions not associated to a data declaration.

MissingDefinitions: Added in version 2.6.0.

Names declared without an accompanying definition.

NotAllowedInMutual: Added in version 2.6.0.

Declarations that are not allowed in a mutual block.

NotStrictlyPositive: Added in version 2.5.2.

Failed strict positivity checks.

OverlappingTokensWarning: Added in version 2.5.4.

Multi-line comments spanning one or more literate text blocks.

PragmaCompiled: Added in version 2.6.0.

COMPILE pragmas not allowed in safe mode.

RecursiveRecordNeedsInductivity: Added in version 2.7.0.

Recursive records that are neither declared inductive nor coinductive.

SafeFlagEta: Added in version 2.6.1.

ETA pragmas with the --safe flag.

SafeFlagInjective: Added in version 2.6.1.

INJECTIVE pragmas with the --safe flag.

SafeFlagNoCoverageCheck: Added in version 2.6.1.

NON_COVERING pragmas with the --safe flag.

SafeFlagNonTerminating: Added in version 2.5.3.

NON_TERMINATING pragmas with the --safe flag.

SafeFlagNoPositivityCheck: Added in version 2.5.3.

NO_POSITIVITY_CHECK pragmas with the --safe flag.

SafeFlagNoUniverseCheck: Added in version 2.6.0.

NO_UNIVERSE_CHECK pragmas with the --safe flag.

SafeFlagPolarity: Added in version 2.5.3.

POLARITY pragmas with the --safe flag.

SafeFlagPostulate: Added in version 2.5.3.

postulate blocks with the --safe flag.

SafeFlagPragma: Added in version 2.5.3.

Unsafe OPTIONS pragmas with the --safe flag.

SafeFlagTerminating: Added in version 2.5.3.

TERMINATING pragmas with the --safe flag.

TerminationIssue: Added in version 2.5.2.

Failed termination checks.

UnknownNamesInFixityDecl: Added in version 2.5.4.

Names not declared in the same scope as their syntax or fixity declaration.

UnknownNamesInPolarityPragmas: Added in version 2.5.4.

Names not declared in the same scope as their polarity pragmas.

UnsolvedConstraints: Added in version 2.5.2.

Unsolved constraints.

UnsolvedInteractionMetas: Added in version 2.5.2.

Unsolved interaction meta variables.

UnsolvedMetaVariables: Added in version 2.5.2.

Unsolved meta variables.

Command-line examples

Run Agda with all warnings enabled, except for warnings about empty abstract blocks:

agda -W all --warning=noEmptyAbstract file.agda

Run Agda on a file which uses the standard library. Note that you must have already created a libraries file as described in Library Management.

agda -l standard-library -i. file.agda

(Or if you have added standard-library to your defaults file, simply agda file.agda.)

Checking options for consistency

Agda checks that options used in imported modules are consistent with each other.

An infective option is an option that if used in one module, must be used in all modules that depend on this module. The following options are infective:

--prop

A coinfective option is an option that if used in one module, must be used in all modules that this module depends on. The following options are coinfective:

--level-universe
--safe

Agda records the options used when generating an interface file. If any of the following options differ when trying to load the interface again, the source file is re-typechecked instead:

References

[1] Jesper Cockx and Dominique Devriese. “Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory.” In Journal of Functional Programming 28, 2018.