我的书签
添加书签
移除书签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
New in version 2.6.1.
For use with other editors such as Atom (no need to invoke yourself).
--interaction-exit-on-error
New 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)]
New in version 2.6.4.
Configure printing of messages when an imported module is accessed during type-checking.
| Do not print any messages about checking a module. |
| Print only Checking … when an access to an uncompiled module occurs. This is the default behavior if —trace-imports is not specified. |
| 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. |
| 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)]
New 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 print diagnostic in colour. |
| 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 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
New 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-dir
New in version 2.6.2.
Outputs the root (AGDA_DIR) of the directory structure holding Agda’s data files such as core libraries, style files for the backends etc.
--transliterate
New 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
New 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
New 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
New 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}
New in version 2.3.0.
Generate a Dot file FILE with a module dependency graph.
--dependency-graph-include={LIBRARY}
New 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
New 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
New 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]
New in version 2.6.0.
Whether to highlight non-Agda code as comments in generated HTML files (default: all; see Generating HTML).
--latex
New in version 2.3.2.
Generate LaTeX with highlighted source code (see Generating LaTeX).
--latex-dir={DIR}
New 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
New 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}
New in version 2.5.1.
Use library LIB.
--library-file={FILE}
New in version 2.5.1.
Use FILE instead of the standard libraries file.
--local-interfaces
New in version 2.6.1.
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).
--no-default-libraries
New in version 2.5.1.
Don’t use default library files.
--no-libraries
New 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
New in version 2.6.2.
Turn on automatic compile-time inlining. See The INLINE and NOINLINE pragmas for more information.
--no-auto-inline
New 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
New in version 2.5.4.
Enable or disable caching of typechecking.
Default: --caching.
--call-by-name
New in version 2.6.2.
Disable call-by-need evaluation in the Agda Abstract Machine.
--no-call-by-name
New in version 2.6.4.
Default, opposite of --call-by-name.
--no-fast-reduce
New in version 2.6.0.
Disable reduction using the Agda Abstract Machine.
--fast-reduce
New in version 2.6.4.
Default, opposite of --no-fast-reduce.
--no-forcing
New in version 2.2.10.
Disable the forcing optimisation. Since Agda 2.6.1 it is a pragma option.
--forcing
New in version 2.6.4.
Default, opposite of --no-forcing.
--no-projection-like
New 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
New in version 2.6.4.
Default, opposite of --no-projection-like.
Printing and debugging
--no-unicode
New in version 2.5.4.
Do not use unicode characters to print terms.
--unicode
New in version 2.6.4.
Default, opposite of --no-unicode.
--show-identity-substitutions
New 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
New in version 2.6.4.
Default, opposite of --show-identity-substitutions.
--show-implicit
Show implicit arguments when printing.
--no-show-implicit
New in version 2.6.4.
Default, opposite of --show-implicit.
--show-irrelevant
New in version 2.3.2.
Show irrelevant arguments when printing.
--no-show-irrelevant
New in version 2.6.4.
Default, opposite of --show-irrelevant.
--verbose={N}, -v={N}
Set verbosity level to N.
--profile={PROF}
New in version 2.6.3.
Turn on profiling option PROF. Available options are
| Measure time taken by various parts of the system (type checking, serialization, etc) |
| Measure time spent on individual (Agda) modules |
| Measure time spent on individual (Agda) definitions |
| Measure things related to sharing |
| Collect detailed statistics about serialization |
| Collect statistics about constraint solving |
| Count number of created metavariables |
| Measure time of interactive commands |
| 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
New in version 2.4.0.
Enable or disable definitions by copattern matching (see Copatterns).
Default: --copatterns (since 2.4.2.4).
--postfix-projections
New in version 2.5.2.
Make postfix projection notation the default.
--no-postfix-projections
New in version 2.6.4.
Default, opposite of --postfix-projections.
Experimental features
--allow-exec
New in version 2.6.2.
Enable system calls during type checking (see Reflection).
--no-allow-exec
New in version 2.6.4.
Default, opposite of --allow-exec.
--confluence-check, —local-confluence-check, —no-confluence-check
New in version 2.6.1.
Enable optional (global or local) confluence checking of REWRITE rules (see Confluence checking).
Default is --no-confluence-check.
--cubical
New in version 2.6.0.
Enable cubical features. Turns on --cubical-compatible and --without-K (see Cubical).
--erased-cubical
New in version 2.6.3.
Enable a variant of Cubical Agda, and turn on --without-K.
--experimental-irrelevance
New in version 2.3.0.
Enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching) (see Irrelevance).
--no-experimental-irrelevance
New in version 2.6.4.
Default, opposite of --experimental-irrelevance.
--guarded
New in version 2.6.2.
Enable locks and ticks for guarded recursion (see Guarded Type Theory).
--no-guarded
New in version 2.6.4.
Default, opposite of --guarded.
--injective-type-constructors
New in version 2.2.8.
Enable injective type constructors (makes Agda anti-classical and possibly inconsistent).
--no-injective-type-constructors
New in version 2.6.4.
Default, opposite of --injective-type-constructors.
--irrelevant-projections, —no-irrelevant-projections
New 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
New in version 2.6.2.
Enable a constraint-solving heuristic akin to first-order unification, see Lossy Unification.
--no-lossy-unification
New in version 2.6.4.
Default, opposite of --lossy-unification.
--prop, —no-prop
New 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
New in version 2.4.2.4.
Enable declaration and use of REWRITE rules (see Rewriting).
--no-rewriting
New in version 2.6.4.
Default, opposite of --rewriting.
--two-level
New 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
New in version 2.6.4.
Default, opposite of --two-level.
Errors and warnings
--allow-incomplete-matches
New 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
New 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
New 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
New 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
New in version 2.6.4.
Default, opposite of --no-termination-check.
--warning={GROUP|FLAG}, -W {GROUP|FLAG}
New in version 2.5.3.
Set warning group or flag (see Warnings).
Pattern matching and equality
--exact-split, —no-exact-split
New 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
New in version 2.6.4.
Enable [disable] hidden argument puns.
Default: --no-hidden-argument-puns.
--no-eta-equality
New in version 2.5.1.
Default records to no-eta-equality (see Eta-expansion).
--eta-equality
New in version 2.6.4.
Default, opposite of --no-eta-equality.
--cohesion
New in version 2.6.3.
Enable the cohesion modalities, in particular @♭ (see Flat Modality).
--no-cohesion
New in version 2.6.4.
Default, opposite of --cohesion.
--flat-split
New in version 2.6.1.
Enable pattern matching on @♭ arguments (see Pattern Matching on @♭). Implies --cohesion.
--no-flat-split
New in version 2.6.4.
Default, opposite of --flat-split.
--no-pattern-matching
New in version 2.4.0.
Disable pattern matching completely.
--pattern-matching
New in version 2.6.4.
Default, opposite of --no-pattern-matching.
--with-K
New in version 2.4.2.
Overrides a global --without-K in a file (see Without K).
--without-K
New in version 2.2.10.
Disables reasoning principles incompatible with univalent type theory, most importantly Streicher’s K axiom (see Without K).
--cubical-compatible
New in version 2.6.3.
Generate internal support code necessary for use from Cubical Agda (see Cubical compatible). Implies --without-K.
--keep-pattern-variables
New in version 2.6.1.
Prevent interactive case splitting from replacing variables with dot patterns (see Dot patterns).
--no-keep-pattern-variables
New in version 2.6.4.
Default, opposite of --keep-pattern-variables.
--infer-absurd-clauses, —no-infer-absurd-clauses
New 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
New 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
New 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
New 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
New 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}
New 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
New in version 2.6.4.
Default, opposite of --type-in-type.
--omega-in-omega
New in version 2.6.0.
Enable typing rule Setω : Setω (this makes Agda inconsistent; see omega-in-omega).
--no-omega-in-omega
New in version 2.6.4.
Default, opposite of --omega-in-omega.
--level-universe, —no-level-universe
New 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
New in version 2.3.0.
Enable [disable] universe polymorphism (see Universe Levels).
Default: --universe-polymorphism.
--cumulativity, —no-cumulativity
New 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}
New in version 2.5.2.
Set instance search depth to N (default: 500; see Instance Arguments).
--inversion-max-depth={N}
New in version 2.5.4.
Set maximum depth for pattern match inversion to N (default: 50). Should only be needed in pathological cases.
--overlapping-instances, —no-overlapping-instances
New in version 2.6.0.
Consider [do not consider] recursive instance arguments during pruning of instance candidates.
Default: --no-overlapping-instances.
--qualified-instances, —no-qualified-instances
New 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
New in version 2.6.2.
Opposite of --double-check. On by default.
--keep-covering-clauses
New 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
New in version 2.6.4.
Opposite of --keep-covering-clauses, default.
--no-print-pattern-synonyms
New 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
New in version 2.6.4.
Default, opposite of --no-print-pattern-synonyms.
--no-syntactic-equality
New in version 2.6.0.
Disable the syntactic equality shortcut in the conversion checker.
--syntactic-equality={N}
New 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
New 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
New 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
New 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
New 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
New in version 2.6.4.
Default, opposite of --no-load-primitives.
--save-metas, —no-save-metas
New in version 2.6.3.
Save [or do not save] meta-variables in .agdai files. The alternative is to expand the meta-variables to their definitions. This option can affect performance. The default is to not save the meta-variables.
Erasure
--erasure, —no-erasure
New 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
New 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
New in version 2.6.3.
Mark parameters as erased in record module telescopes.
Implies --erasure.
--no-erase-record-parameters
New in version 2.6.4.
Default, opposite of --erase-record-parameters.
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.
AsPatternShadowsConstructorOrPatternSynonym
@-patterns that shadow constructors or pattern synonyms.
CantGeneralizeOverSorts
Attempts to generalize over sort metas in variable declaration.
ClashesViaRenaming
Clashes introduced by renaming.
CoverageNoExactSplit
Failed exact split checks.
DeprecationWarning
Deprecated features.
DuplicateFields
record expression with duplicate field names.
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 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.
InvalidConstructor
constructor blocks that contain declarations other type signatures for constructors.
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.
InvalidRecordDirective
Record directives outside of record definition or below field 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.
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.
OldBuiltin
Deprecated BUILTIN pragmas.
OpenPublicAbstract
open public directives in abstract blocks.
OpenPublicPrivate
open public directives 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.
PragmaNoTerminationCheck
NO_TERMINATION_CHECK pragmas; such are deprecated.
ShadowingInTelescope
Repeated variable name in telescope.
TooManyFields
Record expression with invalid field names.
UnfoldTransparentName
Non-opaque names mentioned in an unfolding 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.
UselessInline
INLINE pragmas where they have no effect.
UselessInstance
instance 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 blocks where they have no effect.
UserWarning
User-defined warnings added using one of the WARNING_ON_* pragmas.
WithoutKFlagPrimEraseEquality
primEraseEquality used with the without-K flags.
WrongInstanceDeclaration
Terms marked as eligible for instance search whose type does not end with a name.
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.
CoInfectiveImport
Importing a file not using e.g. --safe from one which does.
CoverageIssue
Failed coverage checks.
InfectiveImport
Importing a file using e.g. --cubical into one which does not.
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.
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.
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:
