git.iko.soy/Idris-dev
on d8fd36a help sign in
Idris-dev/docs/reference/compilation.rst
115 lines 4.4 kB history raw
1***********************
2Compilation and Logging
3***********************
5This section provides information about the Idris compilation process, and
6provides details over how you can follow the process through logging.
8Compilation Process
9===================
11Idris follows the following compilation process:
13#. Parsing
14#. Type Checking
16 #. Elaboration
17 #. Coverage
18 #. Unification
19 #. Totality Checking
20 #. Erasure
22#. Code Generation
24 #. Defunctionalisation
25 #. Inlining
26 #. Resolving variables
27 #. Code Generation
30Type Checking Only
31==================
33With Idris you can ask it to terminate the compilation process after type checking has completed. This is achieved through use of either:
35+ The command line options
37 + ``--check`` for files
38 + ``--checkpkg`` for packages
40+ The REPL command: ``:check``
42Use of this option will still result in the generation of the Idris binary ``.ibc`` files, and is suitable if you do not wish to generate code from one of the supported backends.
44Logging Output
45==============
47The internal operation of Idris is captured using a category based logger.
48Currently, the logging infrastructure has support for the following categories:
50+ Parser
51+ Elaborator
52+ Code generation
53+ Erasure
54+ Coverage Checking
55+ IBC generation
58These categories are specified using the command-line option:
59``--logging-categories CATS``, where ``CATS`` is a quoted colon
60seperated string of the categories you want to see. By default if this
61option is not specified all categories are allowed. Sub-categories
62have yet to be defined but will be in the future, especially for the
63elaborator.
65Further, the verbosity of logging can be controlled by specifying a
66logging level between: 1 to 10 using the command-line option: ``--log
67<level>``.
69+ Level 0: Show no logging output. Default level
70+ Level 1: High level details of the compilation process.
71+ Level 2: Provides details of the coverage checking, and further details the elaboration process specifically: Interface, Clauses, Data, Term, and Types,
72+ Level 3: Provides details of compilation of the IRTS, erasure, parsing, case splitting, and further details elaboration of: Implementations, Providers, and Values.
73+ Level 4: Provides further details on: Erasure, Coverage Checking, Case splitting, and elaboration of clauses.
74+ Level 5: Provides details on the prover, and further details elaboration (adding declarations) and compilation of the IRTS.
75+ Level 6: Further details elaboration and coverage checking.
76+ Level 7:
77+ Level 8:
78+ Level 9:
79+ Level 10: Further details elaboration.
81Environment Variables
82=====================
84Several paths set by default within the Idris compiler can be
85overridden through environment variables. The provided variables are:
87* `IDRIS_CC` Change the `C` compiler used by the `C` backend.
88* `IDRIS_CFLAGS` Change the `C` flags passed to the `C` compiler.
89* `TARGET` Change the target directory i.e. `data dir` where Idris installs files when installing using Cabal/Stack.
90* `IDRIS_LIBRARY_PATH` Change the location of where installed packages are found/installed.
91* `IDRIS_DOC_PATH` Change the location of where generated idrisdoc for packages are installed.
93.. note::
95 In versions of Idris prior to 0.12.3 the environment variables
96 `IDRIS_LIBRARY_PATH` and `TARGET` were both used to affect the
97 installation of single packages and direct where Idris installed
98 its data. The meaning of these variables has changed, and command
99 line options are preferred when changing where individual packages
100 are installed.
102The CLI option `--ibcsubdir` can be used to direct where generated IBC
103files are placed. However, this means Idris will install files in a
104non-standard location separate from the rest of the installed
105packages. The CLI option `--idrispath <dir>` allows you to add a
106directory to the library search path; this option can be used multiple
107times and can be shortened to `-i <dir>`. Similary, the `--sourcepath
108<dir>` option can be used to add directories to the source search
109path. There is no shortened version for this option as `-s` is a
110reserved flag.
112Further, Idris also supports options to augment the paths used, and
113pass options to the code generator backend. The option `--cg-opt
114<ARG>` can be used to pass options to the code generator. The format
115of `<ARG>` is dependent on the selected backend.