Choose a better config file format, to include comments

Each of our servers, plus the `dump` tool, has a config file; at the moment all of these are JSON, which doesn't allow any comments, and in practice hand-writing `core/dump_spec.json` is very tedious and error-prone.

I think we should change to a different config file format. Ether some kind of less-strict JSON that allows more JavaScript-like syntax (e.g., `{foo: 'bar'}` instead of only `{"foo": "bar"}` and comments, or something else that's even simpler to write like YAML.

Considerations:

* The main goals are to make documenting config files possible and hand-writing them easier.
* Since `dump` has the most complex configuration needs, it should probably guide the choice of format.
* Sticking with something that is backwards-compatible with JSON would mean there was no need to change existing config files, and auto-generating dump specs would not require any extra tooling.