Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Level completed with warnings? #276

Open
Timmmm opened this issue Dec 27, 2024 · 2 comments · May be fixed by #305
Open

Level completed with warnings? #276

Timmmm opened this issue Dec 27, 2024 · 2 comments · May be fixed by #305
Labels
bug Something isn't working

Comments

@Timmmm
Copy link

Timmmm commented Dec 27, 2024

On this level I somehow managed to complete it, but it says "Level completed with warnings".

image

cases hxy with a ha
cases hyx with b hb
rw [ha] at hb
rw [← add_zero x] at hb
rw [add_comm] at hb
rw [add_comm (x 0)] at hb

Took me a few seconds but I found the underlined warning which says:

image

As far as I understand it that shouldn't really be an issue (I guess there's some reason for using sorry in that declaration), although it's weird that cases never gave me that warning before.

But also, I don't really understand how I can have solved the level... I was aiming for

0 + x = 0 + x + a + b
rw [add_comm, ...]
0 + x = a + b + 0 + x
apply add_right_cancel
0 = a + b + 0
rw [add_zero]
0 = a + b
(then I'm not sure but I guess it's possible to prove a = b = 0 from here)

But I didn't actually do any of that - Lean never did that many steps for me automatically before..

The thing that is definitely a bug though, is that it says Level complete but Next is still greyed out.

image

@joneugster
Copy link
Collaborator

This is because rw [add_comm (x 0)] at hb produces a parsing error and unfortunately the way Lean and the Game report this is not ideal.

The solution for you is to omit the () since right now, you are trying to apply x (as a function) to 0, which is obviously not right. instead use add_comm x 0.

It's not uncommon that Lean introduces a sorry on parsing errors to avoid a total crash, but we should look into where the error message was lost and why it's not displayed to the user.

@joneugster
Copy link
Collaborator

The action here is: Treat the sorry warning as an error.

@joneugster joneugster added the bug Something isn't working label Jan 25, 2025
tautastic added a commit to tautastic/lean4game that referenced this issue Feb 26, 2025
tautastic added a commit to tautastic/lean4game that referenced this issue Feb 26, 2025
@tautastic tautastic linked a pull request Feb 26, 2025 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants