autograding with GH classroom

Stream: Lean for teaching

[Matthew Ballard]

I put together a basic auto-grading setup for Lean homework assignments using GitHub classroom at https://github.com/c0ppelius/lean-autograding

[Matthew Ballard]

The actual testing can certainly be improved. The main value of the repo is to show how to integrate calls to Lean into the GH classroom setup.

[Heather Macbeth]

Darn, I hacked together something literally last night :)

[Heather Macbeth]

Anyway, thank you for this (I am sure) far more professional setup!

[Matthew Ballard]

Great minds :)

[Matthew Ballard]

Did you use GitHub Actions?

[Heather Macbeth]

Mine is for Gradescope, although it's probably not so different.

[Matthew Ballard]

That seems like it might have better LMS support

[Matthew Ballard]

It also has the advantage of not using git

[Heather Macbeth]

We'll see how my students find it, but the interface seems pretty easy, they just upload a single Lean file with a specified name.

[Heather Macbeth]

And I see we came up with the same mechanism for scoring: first fail globally if the file contains errors or warnings, then apply a series of tests to verify whether each exercise has the type it's supposed to.

[Matthew Ballard]

Ideally one would parse the document and test whether there is a proof of the correct type somewhere in there. If you wanted to give more open ended assignments.

[Matthew Ballard]

Things like axiom's and constant's could be filtered depending on if they came from source file, eg you have to prove X but can assume and use Y,Z and not worry about their proofs

[Matthew Ballard]

Did you include hints or anything in your message to students?

[Heather Macbeth]

@Matthew Ballard I didn't include any check to filter out axioms. My class is small enough that I plan to glance over everyone's code anyway, so I would catch that sort of thing visually. It would be very nice to have this check, though (you do this?).

And I also don't include any hints, except that in the "fails globally" case here:
Heather Macbeth said:

And I see we came up with the same mechanism for scoring: first fail globally if the file contains errors or warnings, then apply a series of tests to verify whether each exercise has the type it's supposed to.

it posts a message saying that it has failed globally due to an error/warning in the file, so that a student with a submission containing 4 correct problems doesn't get confused about why her score is 0.

[Heather Macbeth]

However, the proof is in the pudding! I am curious to see how it works when tried on actual students :)

[Johan Commelin]

If the proof is in the pudding, where is all that pudding in mathlib?? :yum:

[Matthew Ballard]

Continuing with this thread, I have some meta code that checks for a term of a given type anywhere in assignment.lean which removes the requirement that students name their solutions strictly.

[Matthew Ballard]

I still really wish I could pull the axioms without passing through stdout.

[Matthew Ballard]

import tactic
import assignment

variable T : Type

open tactic

meta def in_import (env : environment) (n : name) (path : string) : bool :=
(env.decl_olean n = path) && env.contains n && (n ∉ [``quot, ``quot.mk, ``quot.lift, ``quot.ind])

meta def exact_list : list name → tactic unit
| [] := failed
| (H :: Hs) := do
                  e ← mk_const H,
                  exact e <|> exact_list Hs

meta def check_solutions : tactic unit :=
do env <- get_env,
   let decls := env.fold [] list.cons,
   cwd ← unsafe_run_io io.env.get_cwd,
   let names := decls.map declaration.to_name,
   let assignment_names := names.filter
     (λ x, in_import env x (cwd ++ "/src/assignment.lean") && not x.is_internal),
   exact_list assignment_names

theorem check : T  :=
begin
  check_solutions,
end

[Matthew Ballard]

Update: lean X.lean dumps everything to stdout. stderr is empty. So the GH autograding action only cares about the exit code of the process.

[Gihan Marasingha]

Great stuff! I've been away from Zulip for a few months and it's amazing to see what's happening. I'm actually planning to use Git Hub Classrooms with Lean for the new academic year.

[Eric Wieser]

I recently used github classrooms for a non-Lean course; one tip I'd give would be to put a very minimal action in the student repo that references the real action, so that you can fix bugs in it without having to tell students how to update their git repository to get the new grader. That looks something like:

jobs:
  build:
    # this name must be exactly this for the points to be reported to github classroom
    name: Autograding
    runs-on: ubuntu-latest

    steps:
    - uses: actions/checkout@v3
    - name: Run grading
      uses: my-classrooms/my_class_action@2022  # version by cohort so as not to break submissions next year

where my_class_action is a github "composite action"

[Matthew Ballard]

Gihan Marasingha said:

Great stuff! I've been away from Zulip for a few months and it's amazing to see what's happening. I'm actually planning to use Git Hub Classrooms with Lean for the new academic year.

