git.iko.soy/Idris-dev
on d06ca16 help sign in
Idris-dev/docs/reference/compilation.rst
80 lines 2.6 kB history raw
1***********************
2Compilation and Logging
3***********************
6This section provides highlights of the Idris compilation process, and
7provides details over how you can follow the process through logging.
9Compilation Process
10===================
12Idris follows the following compilation process:
14#. Parsing
15#. Type Checking
17 #. Elaboration
18 #. Coverage
19 #. Unification
20 #. Totality Checking
21 #. Erasure
23#. Code Generation
25 #. Defunctionalisation
26 #. Inlining
27 #. Resolving variables
28 #. Code Generation
31Type Checking Only
32==================
34With Idris you can ask it to terminate the compilation process after type checking has completed. This is achieved through use of either:
36+ The command line options
38 + ``--check`` for files
39 + ``--checkpkg`` for packages
41+ The REPL command: ``:check``
43Use 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.
45Logging Output
46==============
48The internal operation of Idris is captured using a category based logger.
49Currently, the logging infrastructure has support for the following categories:
51+ Parser
52+ Elaborator
53+ Code generation
54+ Erasure
55+ Coverage Checking
56+ IBC generation
59These categories are specified using the command-line option:
60``--logging-categories CATS``, where ``CATS`` is a quoted colon
61seperated string of the categories you want to see. By default if this
62option is not specified all categories are allowed. Sub-categories
63have yet to be defined but will be in the future, especially for the
64elaborator.
66Further, the verbosity of logging can be controlled by specifying a
67logging level between: 1 to 10 using the command-line option: ``--log
68<level>``.
70+ Level 0: Show no logging output. Default level
71+ Level 1: High level details of the compilation process.
72+ Level 2: Provides details of the coverage checking, and further details the elaboration process specifically: Class, Clauses, Data, Term, and Types,
73+ Level 3: Provides details of compilation of the IRTS, erasure, parsing, case splitting, and further details elaboration of: Instances, Providers, and Values.
74+ Level 4: Provides further details on: Erasure, Coverage Checking, Case splitting, and elaboration of clauses.
75+ Level 5: Provides details on the prover, and further details elaboration (adding declarations) and compilation of the IRTS.
76+ Level 6: Further details elaboration and coverage checking.
77+ Level 7:
78+ Level 8:
79+ Level 9:
80+ Level 10: Further details elaboration.