Local Git server

Technical Programming
#1

At my team’s last regional, I downloaded their entire Github repo and brought it on a server so they could continue to commit and push to a backup as desired (over Ethernet to comply with the wired-only communications rules).

I realized that this could service many more teams.

We are traveling to the Houston regional here next week. If you post here (or PM me) the url to your Github repo by Tuesday (the 13th). I will download and cache it to our server that we will be bringing (Tuesday night).

How do I access it?
Bring a long Ethernet cord to run from our pit to yours (with the appropriate taping and mats as needed for safety in walkways - we can bring some rugs/tape), or plan to bring your laptop to a station we will have in our pit (with an Ethernet cord) to connect.

**How would I push or pull? **
Git allows for multiple remotes - https://git-scm.com/docs/git-remote, we will leverage this to setup an extra remote that you can explicitly push to or pull from when connected to the server.

What languages would this support?
All of them. It’s just a Git server just like GitHub (without the WebUI or issue tracking)

We use Github, but I’m not that familiar with Git. Will you help?
Our software team (and several of our mentors including myself) will be available to help teams get setup.

Won’t that mean you have access to our code?
If your code is in a public Github repo, we already do :), but we can also add a user account/password to access the downloaded copy if you want (PM me desired username and pword)

#2

That’s an excellent idea! I can imagine that working really well and benefiting all sorts of teams, however, I want to warn you about the dangers of stringing ethernet cables across multiple pits. Not only is it extremely dangerous (ie. tripping, pulling your server off it’s rack, pulling computers off tables, etc), it’s a massive inconvenience and probably won’t get past any Pit Admins. However, I love the idea. What I would recommend doing is creating a guide to help teams create their own local servers, or making and distributing a program that teams can run on one of their computers and run their own local servers with ease. This way, you can have your server, and your pit won’t become a bird’s nest of cables.

#3

1418 used to just create a remote to a usb stick that we would pass around.

#4

95 uses a raspberry pi and a switch (or router? I’m not sure) in something with call PitHub™ which runs our offline GitHub server. We then dump everything to the real GitHub every night. We’ve loved it since 2016.

This is definitely something teams should be using! Great idea to offer it to other teams mshafer1!

#5

Indeed, PitHub was a huge help this year!

As a logistical helper, you may find this useful:

Since most of the time our laptops are configured to request an IP address via DHCP, it’s useful to run a DHCP server on the Raspbery Pi that hosts our repo. But it’s also useful to connect it to the hotel’s internet connection, which requires NOT running a DHCP server. So we have a hardware switch on the outside, and a Python script that polls the switch and turns the DHCP server on or off as needed. Hope it helps someone!

#6

That sounds like a great idea! I have been thinking about turning an unused laptop into a repository. Does anyone have any tips or suggestions?

#7

Yep. IMO using a USB stick to collaborate is the easiest and least-hardware intensive approach. It’s much simpler than setting up a server on a network (though, very similar in terms of git operations):

  1. Open your terminal, change directory to your USB drive
  2. Execute ‘git init --bare some_name’
  3. Change directory to your locally checked out version of the git repo
  4. Execute ‘git remote add usb /path/to/usb/drive/some_name’
  5. git push usb master

Note that you can name your remote anything, usb is just the name we used.

Once you’ve done this, you can push/pull/whatever to the bare git repo that’s sitting on your USB drive, just like you would any other remote. No complicated networking scripts required.

#8

Hmmm. Not really the responses I was expexting.

That sounds like a great idea! I have been thinking about turning an unused laptop into a repository. Does anyone have any tips or suggestions?

See the post by virtuald.

95 uses a raspberry pi and a switch (or router? I’m not sure) in something with call PitHub™ which runs our offline GitHub server. We then dump everything to the real GitHub every night. We’ve loved it since 2016.

This is definitely something teams should be using! Great idea to offer it to other teams mshafer1!

That’s the setup we were using too. I have a couple of Ethernet switches to expand the number of available ports beyond our consumer router (acting as the dhcp server).

I want to warn you about the dangers of stringing ethernet cables across multiple pits. Not only is it extremely dangerous (ie. tripping, pulling your server off it’s rack, pulling computers off tables, etc), it’s a massive inconvenience and probably won’t get past any Pit Admins.

I expect that if the cords are properly taped and covered with rugs whenever they cross a walkway that it should be ok. We will make sure to get this cleared by either the LRI or the Admin before running wires to be sure.

#9

Remember that since git is a distributed system any repo can pull from any other. The easiest way I’ve found to make repos available is by adding an ssh server to the machine you want to pull from. This makes it easy for us to, say, pull changes off a Jetson onto our laptops :

git pull ssh://ubuntu@10.9.0.8:/home/ubuntu/2018RobotCode

Same thing works between laptops - no need for a central server. No argument that a centralized server makes it easy if you have a large programming team but if there are only 2 or 3 people working on fixes peer-to-peer like this can work. Eventually everyone pushes back to github when they can.

We’re developing using Linux but I see there are similar setups for windows : https://github.com/PowerShell/Win32-OpenSSH/wiki/Setting-up-a-Git-server-on-Windows-using-Git-for-Windows-and-Win32_OpenSSH

#10

It’s pretty clear that most of the folks who have commented here don’t really understand git. The quotes below are from people who do.

One of the misunderstandings that I see programmers make all the time on these forums is conflating git with GitHub. They are not the same. git was never intended to be a centralized versioning system*. It was intended to be distributed. You do not need internet access or network access to commit things or share things, though it does make things easier.

#11

USB stick is the way we go (FlashdriveHub is what I usually call that remote). It is very kind of OP to provide an extra server-based setup for public usage!

One thing to keep in mind: While git can push/pull from any two repositories, even two peer development laptops, a more useful workflow is usually to have one “blessed” repository, that the team agrees is the definitive one. Development work is not “done” until it has been merged & pushed on the blessed repository. Maintaining many blessed repositories leaves it open to interpretation which is correct when they differ on commits.

In general, our workflow shifts such that at a venue, FlashdriveHub becomes the blessed repository. Github will not be up to date. Only at night or after a regional will the two get synced, and Github again becomes the blessed repository.

#12