4. The library🔗

In this chapter we are going to set everything up to be able to contribute to an existing Lean project. In particular, we are going to make a contribution to the Banach lattices library. Open the Banach lattices library GitHub repository and keep reading...

4.1. Welcome to GitHub!🔗

When you open the link above, you will see something like this:

GitHub repo

This is the GitHub repository containing the code of the Banach lattices library.

On the upper left, you can see that the owner of the repository is davidmunozlahoz: this is the GitHub account under which the original Banach lattices library lives. Later we will make our own copy of the same repository. The central part of the page shows the folders and files of the repository. You can click on them and inspect their contents directly in the browser. GitHub provides much more than this: tools to discuss changes, report problems, review code, automate tests, and so on. We do not need all of that, and certainly not now. We will introduce the features as we need them.

Below the list of files, GitHub shows the contents of the file README.md. This is a plain text file, written in a simple format called markdown, whose purpose is to present the repository: what the project is, how to install or use it, what its current state is, and anything else that visitors should know before using the code.

What is markdown?

Markdown is a very simple way of formatting plain text. The file is still just text: you can open it with any text editor and read it comfortably. The only trick is that some symbols have a special meaning. For instance, a line starting with # is a title, text between _ symbols is shown in italics, and text between backticks is shown as code.

For example, if you write # My title, GitHub will display it as a title. If you write _important_, GitHub will display the word in italics. If you write code between backticks, GitHub will display it with a code font. This is why markdown is convenient for files like README.md: it is easy to write, easy to read as plain text, and also looks nice when GitHub renders it in the browser.

Why all this trouble?

Why don't you just send the code by email, or provide a direct download link? If all we wanted was to read the code once, a download link would be enough. But software is rarely a fixed object. People change files, fix mistakes, add new pieces, remove old pieces, and try different approaches. If several people do this at the same time, it quickly becomes hard to know which version is the current one, who changed what, why something was changed, and whether two changes are compatible with each other. This is why all this infrastructure (and much more!) is needed. In fact, this is only the tip of the iceberg. We are about to explain how to use git, the version control system, because keeping track of changes and collaborating in a shared repository is far from trivial!

4.2. Fork🔗

To be able to contribute to the shared project, you first need your own fork of it.

Go to GitHub and use your email address to create an account (you can also sign up using your Google account).
Go back to the Banach lattices library, and click the Fork button. Leave the default options and click Create fork.

Thus we have a remote copy of the Banach lattices library, but not a local copy yet. To create and manage a local copy, we will need to use git. Before doing that, however, it is convenient to set up another little thing. If you now go ahead, copy the repository, make some changes, and try to upload them to GitHub, how do GitHub's servers know that the person trying to upload the changes is the same as the owner of the repository? They cannot know, unless you sign your changes, and then somehow make GitHub aware that the signature is actually yours. In the next section we set this up, once and for all, so that this signing process is done automatically every time we work on a project.

4.3. Connecting to GitHub with SSH🔗

In this section, we are going to connect to GitHub's servers using the SSH protocol. The official guide on how to do this can be found here.

We are going to create a public/private key pair. But before doing so, we need to check whether there is one already available. Open your terminal and run:
$
```
ls -al ~/.ssh
```
If you get an error saying that the directory does not exist, or the directory is empty, then you don't have an SSH key and you can go to step 3. If there is a file named id_rsa.pub, id_ecdsa.pub, or id_ed25519.pub, then you already have an SSH key and you can go to step 4.
Run the following command to generate a new SSH key (remember to replace the example email):
$
```
ssh-keygen -t ed25519 -C "your_email@example.com"
```
```
Generating public/private ed25519 key pair.
```
It will then prompt you for the file in which to save the key. Press Enter to use the default value. Finally, you will have to type a secure passphrase for the key (you can also leave it empty, but this is NOT a secure practice).
Start the SSH agent:
$
```
eval "$(ssh-agent -s)"
```
```
Agent pid 59566
```
Add the new private key to the SSH agent:
$
```
ssh-add ~/.ssh/id_ed25519
```
We have thus created our public/private key pair to communicate over the SSH protocol. Now it is time to let GitHub know our public key.
Run:
$
```
cat ~/.ssh/id_ed25519.pub
```
and copy the output (i.e., your public key).
Go to GitHub, click your profile picture in the upper-right corner, then click "Settings".
In the "Access" section of the sidebar, click "SSH and GPG keys".
Click "New SSH key" or "Add SSH key".
In the "Title" field, add a descriptive label for the new key. For example, if you are using a personal laptop, you might call this key "Personal laptop".
In the "Key" field, paste your public key. Click "Add SSH key".

Finally, we are going to test that you can indeed connect to GitHub's servers. Open your terminal and run:

ssh -T git@github.com

The authenticity of host 'github.com (IP ADDRESS)' can't be established.
 ED25519 key fingerprint is SHA256:+DiY3wvvV6TuJJhbpZisF/zLDA0zPMSvHdkr4UvCOqU.
 Are you sure you want to continue connecting (yes/no)?

Type yes, and we are done.

4.4. git enters the scene🔗

