git.iko.soy/Idris-dev
on 751fb32 help sign in
Idris-dev/docs/reference/compilation.rst
106 lines 3.8 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: Class, Clauses, Data, Term, and Types,
72+ Level 3: Provides details of compilation of the IRTS, erasure, parsing, case splitting, and further details elaboration of: Instances, 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 to generate files.
90* `IDRIS_LIBRARY_PATH` Change the location of where installed packages are found.
92Alternativly, and perhaps a cleaner approach is to configure these
93options using the CLI options. Idris also supports options to augment
94the paths used, and pass options to the code generator backend.
96The option `--cg-opt <ARG>` can be used to pass options to the code
97generator. The format of `<ARG>` is dependent on the selected backend.
99Further, Idris does support multiple include paths. The CLI option
100`-i <dir>` allows you to add a directory to the search path; this
101option can be used multiple times. This is a cleaner option when you
102wish to add single directories to the `IDRIS_LIBRARY_PATH` than
103ammending `IDRIS_LIBRARY_PATH` directly.
105Moreover, rather than using `TARGET` the CLI option `--ibcsubdir` can
106be used to direct where built IBC files are placed.