Using docker results in errors due to rate limit on pulling, so try to
reduce its use as much as possible. It still has to be used under Ubuntu
14.04 because it has a version of Python too old to work with HTTPS
servers using SNI and so using pip fails there.