7. How to contribute🔗

Finally, we have reached the point where all the setup is done. All that we did in the previous chapters only had to be done once, and we are done. I know, it was a long journey, but I hope you learned something in the process. Now I will show you the workflow you will have to follow to make contributions to the library. It may look cumbersome at first, but you will get used to it. The goal of this workflow is to collaborate effectively and without making each other's lives miserable. As always, I will explain the reason and goal of every single command. Instead of trying to memorize the commands (there is no point in doing that), try to follow the big picture of the workflow. You will realize that it makes a lot of sense, and you will not forget it.

7.1. git branches🔗

It would be a mess if everyone that passed by could make changes to the library freely without someone in charge supervising. To make sure that all the new content that is added to the library has the necessary quality and is correct (i.e., Lean still compiles after the change), we have to use git branches.

What is a git commit and a git branch?

Git does not remember the history of a project as a vague continuous thing. It remembers it in discrete steps. The basic unit of this history is called a commit. A commit is a saved snapshot of the repository at a given moment. When we make a commit, git records the contents of the files we want to save, together with a short message explaining what changed, together with some metadata such as the author and a timestamp. This is useful because git can later tell us exactly what changed between two commits, and we can always go back and inspect an older state of the project.

A branch is a separate line of commits. The repository has a main line of work, called master in our case. If we want to add something new, we create a branch starting from the current state of master and make our commits there. This lets us work freely without changing the main version of the library until the changes have been reviewed and accepted. The auxiliary branch, or branches, are eventually merged into master, meaning that the changes of the branch are incorporated into the main branch, resolving any conflicts if necessary.

git branch

What really is a git commit and a git branch?

Internally, git stores the history of a repository as a graph of objects. The contents of a file are stored in a blob. A directory is stored in a tree: it records the names of the files and folders inside it, and points to the corresponding blobs and smaller trees. Thus, one tree can describe the full state of all the files in the repository at a given moment.

A commit is another object. It points to one tree, which is the snapshot of the repository saved by that commit. It also stores some metadata, such as the author, the commit message, and, most importantly, the previous commit or commits. This is how git knows the history: each commit points backwards to its parent. Every object has a hash, computed from its contents, and this hash is the name git uses to identify it.

A branch is not a copy of the files. It is just a name pointing to one commit. When we make a new commit on a branch, git creates the commit and moves the branch name forward so that it points to the new commit. This is why branches are cheap and fast: creating a branch does not duplicate the project, it only creates a new movable pointer into the graph of commits.

There is one more important pointer, called HEAD. This is git's name for "where we currently are". Most of the time, HEAD points to the current branch; for example, if we are working on master, then HEAD points to master, and master points to the latest commit on that branch. When we create a commit, the branch moves forward, and HEAD keeps following it. In some situations HEAD can point directly to a commit instead of to a branch; this is called a detached HEAD. It is useful for inspecting old commits, but it is not the normal state in which we want to do our work.

Git commands are sometimes divided into plumbing and porcelain. Plumbing commands are the low-level commands that manipulate or inspect the object database more directly: blobs, trees, commits, references, and hashes. Porcelain commands are the friendly commands we normally use, such as git status, git add, git commit, git switch, git pull, and git push. They are built on top of the plumbing, and they are the ones we will use all the time in this guide. The point of this technical digression is not that you should start using plumbing commands, but that the porcelain commands make more sense once you know what is underneath. You can learn more about this in the Pro Git book.

The idea is the following: we will check first that our fork of the library is up to date with the original one, then we will create a branch in our fork, make our changes, and finally ask the maintainers of the main library to incorporate the changes of our branch into the main repository. Let's do it.

First things first: open the terminal and navigate to the banlat folder. Remember that you can also use the terminal inside VS Code (if you have the banlat folder open in VS Code, the terminal it spawns will already be inside that folder).
Run
$
```
git switch master
```
to make sure you are in the master branch.

git switch

git switch moves us from one branch to another. Here we use it to go back to master, which is the main branch of this repository: the branch whose contents should agree with the official version of the library.
Run
$
```
git pull
```
git pull

git pull updates the current branch with the changes that have appeared in the remote repository since the last time we updated it. In our case, because master was configured to follow upstream/master, this asks git to look at the original banlat repository, download the new commits from its master branch, and apply them to our local master branch.

If your local repository is up to date with davidmunozlahoz/banlat, you will see a message saying so. Otherwise, it will apply the new changes from the repository, and you will see something similar to this:

Now the state of our local repository is exactly the same as that of davidmunozlahoz/banlat.
Create a new branch, with a descriptive name of the additions or changes to be made to the library. In this particular example, we are going to add the definition and very basic properties of order convergence. You don't need to know what this means: it is just an example. For this reason, we call the new branch basic-order-conv and create it with
$
```
git switch -c basic-order-conv
```
```
Switched to new branch 'basic-order-conv'
```
The -c flag means: create a new branch with this name, and switch to it immediately. As explained by the output, we are now in the branch basic-order-conv.

7.2. Making our changes🔗

We can now safely write our own Lean code. In this particular case, just as an example, I am going to ask Codex to create a new file Convergences/Order.lean with the definition of order convergence and some very basic properties. I will do this in state mode using the following prompt:

Enter state mode. Create a file @Convergence/Order.lean with the
definition of order convergence (the general one, in which the
regulating net need not have the same index set as the original
net), then state that an increasing supremum is a particular case of order
convergence, and that the linear and lattice operations are order
continuous.

