Command-line options

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

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

Added in version 2.6.2.

Alias of --print-agda-data-dir.

--print-agda-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 build flag is enabled, as $XDG_DATA_HOME/agda/$AGDA_VERSION.

  • The data directory can be set at runtime using the Agda_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).

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

--interactive, -I

Start in interactive mode (not maintained).

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

Compilation

See Compilers for backend-specific options.

--compile-dir={DIR}

Set DIR as directory for compiler output (default: the project root).

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

--with-compiler={PATH}

Set PATH as the executable to call to compile the backend’s output (default: ghc for the GHC backend).

Generating highlighted source code

--count-clusters

Added in version 2.5.3.

Count extended grapheme clusters when generating LaTeX code (see Counting Extended Grapheme Clusters). Available only when Agda was built with Cabal flag enable-cluster-counting.

Pragma option since 2.5.4.

--no-count-clusters

Added in version 2.6.4.

Opposite of --count-clusters. Default.

--css={URL}

Set URL of the CSS file used by the HTML files to URL (can be relative).

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

--highlight-occurrences

Added in version 2.6.2.

When generating HTML, place the highlight-hover.js script in the output directory (see --html-dir). In the presence of the script, hovering over an identifier in the rendering of the HTML will highlight all occurrences of the same identifier on the page.

--html

Added in version 2.2.0.

Generate HTML files with highlighted source code (see Generating HTML).

--html-dir={DIR}

Set directory in which HTML files are placed to DIR (default: html).

--html-highlight=[code,all,auto]

Added in version 2.6.0.

Whether to highlight non-Agda code as comments in generated HTML files (default: all; see Generating HTML).

--latex

Added in version 2.3.2.

Generate LaTeX with highlighted source code (see Generating LaTeX).

--latex-dir={DIR}

Added in version 2.5.2.

Set directory in which LaTeX files are placed to DIR (default: latex).

--vim

Generate Vim highlighting files.

Imports and libraries

(see Library Management)

--ignore-all-interfaces

Added in version 2.6.0.

Ignore all interface files, including builtin and primitive modules; only use this if you know what you are doing!

--ignore-interfaces

Ignore interface files (re-type check everything, except for builtin and primitive modules).

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

--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 irrelevant arguments 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 flag.

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

--confluence-check, --local-confluence-check, --no-confluence-check

Added in version 2.6.1.

Enable optional (global or local) confluence checking of REWRITE rules (see Confluence checking).

Default is --no-confluence-check.

--cubical

Added in version 2.6.0.

Enable cubical features. Turns on --cubical-compatible and --without-K (see Cubical).

--erased-cubical

Added in version 2.6.3.

Enable a variant of Cubical Agda, and turn on --without-K.

--experimental-irrelevance

Added in version 2.3.0.

Enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching) (see Irrelevance).

--no-experimental-irrelevance

Added in version 2.6.4.

Default, opposite of --experimental-irrelevance.

--guarded

Added in version 2.6.2.

Enable locks and ticks for guarded recursion (see Guarded Type Theory).

--no-guarded

Added in version 2.6.4.

Default, opposite of --guarded.

--injective-type-constructors

Added in version 2.2.8.

Enable injective type constructors (makes Agda anti-classical and possibly inconsistent).

--no-injective-type-constructors

Added in version 2.6.4.

Default, opposite of --injective-type-constructors.

--irrelevant-projections, --no-irrelevant-projections

Added in version 2.5.4.

Enable [disable] projection of irrelevant record fields (see Irrelevance). The option --irrelevant-projections makes Agda inconsistent.

Default (since version 2.6.1): --no-irrelevant-projections.

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

--rewriting

Added in version 2.4.2.4.

Enable declaration and use of REWRITE rules (see Rewriting).

--no-rewriting

Added in version 2.6.4.

Default, opposite of --rewriting.

--two-level

Added in version 2.6.2.

Enable the use of strict (non-fibrant) type universes SSet (two-level type theory). Since 2.6.4, brings SSet into scope unless --no-import-sorts.

--no-two-level

Added in version 2.6.4.

