document interactions with coqtop
interactions with coqtop are complex and lead to some annoying bugs (sometimes).
coqtop is run in parallel to coquille. A user interaction can lead to more than one action sent to coqtop, and actions are queued before being sent to coqtop for evaluation. Some actions will act on that queue, require coqtop to be in a specific state, etc.
de-synchronisation happens too often, so something must be done.
I need to understand better what coqtop expects from the plugin, what is allowed and what is not. This should lead to a better implementation and testable assumptions!
Scenarios:
- The command ends successfully
- The command ends with an error
- The command doesn't end
On every scenario, what happens if we let them be, and what happens if we send an interrupt in the middle (check for every position an interrupt can be sent; especially before and after answers from coqtop).