Zulip Chat Archive
Stream: metaprogramming / tactics
Topic: comparing declarations across environments
Rob Lewis (Oct 04 2024 at 14:48):
I have an autograder for checking student homework assignments written in Lean. Proofs are easy: check that the declaration's type matches what we expect and that the body doesn't contain any disallowed axioms. Checking definitions is harder (theoretically undecidable and technically more complicated). To check a student's definition defProblem, we want to do something like, take the body submission of the student's definition, the body reference of our solution, set up a goal submission = reference, and try to prove it with some custom tactic.
But we need to choose an environment in which to set up this goal. And since either or both definitions may refer to aux declarations (generated or user defined), we can't assume that either environment is an extension of the other. Even worse the two solutions could refer to different aux declarations with the same name. So the naive approach of just copying submission into the environment of reference fails unless the definitions are reasonably simple. (This isn't just hypothetical, we hit it very quickly.)
The way I can see to fix this is to recursively copy submission into the reference environment, renaming any name conflicts that aren't defeq to the existing versions. We'd also have to copy equational lemmas if we want to use simp to discharge goals.
This sounds moderately annoying so I wanted to ask if anyone had a better idea, or existing work that does this kind of environment embedding. It sounds somewhat similar to some of the stuff that happened in the Lean 3 -> Lean 4 port (@Mario Carneiro ?)
Mario Carneiro (Oct 04 2024 at 14:50):
Why not just make the reference implementation live inside a __NoStudentWillGuessThis namespace
Mario Carneiro (Oct 04 2024 at 14:51):
you can probably also use hygienic names by putting it all in a macro
Rob Lewis (Oct 04 2024 at 14:55):
Mario Carneiro said:
Why not just make the reference implementation live inside a
__NoStudentWillGuessThisnamespace
Hmm, yeah, that would solve the name clash problem. Right now the autograder assumes solution and submission names line up so it introduces an alignment issue but that's easy enough to handle.
Mario Carneiro (Oct 04 2024 at 14:56):
I mean they can't have the same name otherwise you would have a name clash
Mario Carneiro (Oct 04 2024 at 14:56):
like you wrote submission = reference and not submission = submission
Rob Lewis (Oct 04 2024 at 14:57):
Right now we aren't actually creating a new declaration when we copy submission over, we just take the body
Mario Carneiro (Oct 04 2024 at 14:57):
so it's more like submission = <body of reference>?
Rob Lewis (Oct 04 2024 at 14:57):
Right
Rob Lewis (Oct 04 2024 at 14:58):
Or maybe even <body of submission> = <body of reference>
Mario Carneiro (Oct 04 2024 at 14:58):
if the autograder knows about the __NoStudentWillGuessThis namespace you can use name coincidences with and without it to form your alignment, so the only thing you have to do to mark the reference side is to add a namespace __NoStudentWillGuessThis at the top of the file
Mario Carneiro (Oct 04 2024 at 14:59):
you may even be able to do it automatically
Rob Lewis (Oct 04 2024 at 15:01):
Yeah. The medium term goal for this is to have a package for people teaching with Lean, and I don't love that interface. It's easy to forget and not even necessary if you're only checking proofs. But we can probably find a way to make it manageable
Mario Carneiro (Oct 04 2024 at 15:01):
if you do it automatically then it won't be a problem
Mario Carneiro (Oct 04 2024 at 15:02):
except that maybe some stuff breaks if you put it in a namespace; best to report this early on the reference file
Rob Lewis (Oct 04 2024 at 15:02):
What do you mean by doing it automatically?
Mario Carneiro (Oct 04 2024 at 15:03):
the autograder takes the reference file and edits it to add the namespace line before processing it to get an environment
Rob Lewis (Oct 04 2024 at 15:03):
Ah, editing the source file
Mario Carneiro (Oct 04 2024 at 15:04):
you could also modify the toplevel but that seems somewhat heavyweight
Rob Lewis (Oct 04 2024 at 15:09):
This could even simplify the implementation. If we namespace the entire reference file, we can just build an environment that imports both the submission and the reference without any name clashes
Rob Lewis (Oct 04 2024 at 15:09):
So no recursive copying needed, no trickery to figure out what equational lemmas we need
Mario Carneiro (Oct 04 2024 at 15:09):
exactly
Rob Lewis (Oct 04 2024 at 15:10):
This sounds slightly uglier but much easier than what I was imagining. Thanks!
Rob Lewis (Oct 04 2024 at 15:11):
I wonder how much we expect to break in practice by namespacing an entire file
Mario Carneiro (Oct 04 2024 at 15:11):
Not too much, I think the main culprit will be _root_ references but I wouldn't expect to see much of that in an instructor-written solution file
Rob Lewis (Oct 04 2024 at 15:13):
One occurrence in last year's homeworks :grinning:
Mario Carneiro (Oct 04 2024 at 15:13):
luckily you only have to worry about hacks in the instructor's file and not the student's
Jireh Loreaux (Oct 04 2024 at 15:13):
Also dot notation could break. E.g., if you add a List.foo lemma, and then later in the file call l.foo on l : List α.
Mario Carneiro (Oct 04 2024 at 15:16):
seems hygienic namespaces don't work:
macro "open_foo" : command => `(command| namespace Foo)
open_foo -- invalid scope
not that I'm surprised, because namespaces have to be concatenated as name components and hygiene makes use of that for storing additional information
Rob Lewis (Oct 04 2024 at 15:19):
A potential hiccup: student submissions may have build errors, in particular incomplete proofs. (We can assume solutions build.) This will block us from creating a merge file that imports both, won't it?
Mario Carneiro (Oct 04 2024 at 16:11):
You can also fix that by editing, just insert an import of the instructor's file at the top of the student's and insert a line at the end which calls your checker
Mario Carneiro (Oct 04 2024 at 16:12):
or override the toplevel to process each command, which gives you more control to handle failures as appropriate
Last updated: May 02 2025 at 03:31 UTC