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)
--cubical   Enable cubical features (see Cubical Type Theory in Agda)

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)