In simple terms, git is the command-line tool we use to manage the changes we make to a repository. It is already installed on your system, because it is a dependency of Lean (i.e., Lean needs it to work). We are going to use git to create a local copy of the Banach lattices library and set it up so that this copy is aware of your Banach lattices library fork, and also of the original Banach lattices library repository.

First of all, open the terminal. You can either open your system terminal, as we did in tasting the terminal, or open a terminal inside VS Code (go to Terminal > New Terminal); do whatever feels more natural to you.
Navigate, using cd, to the folder where you want to create a copy of the repository (mind you: when copying the repository, git will create its own folder, called banlat).
Run:
$
```
git clone git@github.com:your-username/banlat.git
```
where you have to replace your-username with your GitHub username. Now you have a local copy of the repository in the folder banlat.

What does git clone do?

git clone means: take this repository from GitHub and make a local copy on my computer. The address after it is the repository we want to copy; here it is your fork. Git also remembers that address under the name origin, so later it knows where to send your changes.
Now we are going to make this new repository aware of the original banlat repository. In order to do this, first run cd banlat to go to the repository, and then run:
$
```
git remote add upstream git@github.com:davidmunozlahoz/banlat.git
```
What does the previous command mean?

A remote is a repository that lives somewhere else, usually on GitHub. Your local repository already knows your fork as a remote called origin. The previous command adds another remote, called upstream, pointing to the original Banach lattices repository. From now on, when we say upstream, git knows that we mean git@github.com:davidmunozlahoz/banlat.git.
Run the following:
$
```
git fetch upstream
git branch --set-upstream-to=upstream/master master
```
You should have some faith and skip the explanation of these commands for now.

Explanation of the previous commands

The first command asks git to contact upstream and download its current state. This does not change your files; it only updates git's information about what exists in the original repository.

After that, upstream/master means: "the master branch as it exists in the original repository". The second command tells git that your local master branch should follow that branch. In practice, this means that later, if you run git pull from master, git knows that it should pull changes from the original Banach lattices repository, not from your fork. If you don't know yet what branches are, then you should not be reading this yet.
Same as above:
$
```
git config push.default current
git config push.autoSetupRemote true
```
Explanation of the previous commands

These two commands configure what happens when you upload changes with git push. The first one says that, when you push from a branch, git should push to a branch with the same name. The second one says that, the first time you push a new branch, git should automatically remember where that branch lives on GitHub. This saves us from having to type a longer command the first time we upload a new branch.

Congratulations! Now you have a local copy of the Banach lattices library, and you have everything configured to start making contributions. But before that, maybe we should do a quick tour of what's inside the library, so that you can navigate the folder more comfortably.

4.5. A quick tour of the library🔗

If you list the contents of the folder banlat using ls (or just open the folder in VS Code with File > Open folder...), you should see something like this:

ls

BanLat  AGENTS.md  BanLat.lean lakefile.toml  lake-manifest.json  lean-toolchain  README.md STYLE.md

Let me briefly explain what these files and folders are:

BanLat: This is the main folder, containing all the Lean code. We will explore it further below.
BanLat.lean: The main Lean file of the project, importing all the files inside the BanLat folder. When you create a new file inside BanLat, you have to import it in BanLat.lean for it to be compiled.
lakefile.toml, lake-manifest.json, and lean-toolchain: These files describe how the Lean project is built. The file lean-toolchain says which version of Lean should be used. lakefile.toml is the configuration file for Lake, the build tool used by Lean projects: it says what the project is called, what it depends on, and what should be built. Finally, lake-manifest.json records the exact versions of the dependencies.
README.md: We already covered this in the first section of this chapter.
AGENTS.md and STYLE.md: These are LLM-related files; we will cover them in the next chapter, when we set up our LLM assistant.

To prevent our computer from taking several hours to compile the whole mathlib, run in your terminal:

lake exe cache get

Then build the project with:

lake build

What does it mean to build the project?

Building a Lean project means asking Lake, Lean's build tool, to check the project from the files declared in lakefile.toml. Lake follows the imports, runs Lean on the necessary files, and makes sure that all definitions, statements, and proofs are accepted.

When Lean checks a file successfully, it produces compiled files, especially .olean files. These files store the checked information from the source file in a form that Lean can load quickly later. This is why a project does not have to re-check every imported file from plain text every time.

The command lake exe cache get downloads precompiled files for dependencies such as mathlib, when they are available. This matters because mathlib is huge: compiling it locally from scratch can take a very long time. The cache lets us reuse compiled versions that were already produced elsewhere.

After that, lake build builds our actual project. If something is wrong, for example, a proof does not typecheck or an imported file cannot be found, lake build will report an error.

If you have the banlat folder already open in VS Code (if not, open it using File > Open folder...), expand the BanLat subfolder. There you will see a bunch of Lean files and further folders (with more and more subfolders and Lean files). Let's click, for instance, on Basic.lean. Wait for the Lean language server to start. When it starts, a Lean InfoView window will open, and you will see something like this:

VS Code Lean file

Navigate the Lean file. You will see how the information in the InfoView window changes, showing what we have in context.

VS Code Lean file infoview

We would now like to contribute to this project. However... we don't know how to write Lean code yet! In fact, we won't need to write almost any Lean, we will just need to read it. The writing will be done by our gracious LLM assistant. It is time to set it up.