Thanks. I am not sure if this is in a completely working state currently. I am trying out Lean 4 for my class so will have to rewrite it that in a week or so.

[Matthew Ballard]

This semester is my first honest rodeo with GH classrooms so I am noticing some sharp edges. For example, it appears that instructors cannot set student groups for assignments. In fact, an instructor cannot create the (empty) named groups themselves. All group creation and membership is on the student end. There is a time-intensive workaround to create the empty groups but it still relies on students correctly joining their assigned group. You cannot fix a mistake without dumping the whole assignment and starting over.

[Matthew Ballard]

Perhaps people here are better versed, but is this really the state of things for student group creation/curation?

[Mike Shulman]

I'm trying to use Lean 3 with gradescope, but I'm confused about how to deal with sorry. It seems that definitions using sorry produce only a warning, not an error, and in particular don't set a positive exit-code, so I'm not sure how to test for them programmatically. Is there a flag I can give to Lean to tell it to treat sorry as an error?

[Mike Shulman]

I tried to figure out from the posted GH code how you're dealing with this, but I couldn't even figure out how lean is getting called or its return values parsed.

[Mike Shulman]

Would anyone who's used gradescope be willing to share their autograder setup?

[Alex J. Best]

I think you can use trust level 0 -t0 flag to lean to get this behaviour, not sure what other effects this will have though

[Matthew Ballard]

Hi @Mike Shulman long time no see. Here is the relevant function. The classroom json file just calls lean .test/test.lean and expects nothing in response in stdout.

[Mike Shulman]

@Alex J. Best Thanks, that seems to work! It wasn't at all clear to me from the lean --help output that "do not trust any macro" included "do not allow sorry", but maybe sorry is a macro or something?

[Mike Shulman]

@Matthew Ballard Thanks. You appear to be doing some fancy coding in Lean that I don't understand. What does your script do if the student hasn't solved that exercise?

[Alex J. Best]

Yes this is not obvious from the help menu, but we've had this discussion on here somewhere before I think, and also wondered a lot about how to really check that people used no extra axioms for codeforces-like online challenges (its a long story and very hard to do right it turns out)

[Matthew Ballard]

(Again from memory but) I tested this and it should fail because it yields either an error because there is no statement with the appropriate name or the proof is not complete and it is sorry'd by default

[Matthew Ballard]

At the end of the rabbit hole was "you need to inspect the oleans"

[Matthew Ballard]

Anything beyond that can be gamed but if you just want something plausible, this was enough for me. (Currently I have go test file in the main directory for my cryto class to give you an idea of my level of concern ...)

[Mike Shulman]

Ok, thanks! I think I'm just going to test each exercise with a separate testing file run under -t0, so that I can test the exit codes rather than have to parse the textual output.

[Matthew Ballard]

Mine was mainly an exercise for myself in meta-programming :)

[Mike Shulman]

At least, until someone writes a gradescope-utils package in Lean that will automatically produce JSON... (-:O

[Matthew Ballard]

I am going to take another run in Lean 4 later this week and will report back. (Though not in gradescope)

[Matthew Ballard]

I now remember the concern that led me here: I didn’t want students to declare and use convenient axioms.

[Mike Shulman]

I tried that, but it seemed that student-declared axioms are caught by the computability checker: anything depending on an axiom has to be flagged noncomputable, and my test definitions are not so flagged, hence raise an error. But I don't know much about how Lean works; is there an easy way that students could defeat that?

[Matthew Ballard]

Label them noncomputable?

[Mike Shulman]

But an error will still be raised if my functions in the testing file aren't labeled noncomputable, and the students can't change those.

[Matthew Ballard]

This is good enough for Codewars so is probably good enough for coursework.

[Matthew Ballard]

If you are going to look at the submissions yourself, then the cost to benefit ratio tips over after just a simple sorry check.

[Mario Carneiro]

noncomputable is not a good defense against axiom use, because you are allowed to use axioms that prove propositions in computable functions. So a student could just have axiom my_sorry : false and they could even use it in a function implementation without it getting marked noncomputable.

[Mario Carneiro]

axiom my_sorry : false
def my_computable_def : nat → nat := my_sorry.elim

[Siddhartha Gadgil]

May be a silly question, but what if a student uses sorryAx manually instead of using the sorry macro?

[Matthew Ballard]

Codewars and test.leanboth implement the two step check:

• have Lean check the proof
• inspect the axioms to make sure nothing out of bounds is used

Codewars parses the stdout/stderr using some JavaScript. The test file in the repo does axiom inspection in Lean itself.

[Matthew Ballard]

General consensus from before was that this could be defeated but then a student probably would have learned enough in the process.

[Matthew Ballard]

Both @Rob Lewis and @Heather Macbeth have experience with gradescope in particular. They might know more about talking to it

[Patrick Massot]

All this becomes a real issue only if someone smart figures out a way to cheat and then tell everybody about it.

[Matthew Ballard]

We did make this stream public :smile:

[Matthew Ballard]

But I would think CS students are fairly familiar with looking for the test file, seeing the test cases, and then fitting a function to those.

[Matthew Ballard]

If you are looking at the submission, then this fails quickly though.

[Mike Shulman]

So you're saying there's no way to extract the information from lean about what axioms are used other than something like #print axioms and then parsing its textual output?

[Alex J. Best]

You can do it with lean meta-programming, e.g. as seen in https://github.com/leanprover-community/mathlib/issues/10954

[Matthew Ballard]

test.lean is a specific lean 3 internal implementation of the meta-programming approach Hmm I thought I did a meta-programming one but it appears it took the easy way out :)