Default, opposite of --two-level.

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.

--cohesion

Added in version 2.6.3.

Enable the cohesion modalities, in particular @♭ (see Flat Modality).

--no-cohesion

Added in version 2.6.4.

Default, opposite of --cohesion.

--flat-split

Added in version 2.6.1.

Enable pattern matching on @♭ arguments (see Pattern Matching on @♭). Implies --cohesion.

--no-flat-split

Added in version 2.6.4.

Default, opposite of --flat-split.

--polarity, --no-polarity

Added in version 2.6.5.

Enables the use of modal polarity annotations, and their interaction with the positivity checker. See Polarity Annotations.

Default: --no-polarity.

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

--with-K

Added in version 2.4.2.

Overrides a global --without-K in a file (see Without K).

--without-K

Added in version 2.2.10.

Disables reasoning principles incompatible with univalent type theory, most importantly Streicher’s K axiom (see Without K).

--cubical-compatible

Added in version 2.6.3.

Generate internal support code necessary for use from Cubical Agda (see Cubical compatible). Implies --without-K.

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

--large-indices, --no-large-indices

Added in version 2.6.4.

Allow constructors to store values of types whose sort is larger than that being defined, when these arguments are forced by the constructor’s type.

When --safe is given, this flag can not be combined with --without-K or --forced-argument-recursion, since both of these combinations are known to be inconsistent.

When --no-forcing is given, this option is redundant.

Default: --no-large-indices.

Recursion

--forced-argument-recursion, --no-forced-argument-recursion

Added in version 2.6.4.

Allow the use of forced constructor arguments as termination metrics. This flag may be necessary for Agda to accept nontrivial uses of induction-induction.

Default: --forced-argument-recursion.

--guardedness, --no-guardedness

Added in version 2.6.0.

Enable [disable] constructor-based guarded corecursion (see Coinduction).

The option --guardedness is inconsistent with sized types, thus, it cannot be used with both --safe and --sized-types.

Default: --no-guardedness (since 2.6.2).

--sized-types, --no-sized-types

Added in version 2.2.0.

Enable [disable] sized types (see Sized Types).

The option --sized-types is inconsistent with constructor-based guarded corecursion, thus, it cannot be used with both --safe and --guardedness.

Default: --no-sized-types (since 2.6.2).

--termination-depth={N}

Added in version 2.2.8.

Allow termination checker to count decrease/increase upto N (default: 1; see Termination Checking).

Sorts and universes

--type-in-type

Ignore universe levels (this makes Agda inconsistent; see type-in-type).

--no-type-in-type

Added in version 2.6.4.

Default, opposite of --type-in-type.

--omega-in-omega

Added in version 2.6.0.

Enable typing rule Setω : Setω (this makes Agda inconsistent; see omega-in-omega).

--no-omega-in-omega

Added in version 2.6.4.

Default, opposite of --omega-in-omega.

--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 Set (see level-universe).

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

Default: --no-level-universe.

--universe-polymorphism, --no-universe-polymorphism

Added in version 2.3.0.

Enable [disable] universe polymorphism (see Universe Levels).

Default: --universe-polymorphism.

--cumulativity, --no-cumulativity

Added in version 2.6.1.

Enable [disable] cumulative subtyping of universes, i.e., if A : Set i then also A : Set j for all j >= i.

Default: --no-cumulativity.

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.

Added in version 2.6.5.

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.

--no-syntactic-equality

Added in version 2.6.0.

Disable the syntactic equality shortcut in the conversion checker.

--syntactic-equality={N}

Added in version 2.6.3.

Give the syntactic equality shortcut N units of fuel (N must be a natural number).

If N is omitted, then the syntactic equality shortcut is enabled without any restrictions. (This is the default.)

If N is given, then the syntactic equality shortcut is given N units of fuel. The exact meaning of this is implementation-dependent, but successful uses of the shortcut do not affect the amount of fuel.

Note that this option is experimental and subject to change.

--safe

Added in version 2.3.0.

Disable postulates, unsafe OPTIONS pragmas and primTrustMe. Prevents to have both --sized-types and --guardedness on. Further reading: Safe Agda.

