Bug: Web server hangs indefinitely on final tactic application in "First Real Limit" (Level 2/2)

[yunjiangster]

In Lecture 3, Level 2/2 ("First Real Limit"), the background Lean server appears to hang or enter an infinite loop when applying the final tactic to close the goal. Instead of returning a success message or a tactic failure, the UI gets stuck in a loading state and requires a full page refresh to recover.

[joneugster]

thanks for the report. Do you get a completed level on page reload? or a failure?

[yunjiangster]

Thanks for the quick reply. Even with reload (multiple attempts) it still hangs. If you have the official solution I can give it a try.

[joneugster]

You could paste a link to the specific level together with the entire code, you get when you toggle to "editor mode" (button in the image), that would help reproducing. Most likely it's because your previous line fails (message about aesop not succeeding) but the error isn't displayed. There's an entire stack of issues which are probably all related: #400, #395, #402, ...

[yunjiangster]

Looks like this step has a syntax error

but the interactive UI did not indicate any error.

Only in the edit mode do I see a hint of issue. To be honest I still don't know why ring_nf doesn't work at that line.

[joneugster]

ok so this is a duplicate of #373 then? Thanks for the new bug report on this, I couldn't reproduce that error some time ago.

On a Lean level, ring/ring_nf solves equalities which can be solved by purely algebraic manipulations, e.g. reorganising addition & multiplication, like 2 * a + b = b + a + a. But here there is nothing like that. I'd assume linarith [hN] should work for you.

[yunjiangster]

ok so this is a duplicate of #373 then? Thanks for the new bug report on this, I couldn't reproduce that error some time ago.

On a Lean level, ring/ring_nf solves equalities which can be solved by purely algebraic manipulations, e.g. reorganising addition & multiplication, like 2 * a + b = b + a + a. But here there is nothing like that. I'd assume linarith [hN] should work for you.

Yes that's exactly the same error. I believe the RealAnalysisGame server is still using an older code version. For instance, the abs_add theorem has been updated to abs_add_le in the latest version. But it would be interesting to know which PR fixed the issue.