[Matthew Ballard]

Ah right @Mario Carneiro gave that implementation (also seen here https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/intuitionistic.20logic/near/224372208) and I put adding it to the repository on my to-do list (and never took it off)

[Matthew Ballard]

Also interacting with GitHub Classroom (and Gradescope too?) occurs via stdout/stderr anyway: give some json specifying which command to run and what to compare the output to.

[Mike Shulman]

Gradescope just runs a script that you specify, and expects the results to be placed in a specified JSON file. It doesn't do any output comparison, it expects a particular JSON format that specifies the score.

[Matthew Ballard]

Oh, it appears they have libraries in common languages to help with the file creation. Right? Or is it just Python?

[Matthew Ballard]

Hmm, even the Java one dumps to stdout and saves the result in a json file.

[Mike Shulman]

Yes, they have libraries that integrate with testing frameworks in Python and maybe a few other languages, but the end result is always a json file of the same format.

[Mike Shulman]

After actually trying this, I realized that my original question about sorry wasn't even what I really wanted anyway. Using -t0 answers that question, but raises an error if any function in the file uses sorry, when actually I would like them to be able to leave the sorry there for some questions and still have the others graded. So I guess I need to use print axioms even to detect sorry.

[Gihan Marasingha]

I'm using a Windows machine at the moment and @Matthew Ballard's test.lean file contains the string/src/assignment.lean, which Windows doesn't like!

Is there a way for Lean to use slashes appropriate to the OS or do something else to get the correct path?

[Matthew Ballard]

Does switching to \src\assignment.lean fix the issue?

[Gihan Marasingha]

Matthew Ballard said:

Does switching to \src\assignment.lean fix the issue?

Yes it does. I was wondering if there was an OS-agnostic solution. It's not a big issue if there isn't one!

[Matthew Ballard]

You should be able to match off the head of the result of io.get_cwd to handle different cases. Whether there is a builtin function for constructing a system path from a list, I am not sure.

[Sarah Smith]

Hi @Matthew Ballard , did you end up re-writing your autograder for Lean 4? Do you still plan to? https://github.com/mattrobball/lean-autograding

[Matthew Ballard]

I have something that I am currently using but the functionality is far from what I would like given the capabilities of Lean 4. The main limitation is time.

You can see it at work here.

[Adam Topaz]

https://twitter.com/derKha/status/1578493681304494080?s=20&t=xJ4T-mPBhLLOFn4RwICxAQ

a) cool, Lean made it to homework questions on SO b) "discrete math" seems a bit... broad c) why does the title read like a LLM prompt https://twitter.com/derKha/status/1578493681304494080/photo/1

- Sebastian Ullrich (@derKha)

[Adam Topaz]

Just pointing this out because the questions seem very similar to https://github.com/UofSC-Fall-2022-Math-300-H01/homework5/blob/main/Hw5.lean

[Sebastian Ullrich]

See also https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/Newest.20questions.20tagged.20lean.20-.20Stack.20Overflow/near/302931112 where I took it from :)

[Matthew Ballard]

We talked about this in class today. Sinners-in the-hands-of-an-angry-god-style. :wink:

[Matthew Ballard]

But seriously, the most upsetting issue was the person on twitter that claimed this was from a freshmen CS course on discrete math. Really reminds me not to believe anything I read on the internet.

I should have looked more closely. These were familiar not because they were all in the assignment but because they came from Chapter 4 exercises in Logic and Proof!