The Anatomy of a Lean Project
In this section, we will discuss the basic structure of a Lean project, and that of a Lean file.
Lean Projects
A Lean project is a collection of Lean files which are all located in the same directory. It must contain a few special files, including:
- A
lakefile.leanfile. - A
lean-toolchainfile.
The lakefile.lean file is used to manage the Lean project, declaring dependencies, specifying how to build the project, etc. The lean-toolchain file is used to specify the version of Lean that the project uses; this file is used by the elan tool to determine which version of Lean to use when building the project. We will see explicit examples of such files during lecture.
To create a bare bones Lean project, you can run the following commands in a terminal:
lake new my_project
This will create a new Lean project called my_project in the current directory, with the necessary files (as well as some others). In this case, this is a bare project meant to eventually compile a Lean executable. To create a “library” project, you can use lake new foo lib and to create one which has mathlib as a dependency use lake new foo math.
Mathlib
We should spend a few minutes talking about mathlib, which is the main library of formalized mathematics written in Lean. It is maintained and developed by the Lean community, and has over 300 contributors and over 1 million lines of code. It is still growing rapidly. Here is a link to the GitHub repository.
It is important to note that mathlib takes a very long time to compile, and that it must be compiled in order to be used (see the discussion about imports below). You definitely do not want to spend time compiling mathlib on your own machine. Instead, you can download a precompiled cache for the version of mathlib that you are using. This is done using lake, with the command lake exe cache get. Again, we will see examples during lecture. Note that after updating mathlib in a project, the cache must be updated as well.
Lake
Let me also say a few additional words about lake, which is the build system used by Lean projects: lake = lean + make. It is a tool which is used to manage Lean projects, and is used to compile Lean files. It is also used to manage dependencies, and to download precompiled caches of Lean projects.
To build a project, you use lake build in the root directory of the project (the same location which contains the lakefile.lean of your project). The lakefile can also specify lake executables which can be run with lake exe ... (cache is such an executable which is part of mathlib itself). This tool has various other capabilities as well, and we will discuss them as necessary.
Opening a project
When working with a Lean project in an editor (such as VScode) it is crucial that you open the project’s root directory (the one containing the lakefile). DO NOT OPEN A SINGLE LEAN FILE ON ITS OWN.
The Anatomy of a Lean File
Let’s take a closer look at what goes on in an individual lean file.
Copyright and comments
At the top of the file we usually have a copyright notice as a multiline comment. This looks like this:
/-
Copyright (c) 2023 Joe Shmoe. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joe Shmoe, Jane Doe
-/
Note that multiline comments in Lean are delimited by /- and -/, while single line comments are delimited by --:
/-
A multiline comment.
Another line.
-/
-- A single line comment.
There are two other kinds of comment blocks which we will discuss later.
Imports
Right after the copyright notice, we have a collection of import commands. For example:
import Mathlib.Data.Nat.Basic
import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
import Lean.Data.Json.Parser
These import commands are used to import Lean files from other Lean projects, or other files from within the current project.
After the imports, we have the main body of the file, which contains definitions, theorems, etc.
Docstrings
As mentioned above, there are two additional kinds of comment blocks in Lean. They are delimited by /-! and -/, and /-- and -/. The first one, /-! ... -/ is commonly used for the module docstring. This comment block accepts markdown, and is used to describe the contents of the file. It usually comes right after the imports, and looks like this:
/-!
# Markdown Title
Markdown text.
## Subheading
Etc.
-/
The other kind of comment block, /-- ... -/ is used for docstrings for definitions, theorems, etc. For example:
/-- The meaning of life. -/
def theMeaningOfLife : Nat := 42
We use these two kinds of comment blocks to generate documentation for our code. You can find the automatically generated documentation for mathlib at this link.
What happens in a Lean File?
Let’s take a closer look at what happens in an actual lean file. When we open a lean file in an editor like VSCode, a language server is spawned which lets us interact with the code in the given file in real time (this assumes that the Lean4 package has been properly installed). At the top (after a copyright header) we have the imports of the file. The server then uses these imports to obtain an Environment, which contains all the information (definitions, lemmas, etc.) from the imports.
We can interact with this environment explicitly using metaprogramming. I will demonstrate this in class.
After the import portion of the file, we start writing commands. At the end of the day, these commands all define terms which have some names, and which are added to the environment in question. After each command, the environment could be different!
But what actually happens when Lean (or the Lean Language Server) processes a file? Well, first it looks at the imports and obtains an initial environment (along with messages, etc.). It does this by first parsing the import lines, and using a precompiled version of the files in question. If there is no precompiled version, then it compiles the imports (which amounts to recursively doing what I describe below).
Next, it parses the actual code into Syntax objects. Here Syntax is a built-in type in Lean that we can work with as a first-class citizen in the language. This is a formal representation of the code itself that Lean can work with.
After that, there is a macro expansion step. In Lean4, we can write macros that convert Syntax into Syntax. Custom notation is an example of a macro.
After that comes the main step, which is called “elaboration.” In this step, Lean tried to fill in missing information, such as implicit variables, typeclass parameters, etc. It also does some “unification,” checking that certain things are definitionally equal. This step also converts tactics into actual terms – you can think of tactics as scripts that instruct Lean in constructing actual terms. It also tries to detect and report all possible errors. At the end of this step, the Syntax objects mentioned above are converted into “fully elaborated terms” which are elements of an expression type called Expr. Again, this is a built-in Lean type that can be handled as a first-class citizen.
From here, the fully elaborated terms of Expr are passed to the kernel of the language for typechecking. The kernel is actually responsible for checking that definitions and proofs are correct.
The Lean kernel is purposefully kept as small as possible, so that it is easier to verify the correctness of the program. On the other hand, the elaboration process is much more complex, and may have bugs. It does happen (infrequently) that a fully elaborated term is passed to the kernel, only to be rejected. This indicates that there is a bug in some elaborator which should be fixed.
We wont’t have to worry about all these internals for this course. However, if you plan to do any metaprogramming in Lean (and I recommend that you do), such as writing custom tactics, etc., then understanding the internals is quite important.
Commands
Here is a description of the main commands in Lean4 (others exist and we will encounter them as we go along with the course).
def
The def command is used to define terms. For example:
def foo : Nat := 42
This defines a term called foo of type Nat with value 42, and adds it to the environment.
theorem / lemma
The theorem and lemma commands are used to prove theorems (which means providing terms of propositions). For example:
theorem foo : 1 + 1 = 2 := by
rfl
This defines a term called foo of type 1 + 1 = 2, and adds it to the environment. Mathematically, think of foo as the name of the proof that 1 + 1 = 2.
We can actually use def to define theorems as well, but it is better to use theorem or lemma for this purpose, for various reasons which we don’t need to go into right now.
example
The example command is used to provide examples of terms. It can be used for terms of any type or proposition. The difference between example and theorem/lemma is that example does not add the term to the environment, and thus example doesn’t require a name for the term.
For example:
example : 1 + 1 = 2 := by
rfl
#check
We have already encountered the #check command during lecture. It is used to check the type of a term. For example:
#check 1 + 1
#check 1 + 1 = 2
#check Nat
This doesn’t do anything to the environment.
#eval
The #eval command is used to evaluate a term. For example:
#eval 1 + 1
def foo : Nat := 42
#eval foo
This doesn’t do anything to the environment.
#print
The #print command is used to print the definition of a term. For example:
def foo : Nat := 42
#print foo
This doesn’t do anything to the environment.
#reduce
The #reduce command is used to reduce a term to normal form. For example:
def foo : Nat := 42
#reduce foo + 1
This doesn’t do anything to the environment.
The difference between #eval and #reduce is that #eval will evaluate a term to a value (i.e. it will run the code), while #reduce will only reduce it to normal form.
Here is an example where they have different behaviour:
#eval show IO Unit from IO.println "hello world"
#reduce show IO Unit from IO.println "hello world"
#help
The #help command is used to get help about various things. It’s quite intuitive, just write #help and follow the instructions. For example, to get help about tactics you can use
#help tactic
#help tactic intro
The Infoview
The infoview is a panel in VSCode which displays information about the current Lean file. It should show up automatically when you open a Lean file. We use the infoview to keep track of the context (i.e. the local variables) and the current goal (i.e. the proposition that we are trying to prove). It also displays messages, including error messages, etc.
Goals
Whenever there is some piece of information that Lean cannot infer automatically, it will display it as a goal. Each goal has an associated context, which may include variables that have been introduced, typeclass assertions, etc.
The infoview displays a goal and its associted local context as follows:
n : Nat
h : n = 0
⊢ n = 0
The stuff before ⊢ is the context, and the stuff after ⊢ is the goal. Here the context says: we have a natural number n and a proof/term h for n = 0. And our goal is to provide a proof/term for n = 0.