Set up a course
Your course's organization
Each course edition gets its own GitHub organization. Its students' teams and repositories live there, apart from everything else you have on GitHub. A free organization is enough.
Create it before anything else. The tokens in the next steps are made for this organization alone, and GitHub can only tie a token to an organization that already exists.
Use exactly this name when you create it. Already have one for this course? Just enter its name. The next step checks it exists, and that you own it.
The course repository's name
Students open their registration form in this repository. Keep the default unless you have a reason.
A token for setting up
A website can't make tokens or act on GitHub for you without one. So you make this one yourself on GitHub, with everything filled in, and paste it here. It's for setting up only.
How this token works
- It reaches and nothing else. It's a fine-grained token whose resource owner is . GitHub fixes that one owner when the token is made. It can't touch your own repositories, or any other organization.
- The page checks before using it. Classic tokens are refused, because they reach everything you can. The page then proves the token belongs to , with a request GitHub refuses without changing anything.
- It goes only to GitHub. It stays in this tab's memory and is sent only to
api.github.com. Nothing is saved, so closing the tab forgets it. There's no bedel server. The page's Content-Security-Policy (in its source) stops your browser from letting it connect anywhere else. - It lasts 7 days, and you can delete it the moment setup is done.
Rather not paste a token into a web page? Clone bedel and run ./scripts/setup.sh. It does the same with your gh login.
Make it
- Open GitHub's token page, filled in ↗
- Check that Resource owner says . If it shows your username instead, choose from the list.
- Under Repository access, choose All repositories, meaning all of 's repositories and nothing else. A link can't fill this in.
- Leave the permissions as they are, click Generate token, and copy it.
Every permission it asks for, and why
| Organization administration | Lock down what members can do: students can't create, delete or publish repositories |
| Administration | Create the course repository |
| Contents | Write course.json, your course's settings |
| Issues | Add the labels the bot uses on registrations |
| Secrets | Store the roster and the bot's token, sealed |
| Actions, Workflows | Run the workflow that writes the students' form |
| Pages | Publish your course's own page |
| Members (read only) | Check that you own the organization |
The course
Students see the name. Classes are the weekly sessions that soft deadlines are counted from. Leave them out if your course has none.
| Class | Day | Session ends | Note (optional) |
|---|
Your students
These files don't leave your computer. They're read here, in your browser. Only the student numbers (and classes) found in them are sent to GitHub, sealed as secrets.
The roster is who may register: a CSV export with a student-number column, or a plain list of numbers.
Class listings are optional: one file per class with a Class: P1 (or Turno: P1) line,
or one file of number,class lines.
The bot's token
The bot is the set of GitHub Actions workflows in your course repository. They create teams and repositories and lock them at deadlines, so they need a token of their own, kept for the whole term.
How the bot's token works
- It reaches and nothing else. Like the setup token, it's fine-grained and made for alone. The page checks that before storing it.
- It's sealed, then kept by GitHub. Your browser encrypts it with the course repository's public key.
It's stored as that repository's secret
ORG_ADMIN_TOKEN. From then on only that repository's workflows can read it: not this page, not other repositories, not even you on GitHub. - It can do only what the bot does. Every permission is listed below.
- It lasts as long as your term. When it runs out the bot stops, your course's page tells you, and you replace it there.
- It acts as whoever makes it, who must own . A separate GitHub account just for the bot, made an owner, keeps the bot's actions apart from yours.
Make it
- Open GitHub's token page, filled in ↗
- Check that Resource owner says , and choose All repositories. The bot creates new repositories all term.
- Leave the permissions as they are, generate it, and copy it.
Every permission it asks for, and why
| Administration | Create each group's repositories, give their team access, and make them read-only at the hard deadline |
| Contents | Put the starting files in, and archive every push |
| Issues | Tell each group about a new assignment |
| Commit statuses | Mark commits pushed after the soft deadline as late |
| Workflows | Copy starting files that contain workflows of their own |
| Members | Create each group's team and invite its students |
Set it up
Here's everything that happens. Each part checks what's there first, so running it again changes only what differs.