Skip to content

Repository System

Jump to bottom
David Blajda edited this page Apr 5, 2017 · 2 revisions

Repository System

THIS IS A WIP

The main goal of the repository system is to provide a centralized location for assignment submission that will contain backups of student's work and will allow systems such as an auto grader, similarity checker, and file structure checker to provide interactive feedback.

A requirement of the system is to allow users to modify the repository through the web interface or through command line git.

Current State

To satisfy the above requirement of allowing a web interface, the Git repository cannot just be a bare repository but must also contain a working a working directory. A working directly is what allows a user to use their favorite git verbs add, commit to perform actions on the repository. Git actions through the web interface is provided by the GitElephant library:

https://github.com/matteosister/GitElephant

The requirement of having a working directory increases the complexity of allowing a user to clone their repository to use CLI Git. This conflict is best described with the follow scenario: A student likes to use command Git for the majority of their workflow.

  1. They clone their repository.
  2. They make local changes and commit.
  3. They attempt to push their changes back to the server.
  4. If the system is not set up properly the push will be denied by the remote server since it will screw up the working copy.

To truly understand the problem try this on your local system:

cd
git init a1
git clone a1 a1copy
cd a1copy
touch test
git add test && git commit -m 'init repo' && git push

You will get the following error

[master (root-commit) 2a05419] init repo
 1 file changed, 0 insertions(+), 0 deletions(-)
 create mode 100644 test
Counting objects: 3, done.
Writing objects: 100% (3/3), 206 bytes | 0 bytes/s, done.
Total 3 (delta 0), reused 0 (delta 0)
remote: error: refusing to update checked out branch: refs/heads/master
remote: error: By default, updating the current branch in a non-bare repository
remote: is denied, because it will make the index and work tree inconsistent
remote: with what you pushed, and will require 'git reset --hard' to match
remote: the work tree to HEAD.
remote:
remote: You can set the 'receive.denyCurrentBranch' configuration variable
remote: to 'ignore' or 'warn' in the remote repository to allow pushing into
remote: its current branch; however, this is not recommended unless you
remote: arranged to update its work tree to match what you pushed in some
remote: other way.
remote:
remote: To squelch this message and still keep the default behaviour, set
remote: 'receive.denyCurrentBranch' configuration variable to 'refuse'.
To /home/david/scrap/a1
 ! [remote rejected] master -> master (branch is currently checked out)
error: failed to push some refs to '/home/david/scrap/a1'

Thankfully the error messages tells us how to remedy this

cd ../a1
git config receive.denyCurrentBranch  ignore

Now lets try pushing again

cd ../a1copy
git push


Counting objects: 3, done.
Writing objects: 100% (3/3), 206 bytes | 0 bytes/s, done.
Total 3 (delta 0), reused 0 (delta 0)
To /home/david/scrap/a1
 * [new branch]      master -> master

Cool, looks like everything is fixed! Let's checkout the working copy of a1.

cd ../a1
ls

                                           Nothing is here

Oh no! where did our pushed file go? Maybe git log can tell us something git log

commit 2a0541970b7056664fc0b68d3484b16112f29b7d
Author: David Blajda 
Date:   Tue Apr 4 18:59:46 2017 -0400

    init repo

While it seems like the push did go through... git status

On branch master
Changes to be committed:
  (use "git reset HEAD ..." to unstage)

        deleted:    test

Weird why does git think we deleted the file in this repository? What ended up happening is that git updates the value of HEAD and stores all the required objects for the last commit in .git but during the push it doesn't update the working directory.

To fix this we can do the suggested command, which will then update files in the working directory. git reset HEAD --hard

So to maintain a valid working directory for the user it is important to reset the working directory after each push. This is currently accomplished with a modified version of this script:

https://gist.github.com/dchest/243747

Currently the system is in it's infancy and provides hooks for similarity checking.

Todo

Improvements need to made to the system. Some suggestions are outlined in the following issue.

https://github.com/guelph-code-ninjas/core/issues/56

Clone this wiki locally