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

'constructor assumption' produces undefined state #21

Open TentativeConvert opened 4 months ago

TentativeConvert commented 4 months ago

I've reproduced this in Robo/Logo/Level 14: Enter constructor assumption as the first command. You will get no feedback. You can keep entering further arbitrary commands, and they will simply get listed one after the other, without any feedback or proof states in between.

joneugster commented 4 months ago

I think the underlying issue here is that we don't handle server (Lean) crashes correctly, so some error messages never reach the client.