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

--proof-irrelevance
Enable proof irrelevance (experimental feature)
--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=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

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

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)