Autograder for logic intro with lean

Stream: Lean for teaching

[Thorsten Altenkirch]

We (@Thorsten Altenkirch and @Cas Widdershoven ) are moving our module on Introduction to formal Reasoning (with 400 students !) to Lean4 (using also verso by @David Thrane Christiansen, hurrah). We were using an autograder written by @Jacob Neumann which was coded in lean3. Now we need to implement a new autograder soon (teaching starts end of September) :-(

Any help and advice or examples of existing autograders which fit our purpose would be very much appreciated. We would like to keep it simple.

Thanks a lot!

P.S. For obvious reasons I do not copy the exercises here but I can provide them on request.

[Michael Rothgang]

@Rob Lewis wrote an autograder for Lean. If you search zulip, perhaps you can find it - or a helpful soul can point it out :-)

[Julian Berman]

That's https://github.com/robertylewis/lean4-autograder-main I believe.

[Kevin Buzzard]

Updated to 4.22.0 two days ago :D

[Sergey Cherkis]

@Rob Lewis Is the corresponding shell script updated as well? I am having difficulty running it on Gradescope, even though autograder itself runs locally as expected.

[Rob Lewis]

@Sergey Cherkis we had some trouble last semester running the new version on problem sets that imported a lot of mathlib. Hypothesis, it was a memory issue on Gradescope's servers. Been on my to-do list to debug for a while but I don't have an answer yet. Are you running it with the maximum resources Gradescope offers?

[Sergey Cherkis]

@Rob Lewis Yes, I run it max (4.0 CPU, 6.0GB RAM). I managed to get the autograder to work, also reducing the students' solution compilation time to about 2 mins. Should I push this script or send it to you in some other way?