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.
General options¶
- --help[={TOPIC}], -?[{TOPIC}]¶
Show basically this help, or more help about
TOPIC
. Current topics available:warning
.
- --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 of1
, 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 of2
, 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 forstandard output to include colours. Colours will be usedwhen writing directly to a terminal device on Linux andmacOS.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).
- --version, -V¶
Show version number and cabal flags used in this build of Agda.
- --numeric-version¶
Show just the version number.
- --print-agda-app-dir¶
Added in version 2.6.4.1.
Outputs the (
AGDA_DIR
) directory containing Agda’s application configuration files, such as thedefaults
andlibraries
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.
While this location is usually determined at installation time, it can be controlled at runtime using the environment variable
Agda_datadir
.
- --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.
- --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 libraryL
ifL
is thename
of an.agda-lib
file associated toM
(even ifM
’s file cannot be found via theinclude
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
).
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 standardlibraries
file.
- --local-interfaces¶
Added in version 2.6.1.
Prefer to read and write interface files next to the Agda files they correspond to (i.e. do not attempt to regroup them in a
_build/
directory at the project’s root, except if they already exist there).
- --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 thedebug
flag.
- --profile={PROF}¶
Added in version 2.6.3.
Turn on profiling option
PROF
. Available options areinternal
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
, anddefinitions
can be turned on at a time. You can also give--profile=all
to turn on all profiling options (choosinginternal
overmodules
anddefinitions
, use--profile=modules --profile=all
to pickmodules
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).
- --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
).
- --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, bringsSSet
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
.
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 since 2.7.0:
--exact-split
.
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
.
- --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 universeLevelUniv
and disallows having levels depend on terms that are not levels themselves. When this option is turned off,LevelUniv
still exists, but reduces toSet
(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 alsoA : Set j
for allj >= 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.
- --backtracking-instance-search, --no-backtracking-instance-search¶
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
.
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 givenN
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, alsoProp
, and if--two-level
is active, evenSSet
.
- --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
:
- AbsurdPatternRequiresNoRHS¶
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.
- CoverageNoExactSplit¶
Failed exact split checks.
- DeprecationWarning¶
Deprecated features.
- DuplicateFields¶
record
expression with duplicate field names.
- DuplicateInterfaceFiles¶
There exists both a local interface file and an interface file in
_build
.
- DuplicateRecordDirective¶
Conflicting directives in a record declaration.
- 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.
- 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.
- FixityInRenamingModule¶
Fixity annotations in
renaming
directives for amodule
.
- HiddenGeneralize¶
Hidden identifiers in
variable
blocks.
- IllformedAsClause¶
Illformed
as
-clauses inimport
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.
- InvalidCharacterLiteral¶
Illegal character literals such as surrogate code points.
- InvalidConstructor¶
constructor
blocks that contain declarations other type signatures for constructors.
- InvalidConstructorBlock¶
constructor
blocks outside ofinterleaved mutual
blocks.
- InvalidCoverageCheckPragma¶
NON_COVERING pragmas before non-function or
mutual
blocks.
- InvalidNoPositivityCheckPragma¶
NO_POSITIVITY_CHECK pragmas before something that is neither a
data
norrecord
declaration nor amutual
block.
- InvalidNoUniverseCheckPragma¶
NO_UNIVERSE_CHECK pragmas before declarations other than
data
orrecord
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.
- MissingTypeSignatureForOpaque¶
abstract
oropaque
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.
- NoGuardednessFlag¶
Coinductive record but no
--guardedness
flag.
- NotAffectedByOpaque¶
Declarations that should not be inside
opaque
blocks.
- NotInScope¶
Out of scope names.
- OpenPublicAbstract¶
open public
directives inabstract
blocks.
- OpenPublicPrivate¶
open public
directives inprivate
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.
- PragmaNoTerminationCheck¶
NO_TERMINATION_CHECK pragmas; such are deprecated.
- 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.
- RewriteHeadSymbolIsProjection¶
Rewrite rule head symbol is a record projection.
- 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.
- ShadowingInTelescope¶
Repeated variable name in telescope.
- TooManyFields¶
Record expression with invalid field names.
- UnfoldTransparentName¶
Non-
opaque
names mentioned in anunfolding
clause.
- 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.
- UnreachableClauses¶
Unreachable function clauses.
- UnsupportedAttribute¶
Unsupported attributes.
- UnsupportedIndexedMatch¶
Failures to compute full equivalence when splitting on indexed family.
- UselessAbstract¶
abstract
blocks where they have no effect.
- UselessHiding¶
Names in
hiding
directive that are anyway not imported.
- 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.
- 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.
- 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 bothcoinductive
and havingeta-equality
.
- ConstructorDoesNotFitInData¶
Constructor with arguments in a universe higher than the one of its data type.
- CoverageIssue¶
Failed coverage checks.
- MissingDeclarations¶
Definitions not associated to a 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.
- 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.
- 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.
- SafeFlagTerminating¶
TERMINATING pragmas with the
--safe
flag.
- SafeFlagWithoutKFlagPrimEraseEquality¶
primEraseEquality
used with the--safe
and--without-K
flags.
- TerminationIssue¶
Failed termination checks.
- UnsolvedConstraints¶
Unsolved constraints.
- UnsolvedInteractionMetas¶
Unsolved interaction meta variables.
- UnsolvedMetaVariables¶
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 --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: