Optimize how user options are delivered to the client

Optimize how user options are delivered to the client

We currently embed the full set of user options in a <script> tag in the HTML
output of every page. This is grossly inefficient, because the full set of
options is usually largely made up of site defaults which the user hasn't
customized.

So instead of doing that, let's emit the default options using one
ResourceLoader module and then apply the user's customizations on top.

This has the effect of slightly increasing the total bytes of JavaScript code
(because options that the user has customized will be emitted twice: once with
their default value in the user.defaults module, and then again with the
customized value in user.options). But this is more than offset by the
fact that the bulk of user options code (~4 kB uncompressed on enwiki) becomes
cacheable across requests.

Bonus round:
* Varnish gets to cache 4 kB fewer per page.
* Changes to the default options don't take 30 days to propagate.

Change-Id: I5a7e258d2d69159381bf5cc363227088b8fd6019