Compiler Construction bio photo

Compiler Construction

Twitter Github

Edit on GitHub

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.

Fork

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.

Clone URL

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.

Compare & pull request

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.

Pull request

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.