disappearing text in tutorial world entry page

[kbuzzard]

This has taken a while to pin down, and now I've pinned it down I don't have any understanding of what's going on. The comments below pertain to the debug branch of NNG4 which I made just to showcase this issue.

Uncommenting this line here in the file Game/Levels/Addition/L01zero_add.lean for some reason makes the text from this page magically stop appearing on the intro page to tutorial world http://localhost:3000/#/g/hhu-adam/NNG4/world/Tutorial/level/0 .

So for whatever reason, this import is bad. But I want add_zero and add_succ in addition world! What have I done wrong? Can anyone else reproduce? Go to the debug branch, compile, note that the intro to tutorial world has the text "Welcome to tutorial world! In this world we learn the basics of proving theorems. The boss level of this world is the theorem 2 + 2 = 4...." on the web page, then uncomment out the import, compile again, and the text is gone.

[kbuzzard]

Somehow I have add_zero and add_succ in addition world anyway, without the import.

I think a summary of this issue is: I have no idea why adding the import as explained above causes problems. On the other hand I know how to work around it: it seems that I can just never import tutorial world at all, and just redefine stuff like one_eq_succ_zero a second time in another file and import that instead. So this is no longer blocking me but it's still pretty weird.

[joneugster]

This is a known bug: You must not import a particular level of a different world, only entire worlds. (i.e. Game.Levels.Tutorial instead of Game.Levels.Tutorial.L05add_succ)

leanprover-community/lean4game/issues/60

PS: add_zero and add_succ are defined in Game.MyNat.Addition which is explicitely imported in the file linked, so that seems as expected.