git(hub) for non-programmers

Stream: general

[Julian Berman]

Hello. This is slightly off-topic for Lean itself, but hopefully not too distracting.
I am tasked next week with teaching some non-programmer students Git and GitHub, and ideally with convincing them that even though they are not programmers, that they will 1) encounter these things in their lifetimes and 2) benefit from knowing how to use them in a working sense.

I feel reasonably comfortable with 1, especially knowing some of the software they will deal with. If they want to interact with where that software is being developed, or have an issue, they'll need to navigate GitHub at very least.
I can make arguments for 2, but given I am a biased programmer I am curious if folks in this community have learnings or opinions on whether you wish you were told about them sooner, whether they indeed are helpful or whether it's just programmers saying we use these tools and they're table stakes to work on things, whether you believe their use is or is not limited to mathlib-like cases where the fundamental artifact being worked on is still a piece of software, or whether once you've learned about them you extended their use elsewhere.

I'm less concerned with how much git and github to teach them, I think there's a reasonably easily justifiable subset, but strong thoughts there certainly are welcome nonetheless.

[Arthur Paulino]

I can speak from experience on this one. For a while I was stubborn enough not to adhere to git and maintain projects with dropbox instead. First big issue was when I tried to do anything collaboratively due to conflicts. Second big issue was needing to be excessively careful when making changes on the code base because I was scared of breaking stuff and then having to manually rollback many files in the dropbox app.

Turns out git branches and the mechanics of merge requests (pull requests on GitHub) solve both issues above. Branching out from the default branch provided me so much more freedom to think and try new things in my projects.

Also being able to have a closer look on any proposed change made a big difference. And the changes can be reviewed by more than one person, which is simply amazing in terms of teamwork.

[Kevin Buzzard]

Over the past two weeks a few students have pointed out typos in the course notes in the course I'm teaching with some other lecturers. Because one of the lecturers is computer-phobic we're using dropbox to write these notes, which works fine -- the three of us are in charge of different parts. We update them, recompile, and post an updated pdf once every few days. Yesterday a student sent us a really grumpy message saying that the course notes had changed but they had covered their original v1 pdf copy with comments etc, so could we send them a list of all changes made. Answer: this would have been easy if we were using git.

[Oliver Nash]

This might be a bit of a stretch but maybe a useful "real world" example for non-programmers.

Knowing how to navigate GitHub recently helped me decide where to go on holiday. COVID vaccination rate was a significant factor in choice of destination and Malta came out top. However shortly before I booked, its population proportion vaccinated on a reliable website suddenly dropped. The site is open source so I followed its link to GitHub and after a few minutes link-following to dependent repos, and searching for recent commits containing "Malta" I found this: https://github.com/owid/covid-19-data/commit/b82a7cb189924a8eb4f6ca9a9c0728a6442f98f5

It turns out the proportion had dropped because the population estimate was too low. Being able to navigate GitHub like this allowed me to rebuild my confidence that the data I was using, though not perfect, was worth trusting.

[Jason Rute]

One way to think of git and GitHub is as a really nice backup system that lets you play with ideas and be willing to royally mess things up, but have a safe place to return to. You don’t have to worry about having copy after copy. If they use markdown, html, or latex (I don’t know your audience), then it is a really great place to store your written projects and websites. I versioned my thesis in git. Also github.io is a good place to make a website using only markdown. Also, where this becomes really useful is collaboration. Two people can work in the same document or project without fear of messing up what the other person is doing. (Obviously if you are editing the exact same parts you will have to eventually resolve that, but usually people are working on different parts.) last, GitHub provides a nice culture of sharing. You can fork someone else’s project and just play around with it. If you find a bug, you can fix it and make a PR.

[Arthur Paulino]

Not to mention the possibility of having automated separated batches of tests for new branches before performing any merge.

Another strong point is that it's a canonical practice for git repositories (GitHub, GitLab, BitBucket etc) to implement integrations between issues and merge requests such that when a branch is merged into the default branch, the linked issue is automatically closed. So an automated level of project management kicks in and makes our lives easier.

[Julian Berman]

(Thank you all, these are all really helpful already to hear, and Oliver your example certainly wouldn't have been on my list but I'm very glad you mentioned it :)

[Eric Taucher]

As a programmer who uses many projects stored at GitHub and who checks changes on some daily it is nice to see the changes in almost real time.
On a side note, make sure to cover the granularity of commits. Big commits are bad, IMO multiple commits for one concept are also bad.

[Julian Berman]

My experience is that it's hard to teach that even to programmers who use it daily, but yeah I'll do what I can. And thanks as well, that's another good point I'd forgotten about following changes.

[Kyle Miller]

For an online offering of linear algebra, we used a private git repository on GitHub for source files for course materials as we developed them (mostly files describing quizzes for Canvas). It was nice knowing that every version of every quiz was saved, in case we messed anything up, and also it was nice being able to review what everyone was doing. My colleagues, who had never used git before, used GitHub Desktop successfully after a little bit of training. We never really worked on the same files, so we only had the occasional merge conflict.

[Arthur Paulino]

Good point. GitHub Desktop App can help a lot, abstracting git concepts without the need to memorize git commands

[Adam Topaz]

Here is one way in which I use github for work on a daily basis (this is not about git, per se).

I am teaching two courses this term for which I am posting typeset lecture notes. My university has a CMS for courses (similar yo blackboard), but it's, well, cumbersome. It takes a login and at least 5 mouse clicks to update the pdf for my lecture notes if I want to do it through the web app. As someone who likes vim bindings and who avoids the mouse at all costs, I find this unacceptable. So, I use github to store the latex source for my lecture notes, and I set up a CI script that compiles the notes and uploads a PDF to aws s3 every time there is a push to master. I just posted the link to the pdf file on s3 once, and the students always have the most up-to-date version of the notes. I've also done something similar in the past where students had access to the github repo iteself, so instead of getting 37 emails a week about typos, I would ask them to just open a PR.

[Julian Berman]

Thanks. Also very helpful, and yeah I'm kind of trying to see how I can describe these kinds of GH Action workflows to them, though it's tough learning alongside the rest so I'm still thinking about how to do so -- certainly these are little serverless automation tasks that were 10x harder in the past so it does seem important to touch on if I can fit it in somehow. (I sympathize too on the CMS workflow, Canvas doesn't seem much better.)

[Patrick Massot]

Adam, did you actually ever had a student PR? I tried that but it never worked.

[Siddhartha Gadgil]

Our Mathematics Department website is collectively maintained by a bunch of us by editing the source on github. Of the 8 or so active maintainers I would say only 2 can be called programmers.

[Adam Topaz]

Patrick Massot said:

Adam, did you actually ever had a student PR? I tried that but it never worked.

I actually did get some student PRs! But I should specify that this was a small graduate course. I don't think this would have worked in an undergrad course.