search

hhu-adam / Robo

A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪
https://adam.math.hhu.de
Apache License 2.0
16 stars 9 forks source link

The Web App runs into runtime exceptions constantly #56

Closed tautastic closed 1 month ago

tautastic commented 1 month ago

The page https://adam.math.hhu.de/#/g/hhu-adam/robo does not seem to work anymore.

Steps to reproduce:

  1. From the top right hamburger menu, erase your game data.
  2. Select the first level and continue to the level "Level 1 / 14 : Automatisierung".
  3. Solve the level by using tauto.
  4. You are redirected to a page that reads: "Oops! Sorry, an unexpected error has occurred. undefined has no properties" and the in the console several runtime errors are logged. Most of them are "TypeError: undefined has no properties".

I have tried this on several devices and browsers and this happend on all of them.

Another thing I noticed is that I can no longer open already solved levels. The behaviour from point 4 happens there too.

I am familiar with js, ts and react but I am not familiar with Lean nor do I know where the react code that runs into this problem is even located (I can't find any js or react code in this repo).

For me the game is currently unplayable because of the problems listed above.

tautastic commented 1 month ago

I just tested the Natural Number Game and ran into no problems at all there, still not sure where to start looking for the root of the problem or even a solution.

TentativeConvert commented 1 month ago

Thanks for the report! I can confirm the problem. Unfortunately, our developer @joneugster is on holiday at the moment, and our backup programmer will only start next week.

For the time being, perhaps you can try continuing the game on the development server? https://adam-dev.math.hhu.de/

Of course, there are reasons why the version of the software there is only on the development server. One of them is that every level will first give you an error message, but should be playable once you reload the page.

joneugster commented 1 month ago

I quick guess would be that somebody updated Robo on the main server with the newest development version, which wasn't ready yet.

I'll try to recover a working version of the game tonight or tomorrow.

tautastic commented 1 month ago

@joneugster So I checked the dev branch of leanprover-community/lean4game and https://github.com/leanprover-community/lean4game/commit/8e3dfdea30931aa275cc9ae780ea321092d90f1d (api.ts line 92) causes #57. If I build the stable branches of both lean4game and Robo locally and run them everything works fine.

As far as I can tell your guess seems to be correct.

joneugster commented 1 month ago

Should be fixed live