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.

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

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

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

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

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.

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.

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

--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, --cubical=full

Added in version 2.6.0.

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

--cubical=erased, --erased-cubical

Added in version 2.6.3.

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

--cubical=no-glue

Added in version 2.9.0.

Enable a variant of Cubical Agda without the Glue types. Turns on --cubical=compatible and --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.

This makes Agda anti-classical: injective type constructors are incompatible with the law of excluded middle, see theorem 93 (attributed to Chung-Kil Hur) by Cockx and Devriese [1].

It is also incompatible with univalence, by theorem 92 of the same paper.

Additionally, this possibly makes Agda 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.

--local-rewriting

Added in version 2.9.0.

Enable declaring local rewrite rules with the @rewrite attribute (see Local Rewriting).

--no-local-rewriting

Added in version 2.9.0.

Default, opposite of --local-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.8.0.

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

Default: --no-polarity.

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

--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, --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, see Termination Checking.

Defaults to 3 since 2.9.0.

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

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

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

ConfluenceCheckingIncompleteBecauseOfMeta

Added in version 2.7.0.

Incomplete confluence checks because of unsolved metas.

ConfluenceForCubicalNotSupported

Added in version 2.7.0.

Attempts to check confluence with --cubical.

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.

DivergentModalityInClause

Added in version 2.9.0.

Modalities of clauses that diverge from the modality of the function.

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.

DuplicateRewriteRule

Added in version 2.7.0.

Duplicate declaration of a name as REWRITE rule.

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.

EmptyRewritePragma

Added in version 2.5.2.

Empty REWRITE pragmas.

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.

FixingCohesion

Added in version 2.8.0.

Invalid cohesion annotations, automatically corrected.

FixingPolarity

Added in version 2.8.0.

Invalid polarity annotations, automatically corrected.

FixingRelevance

Added in version 2.8.0.

Invalid relevance annotations, automatically corrected.

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.

InvalidEtaEqualityPragma

Added in version 2.9.0.

ETA_EQUALITY pragmas before declarations other than 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.

LocalRewritingConfluenceCheck

Added in version 2.9.0.

Confluence checking (--confluence-check or --local-confluence-check) is not yet implemented for local rewrite rules (--local-rewriting).

MisplacedAttributes

Added in version 2.8.0.

Attributes where they cannot appear.

MisplacedRewrite

Added in version 2.9.0.

Invalid local rewrite annotations, automatically ignored.

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.

MultipleAttributes

Added in version 2.6.2.

Multiple attributes given where only erasure is accepted.

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.

NotARewriteRule

Added in version 2.8.0.

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

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.

PlentyInHardCompileTimeMode

Added in version 2.6.4.

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

PolarityPragmasButNotPostulates

Added in version 2.5.4.

Polarity pragmas for non-postulates.

PragmaCompileErased

Added in version 2.6.1.

COMPILE pragma targeting an erased symbol.

PragmaCompileList

Added in version 2.7.0.

COMPILE pragma for GHC backend targeting lists.

PragmaCompileMaybe

Added in version 2.7.0.

COMPILE pragma for GHC backend targeting MAYBE.

PragmaCompileUnparsable

Added in version 2.8.0.

Unparsable COMPILE GHC pragmas.

PragmaCompileWrong

Added in version 2.8.0.

Ill-formed COMPILE GHC pragmas.

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.

RewriteLHSNotDefinitionOrConstructor

Added in version 2.7.0.

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

RewriteVariablesNotBoundByLHS

Added in version 2.7.0.

Rewrite rule does not bind all of its variables.

RewriteVariablesBoundMoreThanOnce

Added in version 2.7.0.

Constructor-headed rewrite rule has non-linear parameters.

RewriteVariablesBoundInSingleton

Added in version 2.9.0.

Rewrite rule binds some variables in possibly definitionally singular contexts.

RewriteLHSReduces

Added in version 2.7.0.

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

RewriteHeadSymbolIsProjectionLikeFunction

Added in version 2.7.0.

Rewrite rule head symbol is a projection-like function.

RewriteHeadSymbolIsTypeConstructor

Added in version 2.7.0.

Rewrite rule head symbol is a type constructor.

RewriteHeadSymbolContainsMetas

Added in version 2.7.0.

Definition of rewrite rule head symbol contains unsolved metas.

RewriteConstructorParametersNotGeneral

Added in version 2.7.0.

Constructor-headed rewrite rule parameters are not fully general.

RewriteContainsUnsolvedMetaVariables

Added in version 2.7.0.

Rewrite rule contains unsolved metas.

RewriteBlockedOnProblems

Added in version 2.7.0.

Checking rewrite rule blocked by unsolved constraint.

RewriteRequiresDefinitions

Added in version 2.7.0.

Checking rewrite rule blocked by missing definition.

RewriteDoesNotTargetRewriteRelation

Added in version 2.7.0.

Rewrite rule does not target the rewrite relation.

RewriteBeforeFunctionDefinition

Added in version 2.7.0.

Rewrite rule is not yet defined.

RewriteBeforeMutualFunctionDefinition

Added in version 2.7.0.

Mutually declaration with the rewrite rule is not yet defined.

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

UnguardedEtaRecord

Added in version 2.9.0.

A record with eta-equality that Agda inferred as unguarded, meaning it has recursive occurences that are not protected by a type former that does not have eta equality (such as a data or a no-eta-equality record type).

UnknownAttribute

Added in version 2.8.0.

Unknown attributes.

UnknownFixityInMixfixDecl

Added in version 2.5.4.

Mixfix names without an associated fixity declaration.

UnknownJSPrimitive

Added in version 2.9.0.

A primitive compiled to Undefined by the JS backend because it is not in the list of known primitives.

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.

WithoutKFlagPrimEraseEquality

Added in version 2.6.0.

primEraseEquality used with the without-K flags.

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. --cubical into one which does not.

InferredLocalRewrite

Added in version 2.9.0.

Tried to solve a meta with an ‘@rewrite’ function.

InstanceNotInArgumentPosition

Added in version 2.8.0.

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

LocalRewriteOutsideTelescope

Added in version 2.9.0.

‘@rewrite’ arguments are (currently) only allowed in module telescopes.

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.

RewriteAmbiguousRules

Added in version 2.6.2.

Failed global confluence checks because of overlapping rules.

RewriteMaybeNonConfluent

Added in version 2.6.1.

Failed confluence checks while computing overlap.

RewriteMissingRule

Added in version 2.6.2.

Failed global confluence checks because of missing rules.

RewriteNonConfluent

Added in version 2.6.1.

Failed confluence checks while joining critical pairs.

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.

SafeFlagWithoutKFlagPrimEraseEquality

Added in version 2.6.0.

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

TerminationIssue

Added in version 2.5.2.

Failed termination checks.

TopLevelPolarity

Added in version 2.8.0.

Declaring definitions with an explicit polarity annotation.

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:

Furthermore, the Cubical options are jointly infective in the following sense: if one of them is used in one module, modules depending on it should use a Cubical option at least as strong as the imported module. The Cubical options are listed below in increasing strength:

* : Exceptionally, modules using Full Cubical --cubical[=full] can be imported from modules using Erased Cubical --cubical=erased if --erasure is enabled and imports are only used in erased positions. See here for a summary.

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:

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.