Command-line options

Command-line options

Agda accepts the following options.

General options

--version -V
Show version number
--help -?
Show basically this help
--interactive -I
Start in interactive mode (no longer supported)
For use with the Emacs mode (no need to invoke yourself)


See Compilers for backend-specific options.

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

Generating highlighted source code

Generate Vim highlighting files
Generate LaTeX with highlighted source code (see Generating LaTeX)
Set directory in which LaTeX files are placed to DIR (default: latex)
Count extended grapheme clusters when generating LaTeX code (see Counting Extended Grapheme Clusters)
Generate HTML files with highlighted source code (see Generating HTML)
Set directory in which HTML files are placed to DIR (default: html)
Set URL of the CSS file used by the HTML files to URL (can be relative)
Generate a Dot file FILE with a module dependency graph

Imports and libraries

(see Library Management)

Ignore interface files (re-type check everything)
--include-path=DIR -i=DIR
Look for imports in DIR
--library=DIR -l=LIB
Use library LIB
Use FILE instead of the standard libraries file
Don’t use any library files
Don’t use default library files

Sharing and caching

Enable sharing and call-by-need evaluation (experimental) (default: OFF)
Disable sharing and call-by-need evaluation
Enable caching of typechecking (experimental) (default: OFF)
Disable caching of typechecking
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 arguments when printing
Show irrelevant arguments when printing
Don’t use unicode characters to print terms
--verbose=N -v=N
Set verbosity level to N

Copatterns and projections

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

Experimental features

Enable proof irrelevance (experimental feature)
Enable injective type constructors (makes Agda anti-classical and possibly inconsistent)
Treat type constructors as inductive constructors when checking productivity
Enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching) (see Irrelevance)
Enable declaration and use of REWRITE rules (see Rewriting)

Errors and warnings

Succeed and create interface file regardless of unsolved meta variables (see Metavariables)
Do not warn about not strictly positive data types (see Positivity Checking)
Do not warn about possibly nonterminating code (see Termination Checking)
--warning=MODE -W=MODE
Set warning mode to MODE (available: warn display warnings, error turn warnings into errors, and ignore ignore warnings)

Pattern matching and equality

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

Search depth

Allow termination checker to count decrease/increase upto N (default: 1; see Termination Checking)
Set instance search depth to N (default: 500; see Instance Arguments)

Other features

Disable postulates, unsafe OPTION pragmas and primTrustMe (see Safe Agda)
Ignore universe levels (this makes Agda inconsistent; see Universe Levels)
Use sized types (default, inconsistent with “musical” coinduction; see Sized Types)
Disable sized types (see Sized Types)
Enable universe polymorphism (default; see Universe Levels)
Disable universe polymorphism (see Universe Levels)
Disable projection of irrelevant record fields (see Irrelevance)