Command-line options

Command-line options

Agda accepts the following options.

General options

--version -V
Show version number
--help[=TOPIC] -?[TOPIC]
Show basically this help, or more help about TOPIC. Current topics available: warning.
--interactive -I
Start in interactive mode (no longer supported)
--interaction
For use with the Emacs mode (no need to invoke yourself)
--interaction-json
For use with other editors such as Atom (no need to invoke yourself)
--only-scope-checking
Only scope-check the top-level module, do not type-check it

Compilation

See Compilers for backend-specific options.

--no-main
Do not treat the requested module as the main module of a program when compiling
--compile-dir=DIR
Set DIR as directory for compiler output (default: the project root)
--no-forcing
Disable the forcing optimisation

Generating highlighted source code

--vim
Generate Vim highlighting files
--latex
Generate LaTeX with highlighted source code (see Generating LaTeX)
--latex-dir=DIR
Set directory in which LaTeX files are placed to DIR (default: latex)
--count-clusters
Count extended grapheme clusters when generating LaTeX code (see Counting Extended Grapheme Clusters)
--html
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)
--css=URL
Set URL of the CSS file used by the HTML files to URL (can be relative)
--html-highlight=[code,all,auto]
Whether to highlight non-Agda code as comments in generated HTML files (default: all; see :ref: generating-html)
--dependency-graph=FILE
Generate a Dot file FILE with a module dependency graph

Imports and libraries

(see Library Management)

--ignore-interfaces
Ignore interface files (re-type check everything, except for builtin and primitive modules)
--ignore-all-interfaces
Ignore all interface files, including builtin and primitive modules; only use this if you know what you are doing!
--include-path=DIR -i=DIR
Look for imports in DIR
--library=DIR -l=LIB
Use library LIB
--library-file=FILE
Use FILE instead of the standard libraries file
--no-libraries
Don’t use any library files
--no-default-libraries
Don’t use default library files

Command-line and pragma options

The following options can also be given in .agda files in the {-# OPTIONS --{opt₁} --{opt₂} ... #-} form at the top of the file.

Caching

--caching
Enable caching of typechecking (default)
--no-caching
Disable caching of typechecking

Printing and debugging

--show-implicit
Show implicit arguments when printing
--show-irrelevant
Show irrelevant arguments when printing
--no-unicode
Don’t use unicode characters to print terms
--verbose=N -v=N
Set verbosity level to N

Copatterns and projections

--copatterns
Enable definitions by copattern matching (default; see Copatterns)
--no-copatterns
Disable definitions by copattern matching
--postfix-projections
Make postfix projection notation the default

Experimental features

--injective-type-constructors
Enable injective type constructors (makes Agda anti-classical and possibly inconsistent)
--experimental-irrelevance
Enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching) (see Irrelevance)
--rewriting
Enable declaration and use of REWRITE rules (see Rewriting)
--cubical
Enable cubical features. Turns on --without-K (see Cubical)

Errors and warnings

--allow-unsolved-metas
Succeed and create interface file regardless of unsolved meta variables (see Metavariables)
--no-positivity-check
Do not warn about not strictly positive data types (see Positivity Checking)
--no-termination-check
Do not warn about possibly nonterminating code (see Termination Checking)
--warning=GROUP|FLAG -W=GROUP|FLAG
Set warning group or flag (see Warnings)

Pattern matching and equality

--without-K
Disables definitions using Streicher’s K axiom (see Without K)
--with-K
Overrides a global --without-K in a file (see Without K)
--no-pattern-matching
Disable pattern matching completely
--exact-split
Require all clauses in a definition to hold as definitional equalities unless marked CATCHALL (see Case trees)
--no-exact-split
Do not require all clauses in a definition to hold as definitional equalities (default)
--no-eta-equality
Default records to no-eta-equality (see Eta-expansion)

Search depth and instances

--termination-depth=N
Allow termination checker to count decrease/increase upto N (default: 1; see Termination Checking)
--instance-search-depth=N
Set instance search depth to N (default: 500; see Instance Arguments)
--inversion-max-depth=N
Set maximum depth for pattern match inversion to N (default: 50). Should only be needed in pathological cases.
--no-overlapping-instances
Don’t consider recursive instance arguments during pruning of instance candidates (default)
--overlapping-instances
Consider recursive instance arguments during pruning of instance candidates

Other features

