-
Notifications
You must be signed in to change notification settings - Fork 91
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 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 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.
On a terminal/console issue the command
git version
If 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-get install git
will 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:
`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_DIRECTORY
The next step will create a "set.mm" subdirectory inside HIGHER_DIRECTORY.
Open a terminal and issue the following command, directory and URL properly replaced
git clone --depth 5 --no-single-branch URL.From.Above
The "--depth 5" command tells git that you only want the history of the 5 most recent changes. aka a "shallow clone". In a shallow clone you can't see older history in the repository on your computer, but it's fast to download and takes relatively little space.
Omit "--depth 5" if you want the entire history. 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).
This will create 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. E.g.:
cd set.mm
Issue the following command (replaced "set.mm" if you used renamed your fork):
git remote -v
The 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)
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.git
Whenever you want to work with the repository, you need to "cd" into its directory. E.g.:
cd set.mm
Most likely you want to make a change based on the "develop" branch, and then create a new branch that represents your new contribution.
Now check out your starting point, and 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 develop && git checkout -b YOUR_BRANCH_NAME
This step comprises all your modifications to the files in the downloaded repository on your computer. Obviously, here you are on your own.
Now that you have finished your work, it is time to make it permanent to your local repository. Before, remove all freshly created temporary and back up files from the directory.
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'
There might have been a considerable time passed since you forked from the origin. Meanwhile other contributions may have been applied to it, so your fork is not up-to-date any more. 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 5 upstream
and 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/develop
The 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 proceed with step 5c.
So far you have worked on your local repository on your computer. Again, you need to be in the repository directory (cd set.mm). Transfer it back to your fork on Github:
git push --set-upstream origin
Be prepared to enter your GitHub account credentials on authorization 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.