Skip to content

Commit

Permalink
describe codespaces prebuilds in teaching practices
Browse files Browse the repository at this point in the history
  • Loading branch information
robertylewis authored Jan 21, 2025
1 parent 4c89f57 commit ad09722
Showing 1 changed file with 6 additions and 0 deletions.
6 changes: 6 additions & 0 deletions templates/teaching/practices.md
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,12 @@ For GitHub Codespaces, it is important to remind students to sign up for
GitHub's [student benefits](https://education.github.com/pack)
to take advantage of extra Codespaces hours.

To save students time when creating new codespaces, GitHub has a "prebuild" option.
In your course repository, go to Settings -> Codespaces.
You likely want to prebuild on every push and store 1 version.
There is a nominal cost to storing these images:
currently the image for a course with a full mathlib build will cost about US $0.40 per month.

## Renaming and redefining tactics

The Lean/mathlib names for tactics may not match how you present these topics in class.
Expand Down

0 comments on commit ad09722

Please sign in to comment.