Forums

Hi,

I’m preparing a homework guide for my “dotpy students”. Right now my focus is on the hand-in<->correction workflow (i.e. file syncing mechanism). Git through Gitlab would be my choice. But…

Creating a repo per student would be cumbersome to maintain and symlinking their home directories from my own might not be feasible since git’s behaviour towards out-of-repo files. I can only guess the mechanism that allows me to access my students homes under “my” /home/ but… just thinking out loud…

• What if every teacher got an empty read-writeable /home/.git/ directory ??? (same level as their student’s homes)

That would allow us to issue a git init command and then git commit all of our students’s files (including initialization rc-like files and command histories witch are userfull to track activities pitfalls).

Sounds straightforward, right? :)

Thanks in advance !

Leandro

Hmm, interesting! It's a clever idea, but unfortunately I don't think there's any way we could get that working with the way our system works -- each user's files need to be inside very specific locations, and there's no place that we could store the /home/.git. I'm also not entirely sure how it would interact with your own account -- for example, if you checked out a git repo in your own home directory (or if a student did in one of theirs) I suspect that things would go wrong in hard-to-understand ways...

Hi Giles,

Thanks for your answer. Accordingly, I took another approach: usually called RTFM ;)

It turns out that git’s CLI has some options that serves the purpose, picking an arbitrary root to a repo (either through command line or config files). I’be tested the former with a BASH alias and was able to performe basic operations normally. One can always reset the alias for repos other than the students’.

Steps to get it working. First, started a new project in Gitlab (remember not to initialize it, keep it empty). Then at a BASH console:

studentsRepo=home/CNBA/studentsrepo
gitlabRepo="git@gitlab.com:CNBA/students.git"
alias git="git -C / --git-dir=${studentsRepo} --work-tree=home"
mkdir /${studentsRepo} #note the leading slash
git init
cp ~/exclude /${studentsRepo}/info/exclude
git remote add origin ${gitlabRepo}
git fetch origin
git add .
git commit -m "initial student files"
git push -u origin master

As per your suggestion, and some files that can't be written, this is the final contents of the ~/exclude file:

.gitignore
**/.git/
#student private/readonly files
.bash_history
.viminfo
#myown home
CNBA/
#student homes to exclude
lean/

After that, as long as the alias is in place, all git commands work as usual (commit, push, pull, merge).

Thanks!

Leandro

PS: wasn't cleverness, just lazi* :D

Interesting! You're using a lot of git options I never knew existed -- will have to look them up.