Git
Overview
We use the Git version control system with github.com to manage submissions and grade assignments.
Setup
If you don’t already have a GitHub account, sign up first!
Once you have a GitHub account, set up Git on your computer by following this guide. Be sure to select your operating system at the top of that guide. Also open the Input
informational box for information on how to use git from the command-line, because we will be using that in this guide.
We will explain the steps needed to work on and submit assignments in this guide. To learn the basics of git, read git - the simple guide and try out the Git command-line. If you’d like to learn more, have a look at these resources.
Repository Structure
Let’s look at the repository structure first.
On GitHub, we will create a private git repository for you, which is owned by us, and is only visible to you and the compiler construction team. This repository will host assignment templates and your submissions. Note that you do not have write access to this repository, you can only read from it and submit assignments to it. This is to ensure that you cannot mess with submitted assignments after the deadline.
You create your own private Git repository by making a fork of our private repository. This repository will be used by you to work on assignments. You have write access to this repository since you create it. Our repository on GitHub is called upstream in git terms, because your repository is a fork of it. Your repository on GitHub is called origin. If you’d like to learn more about forking, read this GitHub guide.
Getting started
First, find your private repository in the TUDelft-IN4303-2015 organization on GitHub, it should be called student-id
where id
is your student id. Remember your id, as it is used later. Go to the repository and press the fork button to fork the repository into your account.
To actually do work in the Git repository, you need to make a local clone of the repository on your computer. You can find the URL needed to clone on the bottom right of the page, be sure to use HTTPS
.
Open up the command line and make a local clone with your URL:
git clone https://github.com/username/student-id.git
Now cd into the local clone and confirm that it works:
cd student-id
git status
which should output something like:
On branch master
Your branch is up-to-date with 'origin/master'.
nothing to commit, working directory clean
To make a connection with the upstream repository we forked off, we need to add another remote to the local repository. Use the following command with your id:
git remote add upstream https://github.com/tudelft-in4303-2015/student-id.git
Confirm that it works by fetching commits from upstream:
git fetch upstream
which should output something like:
From https://github.com/tudelft-in4303-2015/student-id.git
* [new branch] master -> upstream/master
Your local repository is set up now! Follow the steps below to work on an assignment.
Workflow
Starting an assignment
Every assignment is put into its own branch, named assignment1
, assignment2
, etc.
The correct assignment branch must be checked out in your local Git repository to be able to work on it.
The steps to check out a branch depend on whether we provide you with a template, or if you continue with work from a previous assignment.
Template
If the assignments asks you to check out a template, which for example assignment1
does, use the following steps:
git fetch upstream
git checkout -b assignment1 upstream/assignment1
git push -u origin assignment1
This checks out a fresh branch from the upstream repository. It does not contain any of your previous work.
Continue from previous assignment
If the assignment asks you to continue from the previous assignment, which for example assignment3
does, use the following steps instead:
git checkout -b assignment3
git push -u origin assignment3
The new assignment3
branch will be in an identical state to the assignment2
branch, but changes will only be comitted to the assignment3
branch, leaving the assignment2
branch as is.
Now you have the assignment branch checked out in your local repository and can start working.
Saving work
Whenever you have changes that you’d like to save, such as after getting (a part of) the assignment working, you need to add, commit, and push your changes:
git add --all
git commit -m "Message describing your changes"
git push
Submitting an assignment
Pull requests are used to submit an assignment in your origin repository to the upstream repository.
Make sure you’ve pushed all your changes first, then go to your origin repository (your fork) on GitHub.
If you’ve recently pushed changes, there should be a button with Compare & pull request
for the right branch, click that.
If there is no button there, go to the Pull requests
tab, press New pull request
, and set both branches to the correct branch for the assignment.
If all is well, it should display Able to merge. These branches can be automatically merged
, and you can press the Create pull request
button to submit your assignment. If not, check the troubleshooting section.
We will grade your assignment and post the results on the pull requests, so check back later.
Switching to another assignment
If you’d like to work on an another assignment, for example to fix things for a new submission, you can just check out the branch for that assignment. Be sure to push any changes to your current branch first, then check out the branch for the assignment you wish to switch to:
git checkout assignment1
Pulling in changes from upstream
If there’s something wrong in the template for an assignment, we fix it in the upstream repository, and you have to merge in those changes. Use the following commands to merge in changes (use the correct branch!):
git fetch upstream
git merge upstream/assignment1
git push
In most cases, Git will automatically merge in any changes, but sometimes conflicts can occur. See Resolving a merge conflict on how to resolve conflicts.
Git GUI clients
This guide uses command-line Git commands, but if you’d rather use a GUI, use SourceTree.
Troubleshooting
Cannot push
No access/rights
When Git complains about not being able to push because you do not have access or rights to the repository, this probably means that you’re trying to push to the upstream repository rather than origin. Push to origin using:
git push -u origin
No upstream branch
When trying to push without an upstream branch (note: an upstream branch is something different than the upstream repository!) being set, git will complain:
git push
fatal: The current branch assignment3 has no upstream branch.
To push the current branch and set the remote as upstream, use
git push --set-upstream origin assignment3
Git will tell you which command to run to set the upstream branch, just execute that. In this case:
git push --set-upstream origin assignment3
Out of date branch
You cannot push changes to a remote when that remote has changes that you haven’t yet pulled, you’ll get an error like:
git push
To ...
! [rejected] assignment3 -> assignment3 (non-fast-forward)
error: failed to push some refs to '...'
hint: Updates were rejected because the tip of your current branch is behind
hint: its remote counterpart. Integrate the remote changes (e.g.
hint: 'git pull ...') before pushing again.
hint: See the 'Note about fast-forwards' in 'git push --help' for details.
First pull changes with git pull
and then push your changes.
Cannot pull
Local changes
When you have changes in your local repository that you have not committed yet, and you try to pull, Git may complain about your changes being overwritten. First add and commit your changes locally with:
git add --all
git commit -m "Message describing your changes"
and then pull changes with git pull
.
No tracking branch
When pulling without a tracking branch being set, you will get the following error:
git pull
There is no tracking information for the current branch.
Please specify which branch you want to merge with.
See git-pull(1) for details
git pull <remote> <branch>
If you wish to set tracking information for this branch you can do so with:
git branch --set-upstream-to=<remote>/<branch> assignment3
Git already hints to the command that fixes the problem. Since you are pulling/pushing from origin, the following command will set the correct tracking branch:
git branch --set-upstream-to=origin/assignment3 assignment3
and then pull changes with git pull
.
Cannot automatically merge pull request
If a pull request cannot be automatically merged, your branch is out of date with the branch on upstream. Merge in changes from upstream (use the correct branch!):
git fetch upstream
git merge upstream/assignment1
git push
Resolving merge conflicts
See Resolving a merge conflict on how to resolve merge conflicts. You can also try a GUI merge tool such as DiffMerge to resolve merge conflicts.