3.2. Compilation🔗

After elaboration, the document is compiled into an executable program. Each genre provides a main function that will carry out the remainder of the steps. Usually, this main function can be applied to the part that represents the whole document; however, genres that don't have a strict linear order (such as the website genre) will provide their own means of configuring the document's layout. The main function typically also takes configuration parameters both in the code and on the command line, such as which output formats to generate or customizations to the generated output. Each document should have a file that defines a main function for the document. The document's main should apply the genre's main to the document itself and supply any additional configuration that is needed.

While it works perfectly well to define an executable that runs the document's main function and run it with lake exe, it is typically faster to run the main function through the Lean interpreter instead. This avoids the overhead of compiling code that will only be discussed or displayed in a document, but not run. This is especially true for documents that import large non-executable libraries such as Mathlib. The best way to run the document's main function is to put it in a file (such as Main.lean) and then invoke lake run versoMain Main.lean in a shell.