Teaching resources / Lean Game Maker for Lean 4

Stream: lean4

[Gihan Marasingha]

I'm currently using Lean 3 for teaching and assessing my large (~260 student) first-year introduction to pure maths module at the University of Exeter.

I've created teaching resources via the Lean Game Maker and the assessment is via GitHub Classroom / GitHub Codepsaces.

The assessment can easily be moved to Lean 4, but has anyone created a Lean Game Maker for Lean 4?

I could offer the teaching resources via GitHub Codepsace for my students (as the University of Exeter pays for the service), but that would be costly for the university and would not be easily accessible for anyone else who wants to use the resources.

This leads to the next question: can the trylean bundles be adapted for Lean 4? Is it simply a matter of using the Lean 4 binaries and mathematical library in the bundle in place of the Lean 3 binaries and mathlib?