--safe
Disable postulates, unsafe OPTION pragmas and primTrustMe. Turns off --sized-types and --guardedness (at most one can be turned back on again) (see Safe Agda)
--type-in-type
Ignore universe levels (this makes Agda inconsistent; see Universe Levels)
--omega-in-omega
Enable typing rule Setω : Setω (this makes Agda inconsistent).
--sized-types
Enable sized types (default, inconsistent with constructor-based guarded corecursion; see Sized Types). Turned off by --safe (but can be turned on again, as long as not also --guardedness is on).
--no-sized-types
Disable sized types (see Sized Types)
--guardedness
Enable constructor-based guarded corecursion (default, inconsistent with sized types; see Coinduction). Turned off by --safe (but can be turned on again, as long as not also --sized-types is on).
--no-guardedness
Disable constructor-based guarded corecursion (see Coinduction)
--universe-polymorphism
Enable universe polymorphism (default; see Universe Levels)
--no-universe-polymorphism
Disable universe polymorphism (see Universe Levels)
--no-irrelevant-projections
Disable projection of irrelevant record fields (see Irrelevance)
--no-auto-inline
Disable automatic compile-time inlining. Only definitions marked INLINE will be inlined.
--no-print-pattern-synonyms
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.
--double-check
Enable double-checking of all terms using the internal typechecker
--no-syntactic-equality
Disable the syntactic equality shortcut in the conversion checker
--no-fast-reduce
Disable reduction using the Agda Abstract Machine

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

Individual warnings can be turned on and off by -W {Name} and -W {noName} respectively. The flags available are:

AbsurdPatternRequiresNoRHS
RHS given despite an absurd pattern in the LHS.
CoverageIssue
Failed coverage checks.
CoverageNoExactSplit
Failed exact split checks.
DeprecationWarning
Feature deprecation.
EmptyAbstract
Empty abstract blocks.
EmptyInstance
Empty instance blocks.
EmptyMacro
Empty macro blocks.
EmptyMutual
Empty mutual blocks.
EmptyPostulate
Empty postulate blocks.
EmptyPrivate
Empty private blocks.
EmptyRewritePragma
Empty REWRITE pragmas.
InvalidCatchallPragma
CATCHALL pragmas before a non-function clause.
InvalidNoPositivityCheckPragma
No positivity checking pragmas before non-data`, record or mutual blocks.
InvalidTerminationCheckPragma
Termination checking pragmas before non-function or mutual blocks.
InversionDepthReached
Inversions of pattern-matching failed due to exhausted inversion depth.
MissingDefinitions
Names declared without an accompanying definition.
ModuleDoesntExport
Names mentioned in an import statement which are not exported by the module in question.
NotAllowedInMutual
Declarations not allowed in a mutual block.
NotStrictlyPositive
Failed strict positivity checks.
OldBuiltin
Deprecated BUILTIN pragmas.
OverlappingTokensWarning
Multi-line comments spanning one or more literate text blocks.
PolarityPragmasButNotPostulates
Polarity pragmas for non-postulates.
SafeFlagNoPositivityCheck
NO_POSITIVITY_CHECK pragmas with the safe flag.
SafeFlagNonTerminating
NON_TERMINATING 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.
SafeFlagPrimTrustMe
primTrustMe usages with the safe flag.
SafeFlagTerminating
TERMINATING pragmas with the safe flag.
TerminationIssue
Failed termination checks.
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.
UnsolvedConstraints
Unsolved constraints.
UnsolvedInteractionMetas
Unsolved interaction meta variables.
UnsolvedMetaVariables
Unsolved meta variables.
UselessAbstract
abstract blocks where they have no effect.
UselessInline
INLINE pragmas where they have no effect.
UselessInstance
instance blocks where they have no effect.
UselessPrivate
private blocks where they have no effect.
UselessPublic
public blocks where they have no effect.

For example, the following command runs Agda with all warnings enabled, except for warnings about empty abstract blocks:

agda -W all --warning noEmptyAbstract file.agda

Consistency checking of options used

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:

  • --cubical
  • --prop

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

  • --safe
  • --without-K
  • --no-universe-polymorphism
  • --no-sized-types
  • --no-guardedness

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:

  • --termination-depth
  • --no-unicode
  • --allow-unsolved-metas
  • --no-positivity-check
  • --no-termination-check
  • --type-in-type
  • --omega-in-omega
  • --no-sized-types
  • --no-guardedness
  • --injective-type-constructors
  • --prop
  • --no-universe-polymorphism
  • --irrelevant-projections
  • --experimental-irrelevance
  • --without-K
  • --exact-split
  • --no-eta-equality
  • --rewriting
  • --cubical
  • --overlapping-instances
  • --safe
  • --double-check
  • --no-syntactic-equality
  • --no-auto-inline
  • --no-fast-reduce
  • --instance-search-depth
  • --inversion-max-depth
  • --warning