-
Notifications
You must be signed in to change notification settings - Fork 89
Getting started with contributing
This page explains how to get started committing to the Metamath "set.mm" set of axioms, definitions, and theorems, also known as the Metamath Proof Explorer (MPE).
This page is a little long, but it provides step-by-step instructions and should be easy to follow. If you have any questions at all, please contact the Metamath mailing list - we'd love to help!! There have now been at least 48 contributors to "set.mm", so it really is doable; we even have a Gource visualization of Metamath set.mm contributors over time which shows that people really have been contributing.
To learn how to achieve the recommended formatting for set.mm and iset.mm prior to submitting your changes, see the CONTRIBUTING.md page.
This page is primarily intended for those who have never used GitHub and git. You might want to go through these first steps to learn how a simple contribution to Metamath Proof Explorer can be made. You will find many more details in GitHub's "help" documentation.
If you are already acquainted with git and GitHub procedures, which are extremely popular, this page is possibly not for you. In that case, see contributing for experts.
In good, ol' times you simply downloaded a file, modified it, and then put it somehow back again as a contribution. Guess what! It is not that simple any more. Collaboration of dozens of contributors across all continents in a timely fashion make repository/version management tools like git indispensable. GitHub is a widely-used web-based service that makes it easy to share data managed by git.
This tutorial will show you the bare steps necessary to perform a simple get-modify-put cycle under this environment, starting from scratch. This is enough for occasional contributions, one-time fixes, and other small bandwidth actions. Once you have successfully contributed, you might want to learn how to act more efficiently, but that is beyond the scope of this article.
You will need:
- An e-mail address;
- An internet connection with a download volume of ca. 150MB (perhaps 1 GB or more if you download everything);
- An operating system;
- (Possibly) An administrative account to install new software;
- A usual internet browser installed;
- 200MB of free hard disk storage (1+ GB to download everything);
- Roughly 10 minutes of time (roughly 2 hours of time if you download everything). The download of the repository will hopefully go unattended, but your internet connection may be blocked for some time.
These instructions focus on POSIX-like operating systems including Linux, macOS, FreeBSD, and Cygwin (on Windows). Native Windows works but isn't fully covered here (you can replace "&&" with pressing "Enter" to implement many of these steps).
Understanding a few key terms will make it much easier to work with others using git and GitHub. These terms are repository, fork, branch, git, and GitHub.
The files processed by Metamath are organized in a directory. But unlike a common directory, a git repository also contains history information about how the files developed into their current state. Moreover, a file may exist in parallel in several versions, for example, in the original state, and one being modified under work. All this extra information accumulates to possibly hundreds of megabytes. We will later go and download a repository for set.mm, so be prepared to set aside sufficient resources to do so.
The original files normally processed by Metamath, such as set.mm, cannot be modified by normal contributors. This set of "original" files is called "origin" here. In a development environment your modifications could too easily overwrite meanwhile contributions of others and vice versa. Instead you work on a snapshot of the Metamath files copied for your own purposes. This creates an independent fork of Metamath usually named after you. Note that this fork can go out of sync to its original, if either you modify your fork, or the origin is modified by others. The process of syncing is called "merging" in git lingo. Updating the "origin" with your contributions is done in a final step via a "pull request". You ask a maintainer of the project to merge the origin with your modified fork. You are not entitled to do it right away, and the maintainer may reject your request, or postpone its application to a later time.
Development is carried out in parallel branches in Metamath. The branch named master is the stable one undergoing changes infrequently only. Most likely you want to contribute to develop, which is the tip of development and updated very often. Your fork contains all branches present in the origin.
The open source program "git" manages a downloaded repository. On your file system a repository appears as a simple directory. The file contents are initially those of the latest version; but you can order git to show an older state, or the modified version of another contributor instead.
In order to contribute, you must have git installed. If it is not already available, in many Linux distributions you need administrative rights to add it.
GitHub, Inc. is a web-based service, hosting repositories of many open-source projects, among them Metamath. You must be registered with GitHub as a user to use their services. Strictly speaking, you need the account only to enable contributing to a repository.
There are several steps for setting up git and GitHub.
On a terminal/console issue the command
git versionIf you receive an answer like this
git version 2.7.4
you can go on with step 1c.
You need to install git. Follow the instructions of your Linux distribution. On Debian based distributions
sudo apt install gitwill usually do. This is where you need your administrative rights.
If you haven't set up git before, you should set up your name and email address. Do this with the following commands (replace "John Doe" with your real name, and the email address with your real email address):
git config --global user.name "John Doe"
git config --global user.email "[email protected]"Open the page Home page of set.mm in a different browser tab than this page, so that you can easily switch between this tutorial and web pages described herein.
If you find your personal icon on the top right corner of the page, and a click on it reveals your user name, you are already signed in and can continue with step 3.
Otherwise, if you already have a GitHub account, sign in using your credentials. Else
Click on Sign up to create a new account and follow the steps. You need to enter an email address somewhere. This address is not only used during account registration, but later in communication with others commenting on your contributions, and in notifications such as a maintainer accepting your pull request.
We already stated it before: you cannot modify the origin directly; this is left to assigned maintainers. Instead, a snapshot of the current state is taken and your personal repository is created by clicking on the Fork button on the top.
Note that from now on your fork and the origin may diverge because contributions of others to the origin are not automatically transferred to your fork.
Your work on the Metamath files is carried out off line on your computer, not on web pages and the like. So you need to copy the repository from GitHub to your computer. If you download the entire history the repository is quite big, but even a "shallow" copy can be over 100MB, so make sure you have enough disk space and download volume left.
Clicking on the green 'Clone or Download' button shows a text field filled with an URL like this:
https://github.com/YOUR_ACCOUNT_NAME/set.mm.git
We will use this URL and the 'git clone' command to download the repository. You probably want to have the repository in a specific location.
Whenever you want to manage your local copy of the repository you need to cd into its directory.
So, first cd to where you want it to be:
cd HIGHER_DIRECTORYThe next step will create a set.mm subdirectory inside HIGHER_DIRECTORY.
Open a terminal and issue the following command, directory and URL properly replaced (the URL will look like https://github.com/YOUR_ACCOUNT_NAME/set.mm.git):
git clone --depth 10 --no-single-branch URL.From.AboveThe options listed here make it faster and take less space by omitting a lot of history. Here are the specifics. The --depth 10 command tells git that you only want the history of the 10 most recent changes, aka a "shallow clone". In a shallow clone you can't see older repository history on your computer, but it's much faster to download and takes much less space. The --no-single-branch option works with depth so that you get a shallow clone (history) of all the branches in the repository, not just one.
Omit --depth 10 if you want the entire history on your local computer. If you download the entire history (and that's great!) the download may take some time. Get yourself a cup of coffee. You can always download the full entire history later if you want it (using git fetch --unshallow).
If github hangs up during the cloning, you can try to extend your "post buffer":
git config --global http.postBuffer 100000000and relaunch the git clone … command.
Eventually, you end up with a subdirectory (by default set.mm) which contains various files and history.
Whenever you want to work with the repository, you need to "cd" into its directory by typing
cd set.mmIssue the following command:
git remote -vThe answer should look like
origin https://github.com/YOUR_ACCOUNT_NAME/set.mm.git (fetch)
origin https://github.com/YOUR_ACCOUNT_NAME/set.mm.git (push)
(with "set.mm" replaced by the name of your fork if you renamed it).
So far, you have downloaded your forked repository. But you need a link to the origin as well, so that you can easily refresh your fork with any updates applied to the origin after fork. The following command prepares this step (assuming you're already in the set.mm directory):
git remote add upstream https://github.com/metamath/set.mm.gitNow, the command git remote -v should output something like
origin https://github.com/YOUR_ACCOUNT_NAME/set.mm.git (fetch)
origin https://github.com/YOUR_ACCOUNT_NAME/set.mm.git (push)
upstream https://github.com/metamath/set.mm.git (fetch)
upstream https://github.com/metamath/set.mm.git (push)
Now that you've set things up, there are a few steps to apply every time you want to contribute.
First, you need to cd (change directory) so that your current directory is the repository
if you aren't already there. If you just completed the previous step then you
don't need to do this.
For example:
cd set.mmYou can base your modifications on any version of the software. Usually you'd make a change based on the develop branch. That's the default in set.mm today, but it's probably wise to make sure that you're starting with the develop branch, so do this:
git checkout developIf you're already on the develop branch it will say Already on 'develop' and that's fine.
Pull the latest information from upstream (if you just cloned the data, this won't do much, but this ensures you're starting from current information):
git pull upstream developNow switch to a new branch for your work (change YOUR_BRANCH_NAME to a simple name without a space that suggests what you're doing):
git checkout -b YOUR_BRANCH_NAMEThis step comprises all your modifications to the files in the downloaded repository on your computer. Obviously, here you are on your own.
Typically proofs are created using mmj2 or metamath.exe, with some other edits being directly
using a text editor on set.mm.
Try to follow our usual conventions.
Some actions (use or change) are specifically discouraged. In particular, some axioms and theorems are marked as "(New usage is discouraged.)".
Normally you won't want to do anything discouraged. If you insist on doing something discouraged, and it's rare for this to be needed, then you need to regenerated the "discouraged" list. Here's how to do this on POSIX systems:
./metamath 'read set.mm' 'set width 9999' 'show discouraged' quit | grep '^SHOW DISCOURAGED.' | \
sed -E -e 's/^SHOW DISCOURAGED. ?//' | LC_ALL=C sort > discouragedBe prepared for additional scrutiny if you're doing something discouraged!
Now you can commit your work. You need to be in your local repository (e.g., cd set.mm). This is done by:
git commit -am 'Short description of what you have done.'If you've made a commit and have not published it publicly (using "git push" as described below), you can locally update your commit. Just make further changes and use the "amend" option of git commit:
git commit --amend -am 'Short description of what you have done.'It's best if you make smaller incremental changes and then contribute them back to set.mm. Then you don't need to deal with conflicts between your changes and others' changes.
However, if a considerable time passed has passed since you forked from the origin and you created your commit, many other contributions may have been applied to it, and your fork might not be up-to-date any more. If those other contributions conflict with your changes, then you'll need to resolve those conflicts. If that's your circumstance, here's how to proceed.
You need to be in your local repository directory (e.g., cd set.mm). The following command first fetches the modifications on origin:
git fetch --depth 10 upstreamand this command applies them to your local repository (replace develop with a different branch if you want to base off some other branch):
git merge upstream/developThe outcome is hopefully a success, but you may encounter occasionally a merge conflict. This happens if someone else has changed lines close to your modifications. In this case you have to go back to step 5b, and compare your lines to those in origin. The relevant locations have been marked with sequences of >>>>>>> and <<<<<<<<<<. Resolve the conflicts as needed and then create another git commit as described above.
So far you have worked on your local repository on your computer; we now need to make those changes visible to the rest of the world. Again, you need to be in the repository directory (cd set.mm). Transfer it back to your fork on GitHub:
git push --set-upstream originBe prepared to enter your GitHub account credentials on authorization request.
Your changes are visible; if you want those changes incorporated, you need to create a "pull request" (also called "merge request").
Open the page Home page of set.mm in a different browser tab than this page, so that you can easily switch between this tutorial and web pages described herein.
Login to your GitHub account and click on Fork. This will not create a new fork, but get you to your existing one.
Select the modified branch from the drop down menu and click on New pull request and fill out the form.
NOTE: Be sure to create a pull request to merge to upstream's develop, not to master. In general, you want to contribute to the upstream develop branch.
After you've published your branch with changes, and you want to make further changes in that branch (e.g., due to comments), you follow a shortened version of the process you've already done.
Switch to the branch with your changes:
git checkout YOUR_BRANCH_NAMENow make the changes.
Once you're done, create a commit as usual:
git commit -am 'short description'Then publish:
git pushOn undoing, fixing, or removing commits in git provides a step-by-step guide to fixing various problems.