		Search-engine friendly clone of the ACL2 documentation.

Definition

Compilation

Compilation of Leo.

We formalize the notion of correct compilation of Leo. In the current version of Leo, this involves relating three files (from the file system): the code file, the input file, and the output file. Each is represented as a finite sequence of Unicode characters, which is the content of each file after UTF-8 decoding.

Leo compilation produces the output file from the code and input files. There will be more files in future versions of Leo, but this is all that we capture for the current version. We capture that as a relation between the code, input, and output file.

The relation is that:

Code, input, and output files (i.e. lists of Unicode characters) are correctly lexed and parsed to CSTs.
Code, input, and output CSTs are correctly abstracted to ASTs.
Code, input, and output ASTs satisfy all their static semsantic requirements.
Executing the code AST on the input AST completes without error and returns a value; executing the output AST yields the same value.

This is an initial formalization of correct compilation. As the Leo langauge and its formalization are extended, we will extend the notion of correct compilation accordingly. In particular, at some point we may formulate it on a (suitably abstract) model of (a portion of) the file system; this will be importnt when a Leo program will consist of multiple files, and will also involve configuration files.

Subtopics

Compilep: Check correct compilation.