Parsing JSON with comments

Stream: general

[Michael Rothgang]

Is there a Lean way to parse JSON with comments? (Use case: for mathlib's directoryDependency linter, I'd like to convert a big list of exceptions from a manually defined map to a .json file. However, the source file has comments above some entries, which I'd like to keep.)

[Ruben Van de Velde]

JSON with comments isn't JSON :)

[Kevin Buzzard]

There's no such thing as a JSON file with comments.

[Kevin Buzzard]

Just make a _comment field in your JSON file or something?

[Eric Taucher]

Kevin Buzzard said:

There's no such thing as a JSON file with comments.

That is correct, JSON does not support comments.

A very popular alternative Yet Another Markup Language (YAML), does support comments.

What’s the Difference Between YAML and JSON?

One specification that uses both JSON and YAML is OpenAPI spec where the files can be distributed as either JSON or YAML. Many developers choose YAML so that comments can be added.

[Michael Rothgang]

There is a certainly "JSON with comments", a common JSON extension --- but fair point, I'll use a small hack then.

[Michael Rothgang]

Using yaml is not an option for me --- because Lean doesn't have a parser for. This is for good reasons, yaml has lots of subtle gotchas.

[Eric Wieser]

Can you use TOML?

[Michael Rothgang]

Sure, that should also work.

[Michael Rothgang]

(I was thinking of "a .json file, but lines starting with (whitespace and) // are removed before parsing". I don't have a strong opinion either way.)

[Eric Wieser]

It would certainly be nice to support that, but there's already toml used in the lean ecosystem, so if you get to choose your own format that might be a good path.

[Ruben Van de Velde]

So no end of line comments? I tend to recommend against using custom formats that are almost but not quite standard

[Alex Meiburg]

JSON with comments exists in the same way that a Group With (Absorbing) Zero exists. :)

[Alex Meiburg]

(it's well-defined, used, and just happens to - as an artifact of English - not actually be a proper hyponym)

[James Sully]

Michael Rothgang said:

(I was thinking of "a .json file, but lines starting with (whitespace and) // are removed before parsing". I don't have a strong opinion either way.)

Maybe you could just manually strip them out as a preprocessing step

[Jz Pan]

Maybe you can try hjson https://hjson.github.io/

[Kyle Miller]

James Sully said:

Maybe you could just manually strip them out as a preprocessing step

Annoyingly strings can contain //. I'm not sure there's any robust way to handle comments by preprocessing.

[Michael Rothgang]

In my case, all strings are mathlib module names, which don't contain slashes - so for my use case, a small hack would be fine. (Or using toml.)

[James Sully]

only allowing comments on their own lines simplifies things as well

[Joscha Mennicken]

Aside from YAML, JSONC, and HJSON, there's even more JSON super sets with comments: JSON5 and HOCON