Command-line options

Command-line options

Agda accepts the following options.

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

--interactive, -I

Start in interactive mode (no longer supported).

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

--only-scope-checking

Only scope-check the top-level module, do not type-check it (see Quicker generation without typechecking).

--version, -V

Show version number.

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 module as the main module of a program when compiling.

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

Count extended grapheme clusters when generating LaTeX code (see Counting Extended Grapheme Clusters).

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

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

--html-highlight=[code,all,auto]

Whether to highlight non-Agda code as comments in generated HTML files (default: all; see Generating HTML).

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

--vim

Generate Vim highlighting files.

Imports and libraries

(see Library Management)

--ignore-all-interfaces

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.

--library={DIR}, -l={LIB}

Use library LIB.

--library-file={FILE}

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

Don’t use default library files.

--no-libraries

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.

Caching

--caching, --no-caching

Enable [disable] caching of typechecking (default).

Default: --caching

Printing and debugging

--no-unicode

Don’t use unicode characters to print terms.

--show-implicit

Show implicit arguments when printing.

--show-irrelevant

Show irrelevant arguments when printing.

--verbose={N}, -v={N}

Set verbosity level to N.

Copatterns and projections

--copatterns, --no-copatterns

Enable [disable] definitions by copattern matching (see Copatterns).

Default: --copatterns

--postfix-projections

Make postfix projection notation the default.

Experimental features

--confluence-check

New in version 2.6.1.

Enable optional confluence checking of REWRITE rules (see Confluence checking).

--cubical

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

--experimental-irrelevance

Enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching) (see Irrelevance).

--injective-type-constructors

Enable injective type constructors (makes Agda anti-classical and possibly inconsistent).

--rewriting

Enable declaration and use of REWRITE rules (see Rewriting).

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.

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

--exact-split, --no-exact-split

Require [do not require] all clauses in a definition to hold as definitional equalities unless marked CATCHALL (see Case trees).

Default: --no-exact-split

--no-eta-equality

Default records to no-eta-equality (see Eta-expansion).

--no-flat-split

New in version 2.6.1.

Disable pattern matching on @♭ arguments (see Pattern Matching on @♭).

--no-pattern-matching

Disable pattern matching completely.

--with-K

Overrides a global --without-K in a file (see Without K).

--without-K

Disables definitions using Streicher’s K axiom (see Without K).

--keep-pattern-variables

New in version 2.6.1.

Prevent interactive case splitting from replacing variables with dot patterns (see Dot patterns).

Search depth and instances

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

--termination-depth={N}

Allow termination checker to count decrease/increase upto N (default: 1; see Termination Checking).

--overlapping-instances, --no-overlapping-instances

Consider [do not consider] recursive instance arguments during pruning of instance candidates.

Default: --no-overlapping-instances

Other features

--double-check

Enable double-checking of all terms using the internal typechecker.

--guardedness, --no-guardedness

Enable [disable] constructor-based guarded corecursion (see Coinduction).

The option --guardedness is inconsistent with sized types and it is turned off by --safe (but can be turned on again, as long as not also --sized-types is on).

Default: --guardedness

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

--no-auto-inline

Disable automatic compile-time inlining. Only definitions marked INLINE will be inlined.

--no-fast-reduce

Disable reduction using the Agda Abstract Machine.

--no-forcing

Disable the forcing optimisation. Since Agda 2.6.1 is a pragma option.

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

--no-syntactic-equality

Disable the syntactic equality shortcut in the conversion checker.

--safe

Disable postulates, unsafe OPTIONS pragmas and primTrustMe. Turns off --sized-types and --guardedness (at most one can be turned back on again) (see Safe Agda).

--sized-types, --no-sized-types

Enable [disable] sized types (see Sized Types).

The option --sized-types is inconsistent with constructor-based guarded corecursion and it is turned off by --safe (but can be turned on again, as long as not also --guardedness is on).

Default: --sized-types

--type-in-type

Ignore universe levels (this makes Agda inconsistent; see type-in-type).

--omega-in-omega

Enable typing rule Setω : Setω (this makes Agda inconsistent; see omega-in-omega).

--universe-polymorphism, --no-universe-polymorphism

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. Implies –subtyping.

Default: --no-cumulativity

--subtyping, --no-subtyping

New in version 2.6.1.

Enable [disable] subtyping rules globally, including subtyping for irrelevance, erasure (@0) and flat (@♭) modalities.

Default: --no-subtyping

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.

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.

CantGeneralizeOverSorts

Attempt to generalize over sort metas in ‘variable’ declaration.

CoInfectiveImport

Importing a file not using e.g. --safe from one which does.

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.

EmptyPrimitive

Empty primitive blocks.

EmptyPrivate

Empty private blocks.

EmptyRewritePragma

Empty REWRITE pragmas.

IllformedAsClause

Illformed as-clauses in import statements.

InfectiveImport

Importing a file using e.g. :option;`–cubical` into one which doesn’t.

InstanceNoOutputTypeName

Instance arguments whose type does not end in a named or variable type are never considered by instance search.

InstanceArgWithExplicitArg

Instance arguments with explicit arguments are never considered by instance search.

InstanceWithExplicitArg

Instance declarations with explicit arguments are never considered by instance search.

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.

LibUnknownField

Unknown field in library file.

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.

PragmaCompiled

COMPILE pragmas not allowed in safe mode.

PragmaCompileErased

COMPILE pragma targeting an erased symbol.

PragmaNoTerminationCheck

NO_TERMINATION_CHECK pragmas are deprecated.

RewriteMaybeNonConfluent

Failed confluence checks while computing overlap.

RewriteNonConfluent

Failed confluence checks while joining critical pairs.

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.

ShadowingInTelescope

Repeated variable name in telescope.

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.

WithoutKFlagPrimEraseEquality

primEraseEquality used with the without-K flags.

WrongInstanceDeclaration

Terms marked as eligible for instance search should end with a name.

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:

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:

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: