@@ -0,0 +1,56 @@
1+***********************
2+Compilation and Logging
3+***********************
4+
5+
6+This section provides highlights of the Idris compilation process, and
7+provides details over how you can follow the process through logging.
8+
9+Compilation Process
10+===================
11+
12+Idris follows the following compilation process:
13+
14+1. Parsing
15+2. Type Checking
16+ 1. Elaboration
17+ 2. Coverage
18+ 2. Unification
19+ 1. Totality Checking
20+ 1. Erasure
21+3. Code Generation
22+ 1. Defunctionalisation
23+ 1. Inlining
24+ 1. Resolving variables
25+ 2. Code Generation
26+
27+
28+Type Checking Only
29+==================
30+
31+With Idris you can ask it to terminate the compilation process after type checking has completed. This is achieved through use of either:
32+
33++ The command line options
34+ + ``--check`` for files
35+ + ``--checkpkg`` for packages
36++ The REPL command: ``:check``
37+
38+Use 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.
39+
40+Logging Output
41+==============
42+
43+Logging of the Idris output can be used to diagnose problems with the compilation of your program.
44+Idris supports the logging at various different levels of verbosity: 1 to 10.
45+
46++ Level 0: Show no logging output. Default level
47++ Level 1: High level details of the compilation process.
48++ Level 2: Provides details of the coverage checking, and further details the elaboration process specifically: Class, Clauses, Data, Term, and Types,
49++ Level 3: Provides details of compilation of the IRTS, erasue, parsing, case splitting, and further details elaboration of: Instances, Providers, and Values.
50++ Level 4: Provides further details on: Erasure, Coverage Checking, Case splitting, and elaboration of clauses.
51++ Level 5: Provides details on the prover, and further details elaboration (adding declarations) and compilation of the IRTS.
52++ Level 6: Further details elaboration and coverage checking.
53++ Level 7:
54++ Level 8:
55++ Level 9:
56++ Level 10: Further details elaboration.