import file with errors

Stream: lean4

[Rob Lewis]

I'm working on improving my Lean 4 autograder for Gradescope (based on code by @Vanessa Rodrigues and @Gabriel Ebner ). The big-picture structure of the autograder is this. We have a course project with a whole bunch of files. A student edits one file, HW.lean, and upload it to the autograder. The autograder has the full course project including the original HW.lean, which has some problems tagged as exercises. It creates two environments, one with the original HW.lean and one with the student's version, and checks that the tagged declarations exist in the student's version and do not contain sorry or extra axioms.

The problem is, if the student's submission doesn't compile, we can't create the second environment -- the import fails and the grade is a 0. This is confusing in the case, for example, where a student has finished 9/10 of their proof obligations. If they submit a file with one unfinished proof they don't get credit for the 9 they did finish. In VSCode it looks like the file "works" except for the one issue. This spring I tried to train students to always sorry incomplete proofs. This works but isn't foolproof, it can be easy to miss especially if an incomplete proof has multiple goals left.

Is there any way to do a "soft" import of the submitted file, that works more like a file with errors in the editor, where incomplete proofs are sorryed?

[Mario Carneiro]

Don't use an import, process the file directly to get an environment

[Mario Carneiro]

that is, do it like the server would

[Rob Lewis]

This part of the autograder came from Vanessa's original script, so I'm not as clear on the details. Right now it's using importModules to produce the environment. When you say "process the file directly," is there a different function to drop in here?

[Rob Lewis]

(This is an older version of the autograder, our updates are in a private repo, but we haven't changed anything relevant to this question)

[Adam Topaz]

I don't know what Mario has in mind precisely, but I suppose you could compile the file with docs#Lean.Elab.IO.processCommands . I did something similar in the auto-grading tool I made here: https://github.com/adamtopaz/lean_grader

[Rob Lewis]

Oh, interesting. Does your grader handle the case where some proofs are incomplete?

[Adam Topaz]

no, it's very rudimentary -- it just checks whether a term solution exists in the file Solution.lean, that it doesn't use axioms, and that the hash of the type of solution matches what's provided as an argument.

[Adam Topaz]

But to obtain solution from the environment it doesn't import anything, but rather actually compile the Solution.lean file.

[Adam Topaz]

Here's the precise line where the environment is obtained: https://github.com/adamtopaz/lean_grader/blob/78fdff947d45a161412debce6e1fa2779b5d628a/Main.lean#L18

[Rob Lewis]

Oh, cool -- I think that does work the way I need. Thanks very much!

[Adam Topaz]

Ha, I just noticed docs#Lean.Elab.process which should work just as well

[Mario Carneiro]

Yes, what Adam is suggesting is what I meant

[Scott Morrison]

@Rob Lewis you might like the frontend wrapper at https://github.com/semorrison/lean-training-data/blob/master/TrainingData/Frontend.lean. It gives you the Environment before and after every command, along with error messages (also syntax, source, info trees).

[Scott Morrison]

I'd like to upstream somewhere a nice frontend library that covers most people's needs. I'm not sure where that should actually be --- maybe just a top level library, or downstream of Std if that's helpful.

[Rob Lewis]

Thanks Scott, we'll take a look at that too -- I'm not sure we need something that fine-grained yet, but we might in the future

[Rob Lewis]

Once our autograder is more polished we'll make it public. It's a little more complex than Adam's, but tied to Gradescope instead of Github Classrooms