performance
When proving a subgoal with a lot of unfocused subgoals, it seems that the python process can take more CPU that coqtop itself, making it noticeably slower to evaluate the first subgoal than the last. One part of the performance issue can be explained by logging, but it doesn't seem to be the only issue.
Another part of the problem may be caused by attempting to decode coqtop's answer before it is complete. Since it is longer when there are more unfocused subgoals, there will be more attempts to decode it than when there is no other subgoal.
Edited by Julien Lepiller