Crashing NNG4: "Cannot read properties of undefined"

Stream: new members

[Isak Colboubrani]

Doing the following crashes NNG4 for me. Anyone able to reproduce?

Go to https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/Multiplication/level/3

Run:

induction b
repeat rw [mul_zero]
rw [add_zero]
rfl
repeat rw [mul_succ]
rw [n_ih]
repeat rw [add_right_comm]

Error message:

Oops!
Sorry, an unexpected error has occurred.
Cannot read properties of undefined (reading 'steps')

[Kevin Buzzard]

I should think that repeat rw [add_right_comm] would crash anything, no?

[Isak Colboubrani]

To make that clear: I fully understand why repeat rw [add_right_comm] is not a wise move to make :sweat_smile:

I expected a normal error message saying something along the lines of maximum recursion depth has been reached or similar. Not that the game would hard crash and be stuck in a crashing state even after reloading.

I thought it was a bug worth reporting. I really like the game!

[Kevin Buzzard]

Yeah this came up recently. I don't know if it's a regression or whether they just put something in the global water supply to make people do repeat rw (involution) more. If the game is now unusable for you on that level then I'm afraid the only fix right now is to download the savefile and manually edit it.

[Kevin Buzzard]

Finally at a computer. Yeah it's the same issue. I think Jon has a fix for this in the works. Until then I think you have to save, delete the bad lemma (or just the line that loops) and then load. Sorry for the inconvenience!

[Isak Colboubrani]

Ah, no worries for me! I wasn't really blocked by this issue. I quickly fixed my game session by extracting the game_progress JSON from local storage and then running the following command:

json_pp < game_progress.json | sed 's/repeat rw \[add_right_comm\]/sorry/g'

After that, I re-imported the resulting JSON into local storage again using the game_progress key. Problem solved!

[Jon Eugster]

I'll see that I'll push a fix for this first thing monday morning!