--no-import-sorts

Added in version 2.6.2.

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

--import-sorts

Added in version 2.6.4.

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

Brings Set into scope, and if --prop is active, also Prop, and if --two-level is active, even SSet.

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

Erasure

--erasure, --no-erasure

Added in version 2.6.4.

Allow use of the annotations @0 and @erased; allow use of names defined in Cubical Agda in Erased Cubical Agda; and mark parameters as erased in the type signatures of constructors and record fields (if --with-K is not active this is not done for indexed data types).

Default: --no-erasure.

--erased-matches, --no-erased-matches

Added in version 2.6.4.

Allow matching in erased positions for single-constructor, non-indexed data/record types. (This kind of matching is always allowed for record types with η-equality.)

Default: --erased-matches when --with-K is active, either by explicit activation or the absence of options like --without-K; otherwise --no-erased-matches.

If --erased-matches is given explicitly, it implies --erasure.

--erase-record-parameters

Added in version 2.6.3.

Mark parameters as erased in record module telescopes.

Implies --erasure.

--no-erase-record-parameters

Added in version 2.6.4.

Default, opposite of --erase-record-parameters.

--lossy-unification

Added in version 2.6.4.

Enable lossy unification, see Lossy Unification.

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

RHS given despite an absurd pattern in the LHS.

BuiltinDeclaresIdentifier

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

AsPatternShadowsConstructorOrPatternSynonym

@-patterns that shadow constructors or pattern synonyms.

CantGeneralizeOverSorts

Attempts to generalize over sort metas in variable declaration.

ClashesViaRenaming

Clashes introduced by renaming.

ConflictingPragmaOptions

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

ConfluenceCheckingIncompleteBecauseOfMeta

Incomplete confluence checks because of unsolved metas.

ConfluenceForCubicalNotSupported

Attempts to check confluence with --cubical.

CoverageNoExactSplit

Failed exact split checks.

DeprecationWarning

Deprecated features.

DuplicateFields

record expression with duplicate field names.

DuplicateRecordDirective

Conflicting directives in a record declaration.

DuplicateRewriteRule

Duplicate declaration of a name as REWRITE rule.

DuplicateUsing

Repeated names in using directive.

EmptyAbstract

Empty abstract blocks.

EmptyConstructor

Empty constructor blocks.

EmptyField

Empty field blocks.

EmptyGeneralize

Empty variable blocks.

EmptyInstance

Empty instance blocks.

EmptyMacro

Empty macro blocks.

EmptyMutual

Empty mutual blocks.

EmptyPolarityPragma

POLARITY pragmas not giving any polarities.

EmptyPostulate

Empty postulate blocks.

EmptyPrimitive

Empty primitive blocks.

EmptyPrivate

Empty private blocks.

EmptyRewritePragma

Empty REWRITE pragmas.

EmptyWhere

Empty where blocks.

FaceConstraintCannotBeHidden

Face constraint patterns that are given as implicit arguments.

FaceConstraintCannotBeNamed

Face constraint patterns that are given as named arguments.

FixingCohesion

Invalid cohesion annotations, automatically corrected.

FixingPolarity

Invalid polarity annotations, automatically corrected.

FixingRelevance

Invalid relevance annotations, automatically corrected.

FixityInRenamingModule

Fixity annotations in renaming directives for a module.

HiddenGeneralize

Hidden identifiers in variable blocks.

IllformedAsClause

Illformed as-clauses in import statements.

InlineNoExactSplit

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

InstanceNoOutputTypeName

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

InstanceArgWithExplicitArg

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

InstanceWithExplicitArg

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

InteractionMetaBoundaries

Interaction meta variables that have unsolved boundary constraints.

InvalidCatchallPragma

CATCHALL pragmas before a non-function clause.

InvalidCharacterLiteral

Illegal character literals such as surrogate code points.

InvalidConstructorBlock

constructor blocks outside of interleaved mutual blocks.

InvalidCoverageCheckPragma

NON_COVERING pragmas before non-function or mutual blocks.

