"Complete formalized solutions" on dashboard

[mayorov-m-a]

Looks like I'll be the first user of this :)

I was just wondering if the discrepancy between what's reported on your dashboard as "complete formalized solution" vs actually complete solutions is intentional or not.
I saw the Imo2009P6 "grasshopper problem" and was intrigued that you have it marked as fully solved.
But the actual file that you have for it has 3 sorries and the proof depends on them(transitively).

I don't understand Lean metaprogramming that well to understand why the buildWebpage script works this way, but it does seem to check for sorries.

All in all, that's your choice of course, I just want to understand if this is intentional or not.

[dwrensha]

Good catch! That definitely should not be marked as complete.
The code that's supposed to detect whether a solution is complete is here:

compfiles/scripts/buildWebpage.lean

Line 353 in 6ac7969

if v.hasSorry then proved := false

We should find a better way to do that.

[dwrensha]

I think 3c2383c should fix it. Let me know if you see anything else that looks wrong.

[mayorov-m-a]

Yeah that looks like what I got by simply searching for "sorry".
The only one I don't agree with is 1992P6 which is now marked as incomplete because of native_decide.

[dwrensha]

Interesting! I didn't realize that native_decide was being used there. I think it's good to mark that as incomplete -- ideally we would not ever need to use native_decide.

I wonder if there's a more clear way that we can communicate the reason that this proof is not considered "complete".

[mayorov-m-a]

While we're at it I also noticed that the links in the "Open with the in-brower editor at live.lean-lang.org:" section don't work because of "%3A" in the generated urls(results in "Error: failed to load code from https%3A//dwrensha.github.io/compfiles/problems/Compfiles....lean")

I tried it with just a colon instead and it worked fine.

[dwrensha]

Thanks! I think this should fix it: fb739e3

[dwrensha]

And this removes the native_decide: 2d52f06