'constructor assumption' produces undefined state

[TentativeConvert]

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]

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