As suggested in #7435 and various other places, we should move from our "homegrown" JSON parser to yojson.