Transition to ndjson export format #10
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
hargoniX
reviewed
Jan 7, 2026
format_ndjson.md
Outdated
| Expr.lit (Literal.strVal) | ||
| ``` | ||
| { | ||
| "lit": { |
Contributor
There was a problem hiding this comment.
This does not seem to be what your program currently actually prints?
| .lit (.natVal i) => return .mkObj [("natVal", s!"{i}")]
| .lit (.strVal s) => return .mkObj [("strVal", s)]
Contributor
Author
There was a problem hiding this comment.
Thanks, I've pushed a correction for the format specification.
hargoniX
reviewed
Jan 7, 2026
format_ndjson.md
Outdated
| "levelParams": Array<integer>, | ||
| "type": integer, | ||
| "value": integer, | ||
| "hints": Array<"opaque" | "abbrev" | integer> |
Contributor
There was a problem hiding this comment.
This is also incorrectly documented afaict?
Corrects two errors in the format specification for string literals and reducibility hints.
hargoniX
reviewed
Jan 7, 2026
Correct a typo of `deBruijnIndex`
nomeata
reviewed
Jan 8, 2026
Contributor
Author
|
The open comments should be resolved, and I believe I addressed the remaining points in #10 |
+ Namespaces backreferences from a generic "i" to "in", "il", and "ie" for name, level, and expr. + Abbreviates some json attribute names
|
Thanks! (Seeing how slow lean4export is I’m inclined to rewrite the exporter to use simple string interpolation into hardcoded JSON lines, at least for everything that only contains numbers, but that can wait until other dust has settled.) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
When ready, will close #3 (also see that issue for relevant discussion).
The format is described in
format_ndjsonand the README has been updated accordingly, along with the recommended command for invocation; the old README recommended invokinglake exe, which will not correctly set up the lake env in the most common use case, something like exporting mathlib.