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