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)

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

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)
--guardedness-preserving-type-constructors: Treat type constructors as inductive constructors when checking productivity
--experimental-irrelevance: Enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching) (see Irrelevance)
--rewriting: Enable declaration and use of REWRITE rules (see Rewriting)

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¶

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

Other features¶

--safe: Disable postulates, unsafe OPTION pragmas and primTrustMe (see Safe Agda)
--type-in-type: Ignore universe levels (this makes Agda inconsistent; see Universe Levels)
--sized-types: Use sized types (default, inconsistent with “musical” coinduction; see Sized Types)
--no-sized-types: Disable sized types (see Sized Types)
--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)

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:

OverlappingTokensWarning: Multi-line comments spanning one or more literate text blocks.
UnknownNamesInFixityDecl: Names not declared in the same scope as their syntax or fixity declaration.
UnknownFixityInMixfixDecl: Mixfix names without an associated fixity declaration.
UnknownNamesInPolarityPragmas: Names not declared in the same scope as their polarity pragmas.
PolarityPragmasButNotPostulates: Polarity pragmas for non-postulates.
UselessPrivate: private blocks where they have no effect.
UselessAbstract: abstract blocks where they have no effect.
UselessInstance: instance blocks where they have no effect.
EmptyMutual: Empty mutual blocks.
EmptyAbstract: Empty abstract blocks.
EmptyPrivate: Empty private blocks.
EmptyInstance: Empty instance blocks.
EmptyMacro: Empty macro blocks.
EmptyPostulate: Empty postulate blocks.
InvalidTerminationCheckPragma: Termination checking pragmas before non-function or mutual blocks.
InvalidNoPositivityCheckPragma: No positivity checking pragmas before non-data`, record or mutual blocks.
InvalidCatchallPragma: CATCHALL pragmas before a non-function clause.
OldBuiltin: Deprecated BUILTIN pragmas.
EmptyRewritePragma: Empty REWRITE pragmas.
UselessPublic: public blocks where they have no effect.
UnreachableClauses: Unreachable function clauses.
UselessInline: INLINE pragmas where they have no effect.
DeprecationWarning: Feature deprecation.
InversionDepthReached: Inversions of pattern-matching failed due to exhausted inversion depth.
TerminationIssue: Failed termination checks.
CoverageIssue: Failed coverage checks.
CoverageNoExactSplit: Failed exact split checks.
NotStrictlyPositive: Failed strict positivity checks.
UnsolvedMetaVariables: Unsolved meta variables.
UnsolvedInteractionMetas: Unsolved interaction meta variables.
UnsolvedConstraints: Unsolved constraints.
SafeFlagPostulate: postulate blocks with the safe flag
SafeFlagPragma: Unsafe OPTIONS pragmas with the safe flag.
SafeFlagNonTerminating: NON_TERMINATING pragmas with the safe flag.
SafeFlagTerminating: TERMINATING pragmas with the safe flag.
SafeFlagPrimTrustMe: primTrustMe usages with the safe flag.
SafeFlagNoPositivityCheck: NO_POSITIVITY_CHECK pragmas with the safe flag.
SafeFlagPolarity: POLARITY pragmas with the safe flag.

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

Command-line options¶