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