"uncaught exception: Challenge and solution constant kind don't match" is both unhelpful and untrue

[JasonGross]

I have identical files for challenge and solution:

def placeholder := @Eq.refl

I get

Building Challenge
Build completed successfully (3 jobs).
Exporting #[placeholder] from Challenge
Building Solution
Build completed successfully (3 jobs).
Exporting #[placeholder] from Solution
uncaught exception: Challenge and solution constant kind don't match: 'placeholder'

This error message doesn't actually tell me what is going wrong. But it seems like it should succeed in any case.

[JasonGross]

In fact I can't seem to get comparator to work on anything that is a def rather than a theorem

[hargoniX]

Yes, it currently only supports theorems as opposed to arbitrary constructs for simplicity. It's not quite clear what the comparison between challenge and solution should be for anything but a theorem IMHO.

Your PR at #5 would open up several additional issues. It only checks that the type of two things is the same. But is it for example enough to have the type of two inductive types match to consider one a solution? I don't know, maybe they should at least have the same constructors? Should the constructors have the same types or should they be allowed to contain sorries somewhere? If they have parameters/indices, should those be enforced to match? It's completely unclear to me. I would personally like to instead just print that anything but theorems is not supported.

[JasonGross]

It only checks that the type of two things is the same.

I see. That was indeed not my intention.

I would say that the following rule should be used in general:
the two terms must match exactly except at sorry, which should be treated as a wildcard.

[JasonGross]

What do you think of #7? (My main goal here is to permit challenges to build things informative things.)

[hargoniX]

Do I understand correctly that #7 basically extends the challenge/solution mechanism to also enforce replacing axioms with theorems if they are not on the allowed axiom list? That would seem like a conservative enough extension to me yes.

Note that the purpose of comparator is not to be a grading tool or anything like that. Its purpose is to be the program that tells you with as high certainty as possible whether you proved a theorem in Lean without any of the well known cheating methods out there.

[JasonGross]

Do I understand correctly that #7 basically extends the challenge/solution mechanism to also enforce replacing axioms with theorems if they are not on the allowed axiom list?

Not so much enforce as allow, but yes. And something on the allowed list which is listed as a theorem in the challenge is allowed to become an axiom in the solution. But the code is a bit misleading in that both Compare and Axioms do different checks on the solution constant kind, which is what led me to create #8 to solve this and other issues.

Note that the purpose of comparator is not to be a grading tool or anything like that. Its purpose is to be the program that tells you with as high certainty as possible whether you proved a theorem in Lean without any of the well known cheating methods out there.

Sure, though it's not clear to me what the difference is between "grading" and what you describe.