feat: JSON format parser

[hargoniX]

Parser for the new JSON format proposed in #10.

TODOs:

• Some nice tests (manually tested that it parses the example ndjson file)
• figure out how to do mdata properly

[ammkrn]

The thing about the semver value just being a definition in Main.lean was mentioned in the issue, it seems like the conclusion was that it's not really possible to reference the version parameter in the lakefile from within the program. I don't have much experience with the latest linter/script stuff but if possible, it would probably be wise to have something to ensure that semver value stays up to date.

[nomeata]

Doesn’t quite work for me yet. I am getting

uncaught exception: offset 27145: Expr.letE 357 invalid

when running on a Init.Prelude export, and

uncaught exception: offset 7483: axiomInfo invalid

when running on all of Init. (Maybe independent issues, and just depend on which one occurs first.)

A peek at the file and the code doesn’t tell me what’s wrong, though.

In
init-prelude.ndjson.gz
the problematic line is

{"i":357,"letE":{"body":356,"declName":73,"nondep":true,"type":308,"value":347}}

ah, it says declName and type rather than binderName and binderType as expected by the parser.

Ah, and the other issue is with opaqueInfo not axiomInfo (wrong message), and the exporter is missing the isUnsafe field. Reported at #10 (review)

[nomeata]

Suggested change

	let value ← getExpr bodyIdx
	let value ← getExpr valueIdx