beginner

Stream: Lean for teaching

[Scott Vaughen]

Hello, I'm a beginner with Lean (and git). I'm planning to learn Lean with my students when I teach an intro proof course starting in a few weeks. So far, I finished just the first two sections of Heather Macbeth's Mechanics of Proof and I'm so impressed - even if we do just a little in my class - I will be thrilled with any progress. I set up a github classroom but unfortunately I'm also a beginner with git. My question is for any guidance on the autograder. I found this: https://github.com/adamtopaz/hw_template but all this looks pretty confusing to a beginner. What does it mean "Just modify the hash in the file .github/classroom/autograding.json. So far I managed to make an assignment that students can modify a file and I can see the edits... I don't know how to accomodate the dependencies "lean_grader" and "mathlib4". Basically what do I need in the repo I create for students? thank you!!!!!

[Patrick Massot]

I’ll @Adam Topaz answer questions about his setup, but I’d like to point out https://leanprover-community.github.io/teaching/index.html in case you don’t know about it.

[Scott Vaughen]

thank you - if anyone has any experience using Heather MacBeth's book for an intro to proof course, I'd be very interested to hear from you - I'm particularly interested in using an autograder and I'm a very new beginner with Lean and GitHub so if you have patience to answer questions I have lots but I'm very excited about Lean as educational tool.

[Adam Topaz]

@Scott Vaughen here are some additional details on how my autograder works, in case it helps. As I mentioned in the PM, this currently only grades for complete correctness (so either 100% or 0%, nothing in between).

First a note: the homework template mentioned above uses the hash_approach branch of the autograder repo. What the autograder does is simply look for a file called Solution.lean in the homework assignment repo, and in that file it looks for a term called solution. It then looks at the type of solution, computes the "hash" of that type, and compares it with the hash provided when you run the command. It also ensures that the only axioms used in solution are the "standard" ones (the axiom of choice, soundness of quotients, and propext).

To work with this tool you can clone the homework_template repo, and add the command #type_hash solution after solution is declared in the Solution.lean file in order to get the hash (the default one should be 421340980, which you can see in the autograding.json file in the github classroom folder of the homework template). To grade the assignment, use lake exe grade 421340980 (replacing the number with the correct hash, of course). This is exactly the command that is run by github classrooms during the autograding step.

[Scott Vaughen]

super - thanks for the follow up - yes - this is very helpful - I'll keep experimenting and perhaps I can be a part of future conversations about autograders for Lean assignments