InvalidNoPositivityCheckPragma

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

InvalidNoUniverseCheckPragma

NO_UNIVERSE_CHECK pragmas before declarations other than data or record declarations.

InvalidTerminationCheckPragma

Termination checking pragmas before non-function or mutual blocks.

InversionDepthReached

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

LibUnknownField

Unknown fields in library files.

MisplacedAttributes

Attributes where they cannot appear.

MissingTypeSignatureForOpaque

abstract or opaque definitions that lack a type signature.

ModuleDoesntExport

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

MultipleAttributes

Multiple attributes given where only erasure is accepted.

NoMain

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

NotAffectedByOpaque

Declarations that should not be inside opaque blocks.

NotARewriteRule

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

NotInScope

Out of scope names.

OldBuiltin

Deprecated BUILTIN pragmas.

OpenImportAbstract

open or import statements in abstract blocks.

OpenImportPrivate

open or import statements in private blocks.

OptionRenamed

Renamed options.

PatternShadowsConstructor

Pattern variables that shadow constructors.

PlentyInHardCompileTimeMode

Use of attributes @ω or @plenty in hard compile-time mode.

PolarityPragmasButNotPostulates

Polarity pragmas for non-postulates.

PragmaCompileErased

COMPILE pragma targeting an erased symbol.

PragmaCompileList

COMPILE pragma for GHC backend targeting lists.

PragmaCompileMaybe

COMPILE pragma for GHC backend targeting MAYBE.

PragmaCompileUnparsable

Unparsable COMPILE GHC pragmas.

PragmaCompileWrong

Ill-formed COMPILE GHC pragmas.

PragmaCompileWrongName

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

PragmaExpectsDefinedSymbol

Pragmas referring to identifiers that are not defined symbols.

PragmaExpectsUnambiguousConstructorOrFunction

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

PragmaExpectsUnambiguousProjectionOrFunction

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

PragmaNoTerminationCheck

NO_TERMINATION_CHECK pragmas; such are deprecated.

InvalidDisplayForm

An illegal DISPLAY form; it will be ignored.

RewriteLHSNotDefinitionOrConstructor

Rewrite rule head symbol is not a defined symbol or constructor.

RewriteVariablesNotBoundByLHS

Rewrite rule does not bind all of its variables.

RewriteVariablesBoundMoreThanOnce

Constructor-headed rewrite rule has non-linear parameters.

RewriteLHSReduces

Rewrite rule LHS is not in weak-head normal form.

RewriteHeadSymbolIsProjectionLikeFunction

Rewrite rule head symbol is a projection-like function.

RewriteHeadSymbolIsTypeConstructor

Rewrite rule head symbol is a type constructor.

RewriteHeadSymbolContainsMetas

Definition of rewrite rule head symbol contains unsolved metas.

RewriteConstructorParametersNotGeneral

Constructor-headed rewrite rule parameters are not fully general.

RewriteContainsUnsolvedMetaVariables

Rewrite rule contains unsolved metas.

RewriteBlockedOnProblems

Checking rewrite rule blocked by unsolved constraint.

RewriteRequiresDefinitions

Checking rewrite rule blocked by missing definition.

RewriteDoesNotTargetRewriteRelation

Rewrite rule does not target the rewrite relation.

RewriteBeforeFunctionDefinition

Rewrite rule is not yet defined.

RewriteBeforeMutualFunctionDefinition

Mutually declaration with the rewrite rule is not yet defined.

RewritesNothing

rewrite clauses that do not fire.

ShadowingInTelescope

Repeated variable name in telescope.

TooManyArgumentsToSort

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

TooManyFields

Record expression with invalid field names.

TooManyPolarities

POLARITY pragma with too many polarities given.

UnfoldingWrongName

Names in an unfolding clause that are not unambiguous definitions.

UnfoldTransparentName

Non-opaque names mentioned in an unfolding clause.

UnknownAttribute

Unknown attributes.

UnknownFixityInMixfixDecl

Mixfix names without an associated fixity declaration.

UnknownNamesInFixityDecl

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

UnknownNamesInPolarityPragmas

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

