Lean projects #
In general, if you just open a single .lean
file in your text editor
and try to compile it, you'll get a bunch of confusing errors.
Every non-trivial piece of Lean code needs to live inside a Lean project
(sometimes also called a Lean package).
A "Lean project" is more than just a folder that you've named "My Lean stuff".
Rather, it's a folder containing some very specific things:
in particular, a git repository and a file
lakefile.lean
that gathers information about dependencies of the
project, including for instance the version of Lean that should be used.
If you're interested in contributing to mathlib you only need to set up a Lean project once, which you can use for all your contributions — you don't need to set up a new Lean project for each new contribution.
Setting up and managing all this is done by a program called lake
(this is
a portmanteau of lean
and make
).
This page describes the basic use of this tool, and should be sufficient
for everyday use.
If this is not enough for your purposes, you can read the
full lake documentation.
Working on an existing project #
Suppose you want to work on an existing project. As example, we will take the Mathematics in Lean book. Open a terminal.
-
If you have not logged in since you installed Lean and mathlib, then you may need to first type
source ~/.profile
orsource ~/.bash_profile
depending on your OS. -
Go the the directory where you would like this package to live.
-
Run
git clone https://github.com/leanprover-community/mathematics_in_lean.git
. -
Run
cd mathematics_in_lean
-
Run
lake exe cache get
(note: this command currently only works in projects which importmathlib4
as a dependency) -
Launch VS Code, either through your application menu or by typing
code .
. (MacOS users need to take a one-off extra step to be able to launch VS Code from the command line.) -
If you launched VS Code from a menu, on the main screen, or in the File menu, click "Open folder" (just "Open" on a Mac), and choose the folder
mathematics_in_lean
(not one of its subfolders). -
Using the file explorer on the left-hand side, explore everything you want in
MIL
. See the MIL instructions for advice about how to do the exercises in this book.
Creating a Lean project #
We will now create a new project depending on mathlib. The following commands should be typed in a terminal.
-
Go to a folder where you want to create a project in a subfolder
my_project
, and typelake +leanprover/lean4:nightly-2023-02-04 new my_project math
. Do not worry about the date in the previous command, it ensures you will use a sufficiently recent version oflake
but has no impact on the version oflean
your project will use. If you get an error message sayinglake
is an unknown command and you have not logged in since you installed Lean, then you may need to first typesource ~/.profile
orsource ~/.bash_profile
. The keywordmath
at the end of this command addsmathlib4
to the dependencies of your project, so that you can useimport Mathlib
in your project files. -
Go inside the
my_project
folder and typelake update
, thenlake exe cache get
and thenmkdir MyProject
.- Some Windows users have reported an error like this when running
lake exe cache get
:If you see this error, you likely have an antivirus program that scans each downloaded file, which results in errors. Please disable your antivirus program and then runcurl: (35) schannel: next InitializeSecurityContext failed: Unknown error (0x80092012) - The revocation function was unable to check revocation for the certificate
lake exe cache get!
. The exclamation mark forceslake
to re-download the cache files it failed to download before running this command. (If you are uncomfortable disabling your antivirus, try to follow these instructions and then runlake exe cache get!
). You can turn on your antivirus program on afterwards. However, some users also reported that the antivirus programs significantly slow down Lean during normal usage. If Lean is slower than what is expected, either turn off your antivirus program or tell it to ignore/allow the operation oflean.exe
.
- Some Windows users have reported an error like this when running
-
Launch VS Code, either through your application menu or by typing
code .
. -
If you launched VS Code through a menu: on the main screen, or in the File menu, click "Open folder" (on a Mac, just "Open"), and choose the folder
my_project
(not one of its subfolders). -
Your Lean code should now be put inside files with extension
.lean
living inmy_project/MyProject/
or a subfolder thereof. In the file explorer on the left-hand side of VS Code, you can right-click onMyProject
, chooseNew file
, and type a filename to create a file there.
If you want to make sure everything is working, you can start by
creating, say my_project/MyProject/Test.lean
containing:
import Mathlib.Topology.Basic
#check TopologicalSpace
When the cursor is on the last line, the right hand part of VS Code
should display a "Lean Infoview" area saying:
TopologicalSpace.{u} (α : Type u) : Type u
.
Note that you can import your own files in the project. For instance if you created a
file my_project/MyProject/Definitions.lean
, you can start a new file
my_project/MyProject/Lemmas.lean
with import MyProject.Definitions
.
If, for some reason, you happen to lose the "Lean Infoview" area, you can get it back with Ctrl-Shift-Enter (Cmd-Shift-Enter on MacOS). Also, you can get the Lean documentation inside VS Code using Ctrl-Shift-p (Cmd-Shift-p on MacOS) and then, inside the text field that appears, type "lean doc" and hit Enter. Then click "Mathematics in Lean" or "Theorem Proving in Lean" and enjoy.
Hosting your project on GitHub #
Your project is already a git repository, and as it grows, you may want to host it on GitHub. If you take this step, the community offers some GitHub Actions scripts that could help manage your repository. But don't worry if you don't know what this means. It's not necessary for using Lean.