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)
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
Sharing and caching¶
--sharing
- Enable sharing and call-by-need evaluation (experimental) (default: OFF)
--no-sharing
- Disable sharing and call-by-need evaluation
--caching
- Enable caching of typechecking (experimental) (default: OFF)
--no-caching
- Disable caching of typechecking
--only-scope-checking
- Only scope-check the top-level module, do not type-check it
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 andprimTrustMe
(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)
--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.
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
ormutual
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 flagSafeFlagPragma
- 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