After thinking for a while, Codex has proposed a patch with the definitions and facts I asked for.

Codex proposed patch

After carefully reviewing the patch, I have approved it and Codex has created the file you can see below.

Order convergence file

This file compiles modulo sorries, meaning that the statements and definitions compile, but there are no proofs (they are replaced by sorries). Now it is time to start a new conversation with Codex and ask it to enter prove mode and fill in the sorries in the file:

Enter prove mode and fill in the sorries in @Convergences/Order.lean

Why start a new conversation?

Codex does not only see your last message. It also sees a certain amount of the previous conversation, which is called the context. This is useful, because it lets Codex remember what you have been doing. But it can also become a problem: old instructions, failed attempts, long explanations, and unrelated details may still influence what Codex does next.

Here we are changing tasks. First we asked Codex to state definitions and theorems modulo sorry; now we want it to prove the existing statements without changing their meaning. Starting a new conversation keeps the context clean: the new conversation contains the precise file and the precise task, and not the whole history of how the file was created. This is much cheaper (in terms of tokens), and more efficient.

Naming conventions

Lean names are case-sensitive, and mathlib follows fairly stable naming conventions. Files and folders usually start with capital letters, as in Convergences/Order.lean. This file can then be imported through its module name, for instance BanLat.Convergences.Order.

Inside the files, types, structures, classes, and namespaces usually start with capital letters: for example OrderConvergesTo. Ordinary definitions usually start with a lowercase letter and use camel case, as in orderConvergesTo. Theorems and lemmas usually have lowercase descriptive names, often with words separated by underscores, such as map_add, sup_le_iff, or orderConvergesTo_of_monotone_isLUB.

You don't need to memorize all of this. The practical rule is: look at nearby files and at mathlib, and imitate the local style. Good names are not only cosmetic; they make it much easier for other people, and for Codex, to find and reuse the results later.

After a while, and if they are within reach (i.e., the adequate infrastructure is already available), Codex will have filled in the proofs, creating auxiliary lemmas when needed.

Codex proof conversation

7.3. Saving our changes🔗

We have thus contributed to the library! We now have to "save" these changes (that is, commit them), and then upload them, first to our own fork of banlat, and then to the original one. In the terminal you have open, run

git status

to see what files have been modified since the last commit (remember: a commit is nothing more than a snapshot of the current state of the repository).

We are going to create a new commit with the changes we have made. To add files to be committed, use git add. For instance, to add the file BanLat.lean, run git add BanLat.lean, as I did below. You can see that now the file has a new status, and appears under "Changes to be committed:"

git status after staging

This is useful if you only want to add certain files to the next commit. If you want to add all the modified files, just run:

git add .

These files are now staged and ready to be committed.

We can now commit our changes. Each commit has a message (that should consist of no more than one line) describing the changes made. In my case, the commit looks something like this:

git commit -m "feat: add order convergence definition and order continuity of operations"

feat?

The feat: at the beginning is a commit message convention. It says that this commit adds a new feature. Other common prefixes are fix: for bug fixes, doc: for documentation, style: for formatting, refactor: for reorganizing code without changing its meaning, and chore: for maintenance.

The Lean community uses conventions of this kind for mathlib: a title has the shape <type>(<optional-scope>): <subject>, where the scope can name the file or directory affected by the change. The subject should be short, lowercase, in the imperative present tense, and without a final period. For example, feat: add order convergence or doc(Convergences): fix typo in order convergence docstring.

We do not need to be strict about this, but it is a good habit. A clean commit message makes the history easier to scan, and makes reviewing the contribution easier. You can find the full mathlib conventions here: mathlib commit conventions.

The changes are now committed; it is time to

git push

We can now go to our repository on GitHub, click on the branches button (the button where it says master by default and there is an arrow to expand it), and see our branch there.

GitHub branch selector

Click on that branch. The repository will show the new commit we made, and the changes it incorporates.

7.4. Pull requesting🔗

The moment of truth has come. We want to add the changes of this branch to the main banlat library. For this we have to do a pull request.

In order to do this, click on the "Contribute" button that GitHub shows in a banner, then click on "Open pull request".

GitHub open pull request prompt

Write a clear title, and description if needed, so as to make the life of the maintainer of the library (i.e., me) easy.

Pull request conventions

The title of the pull request should usually have the same shape as a good commit message:

<type>(<optional-scope>): <subject>

For instance, in our example we could write feat(Convergences): add order convergence. The type says what kind of change this is: feat for a new feature, fix for a correction, doc for documentation, refactor for reorganizing code, and so on. The optional scope says where the change lives, and the subject says what the pull request does. As with commit messages, keep the subject short, lowercase, in the imperative present tense, and without a final period.

The description should explain the motivation and the contents of the change. It does not need to be long, but it should give the maintainer enough context to review the pull request without guessing.

The full mathlib conventions are explained here. We do not have to be strict, but the closer we are to these conventions, the easier the review process becomes.

GitHub pull request form

Your pull request is created now. In order for your commits to be incorporated into the main repository, this pull request has to be merged. Before that, the maintainer may send you messages asking for clarifications or corrections. You can interact with the maintainer using the conversation window in the pull request. Once the pull request has been merged:

Merged pull request

You can now safely delete the branch from your repository doing

git switch master
git branch -d basic-order-conv

And get everything up to date with

git pull
git push

We are done! Your contribution is now accessible to everyone through the banlat library!