Check if variable (is|contains) sorry

Stream: lean4

[Cas Widdershoven]

Hi all, this may be a very simple question but I can't find a simple solution. In my code, I'm passed a Finset (for example) defined by a student, and before I do anything else with it I want to check if this object is sorry (or if its definition anywhere contains sorry), any idea how to do that? Thanks!

[Aaron Liu]

You can use #print axioms declName to see the axioms that declName depends on, if declName depends transitively on sorry then this list will contain docs#sorryAx.

[Cas Widdershoven]

Is there any way to do this in code? Instead of a command I'd like a term telling me whether the Finset is sorry, so that I can modify the program flow accordingly

[Aaron Liu]

there's docs#Lean.Expr.hasSorry but this doesn't transitively check the declarations used in the expression

[Aaron Liu]

there's also docs#Mathlib.PrintSorries.collectSorries

[Niels Voss]

Could you explain what you are trying to accomplish? It seems what you are trying to do is only possible at the meta level but its unclear if you are trying to use this information at the object level.

[Max Nowak 🐉]

You can look at the implementation of #print axioms ... to see how it collects the sorries, and probably call that yourself from a metaprogram.

[Mirek Olšák]

docs#Lean.collectAxioms

[Shreyas Srinivas]

Cas Widdershoven said:

Hi all, this may be a very simple question but I can't find a simple solution. In my code, I'm passed a Finset (for example) defined by a student, and before I do anything else with it I want to check if this object is sorry (or if its definition anywhere contains sorry), any idea how to do that? Thanks!

Hi Cas, essentially as others point out you need to do some metaprogramming to check this. I also don't think you actually ought to make such a check since you might end up with code you can't really prove anything about, because of potential calls to partial or unsafe functions.

[Shreyas Srinivas]

In general the editor will throw warnings if there are sorries anywhere

[Shreyas Srinivas]

(PS : Also, nice to meet you here again (MFoCS))

[Cas Widdershoven]

Hey Shreyas, nice to see you here, long time no see! Yeah, it seems like I'm going to need to do some metaprogramming. Based on everyone's comments (thanks a lot!) I've been trying to figure it out myself, but my lack of experience is showing and I was unable to get it to work properly.

Basically, my setup is as follows: I have a student-submitted file, "ex1.lean", which contains a "def q1 : Finset" which students are supposed to define. It is given to them as "sorry", and they should replace it with their own definition. I imported ex1 and tried passing ex1.q1 to my grader function as an argument q1, but I couldn't turn it into an Expr within that function using mkConst. However, I did figure out that I could use mkConst on ex1.q1 within the grader, and check hasSorry there. I did an if hasSorry - else on the resulting Expr, but still if I #eval! grader, it crashes complaining about (potential) reliance on sorry - I'm unsure how to solve this, any advice?

[Shreyas Srinivas]

I think you might want to look at the auto-grader tools mentioned in #Lean for teaching channel

[Shreyas Srinivas]

They would have already solved this problem

[Shreyas Srinivas]

Here : https://github.com/robertylewis/lean4-autograder-main

[Cas Widdershoven]

Yes, that's the one I'm using for another module I teach (and it's working well, for the most part!) but for this module I inherited a grading solution from last year, I'm just trying to increase its robustness so I don't have to filter out these things myself