Installation manual for students

Stream: Lean for teaching

[Martin Dvořák]

Which version of Lean do you use for teaching? What installation manual do you give your students? Do students often encounter technical obstacles?

[Patrick Massot]

So far I teach using Lean 3, and I give them autonomous bundles that can be seen as customized versions of https://leanprover-community.github.io/get_started.html#maybe-a-couple-of-nights (although technically it's the other way around, the bundles on the website are derived from my teaching setup).

[Jannis Limperg]

For Logical Verification we use Lean 3 with these installation instructions: https://github.com/blanchette/logical_verification_2022 (based on those from the leanprover-community site). A clear majority of students have no technical issues. We also provide a VM, but as far as we know it has gone unused for two years.

[Martin Dvořák]

Jannis Limperg said:

For Logical Verification we use Lean 3 with these installation instructions: https://github.com/blanchette/logical_verification_2022 (based on those from the leanprover-community site). A clear majority of students have no technical issues. We also provide a VM, but as far as we know it has gone unused for two years.

Do students with Windows follow the whole setup?
Get Lean
Get Python
Configure Git
Install Lean Tools
Install and Configure the Editor
Install Our Logical Verification Repository

[Jannis Limperg]

Yes (unless, I guess, they already have Python or Git).

[Matthew Ballard]

Lean 4. I stick to core and pin it to stable. It makes it painful to incorporate useful facts (like most proofs for int) from either std4 or mathlib4 since those run on nightly but it avoids any breakage of existing code in core. I assume they will not be installing it on their own machines so provide container config files. We started with just GitPod but now each repository has GitPod and Codespaces config files. Students seem to generally Codespaces because it is a single click away from the GitHub repository by default. The assignment due today is https://github.com/UofSC-Fall-2022-Math-300-H01/homework10.