I was reading some code today and I suddenly realized that Resources.php in MediaWiki code is indeed a PHP file, instead of a JSON file, unlike almost all ResourceLoader module definitions in almost all extensions.

Is there a reason for this, or is it simply because no one has changed it yet? (It looks like it might be slightly tricky to change, because the JSON definitions loading is tied to loading extensions…)