UnknownPolarity

Unknown polarities.

UnreachableClauses

Unreachable function clauses.

UnsupportedAttribute

Unsupported attributes.

UnsupportedIndexedMatch

Failures to compute full equivalence when splitting on indexed family.

UnusedVariablesInDisplayForm

DISPLAY forms that bind variables they do not use.

UselessAbstract

abstract blocks where they have no effect.

UselessHiding

Names in hiding directive that are anyway not imported.

UselessInline

INLINE pragmas where they have no effect.

UselessInstance

instance blocks where they have no effect.

UselessMacro

macro blocks where they have no effect.

UselessOpaque

opaque blocks that have no effect.

UselessPatternDeclarationForRecord

pattern directives where they have no effect.

UselessPragma

Pragmas that get ignored.

UselessPrivate

private blocks where they have no effect.

UselessPublic

public directives where they have no effect.

UselessTactic

@tactic attributes in non-hidden and instance arguments.

UserWarning

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

WarningProblem

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

WithClauseProjectionFixityMismatch

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

WithoutKFlagPrimEraseEquality

primEraseEquality used with the without-K flags.

WrongInstanceDeclaration

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

CustomBackendWarning

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.

CoinductiveEtaRecord

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

CoInfectiveImport

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

ConstructorDoesNotFitInData

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

CoverageIssue

Failed coverage checks.

InfectiveImport

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

MissingDataDeclaration

Constructor definitions not associated to a data declaration.

MissingDefinitions

Names declared without an accompanying definition.

NotAllowedInMutual

Declarations that are not allowed in a mutual block.

NotStrictlyPositive

Failed strict positivity checks.

OverlappingTokensWarning

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

PragmaCompiled

COMPILE pragmas not allowed in safe mode.

RewriteAmbiguousRules

Failed global confluence checks because of overlapping rules.

RewriteMaybeNonConfluent

Failed confluence checks while computing overlap.

RewriteMissingRule

Failed global confluence checks because of missing rules.

RewriteNonConfluent

Failed confluence checks while joining critical pairs.

SafeFlagEta

ETA pragmas with the --safe flag.

SafeFlagInjective

INJECTIVE pragmas with the --safe flag.

SafeFlagNoCoverageCheck

NON_COVERING pragmas with the --safe flag.

SafeFlagNonTerminating

NON_TERMINATING pragmas with the --safe flag.

SafeFlagNoPositivityCheck

NO_POSITIVITY_CHECK pragmas with the --safe flag.

SafeFlagNoUniverseCheck

NO_UNIVERSE_CHECK pragmas with the --safe flag.

SafeFlagPolarity

POLARITY pragmas with the --safe flag.

SafeFlagPostulate

postulate blocks with the --safe flag.

SafeFlagPragma

Unsafe OPTIONS pragmas with the --safe flag.

SafeFlagTerminating

TERMINATING pragmas with the --safe flag.

SafeFlagWithoutKFlagPrimEraseEquality

primEraseEquality used with the --safe and --without-K flags.

TerminationIssue

Failed termination checks.

TopLevelPolarity

Declaring definitions with an explicit polarity annotation.

UnsolvedConstraints

Unsolved constraints.

UnsolvedInteractionMetas

Unsolved interaction meta variables.

UnsolvedMetaVariables

Unsolved meta variables.

HiddenNotInArgumentPosition

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

InstanceNotInArgumentPosition

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

MacroInLetBindings

Macros can not be let-bound.

AbstractInLetBindings

Let bindings can not be made abstract.

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:

Furthermore --cubical and --erased-cubical are jointly infective: if one of them is used in one module, then one or the other must be used in all modules that depend on this module.

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:

Furthermore the option --cubical-compatible is mostly coinfective. If a module uses --cubical-compatible then all modules that this module imports (directly) must also use --cubical-compatible, with the following exception: if a module uses both --cubical-compatible and --with-K, then it is not required to use --cubical-compatible in (directly) imported modules that use --with-K. (Note that one cannot use --cubical-compatible and --with-K at the same time if --safe is used.)

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: