Do manual line buffering in Python

[simonlindholm]

This reduces the Python overhead by a factor ~5-10 (!). Previously when our program ran for like 10ms Python accounted for 30ms and made it difficult not to time out; now that becomes ~3-6ms.

Conflicts somewhat with #147, and makes #148 rather less important (though it's probably still a good idea).

[simonlindholm]

Oh, and I've tested this in both docker and nodocker on Linux, not on other OSes though (maybe Windows is weird with certain types of sockets).

[simonlindholm]

(Note that recv_socket.makefile('rwb', 1) only creates a line-buffered file object in Python 2; in Python 3 it changed semantics to have a buffer of size 1 instead. Which I guess you could technically still refer to as line buffered, but performance is abysmal.)