Skip to content

Commit

Permalink
describe codespaces prebuilds in teaching practices (#582)
Browse files Browse the repository at this point in the history
Co-authored-by: Bryan Gin-ge Chen <[email protected]>
  • Loading branch information
robertylewis and bryangingechen authored Jan 26, 2025
1 parent dbec3e4 commit d651d85
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 (Jan. 2025) 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 d651d85

Please sign in to comment.