Transition to ndjson export format by ammkrn · Pull Request #10 · leanprover/lean4export

ammkrn · 2026-01-01T09:07:01Z

When ready, will close#3 (also see that issue for relevant discussion).

The format is described in format_ndjson and the README has been updated accordingly, along with the recommended command for invocation; the old README recommended invoking lake exe, which will not correctly set up the lake env in the most common use case, something like exporting mathlib.

hargoniX · 2026-01-07T13:30:44Z

+Expr.lit (Literal.strVal)
+```
+{
+ "lit": {


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)]

Thanks, I've pushed a correction for the format specification.

hargoniX · 2026-01-07T14:45:44Z

+ "levelParams": Array<integer>,
+ "type": integer,
+ "value": integer,
+ "hints": Array<"opaque" | "abbrev" | integer>


This is also incorrectly documented afaict?

Corrects two errors in the format specification for string literals and reducibility hints.

Correct a typo of `deBruijnIndex`

ammkrn · 2026-01-09T16:13:08Z

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

nomeata · 2026-01-09T16:35:24Z

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.)

Modifies the export procedure and format to export the components of an inductive declaration (the inductive specification(s), constructors, and recursors) together. Consumers are generally going to want to find these related declarations anyway, and with the introduction of the auxiliary `.rec_<N>` recursors motivated by nested inductive support, (in my opinion) this is a more comprehensible format.

ammkrn · 2026-01-13T14:29:54Z

I've added one commit 50db814 to implement the change mentioned elsewhere, packaging related elements of an inductive declaration.

nomeata · 2026-01-13T14:42:57Z

Great! Are declarations now following the Lean.Declaration type consistently, so that a lean-using importer can parse to that type directly?

Hmm, it seems we now have a somewhat odd mix of Lean.Declaration and Lean.ConstantInfo. But if its a “best of both worlds” mix it’s maybe fine?

ammkrn · 2026-01-13T15:01:25Z

Great! Are declarations now following the Lean.Declaration type consistently, so that a lean-using importer can parse to that type directly?
Hmm, it seems we now have a somewhat odd mix of Lean.Declaration and Lean.ConstantInfo. But if its a “best of both worlds” mix it’s maybe fine?

I'm not sure how one would be able to parse anything directly regardless of format since (a) we're using integer pointers and (b) it was already suggested that we make simplifying cuts that would prevent direct parsing, like removing "deBruijnIndex" and changing "binderName".

Lean.Declaration only includes what's strictly necessary for a "full" kernel implementation to do the work of type checking; for example it expects the consumer to both construct and check recursors. The very first exporter implementation followed that pattern.

In the previous round of format changes, it was decided that the exporter should include additional information (like "targets" for the recursors and rec rules, Eq/Quot declarations, etc.). With this additional info it's much easier to bootstrap new checkers, implement certain memory optimizations, and have things like parallel checkers.

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.

nomeata · 2026-01-13T15:22:08Z

I didn’t mean “parse generically”, but I meant “parse export to List Lean.Declaration” (so field name changes or indirections are not a blocker).

But thanks for the historical perspective, agreed on that count.

nomeata · 2026-01-15T12:24:36Z

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.

These are always ever unsafe, so not of high importance here? But in principle you are right.

Exports elements of mutual theorem and def/opaque blocks together.

ammkrn · 2026-01-15T16:50:45Z

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.
These are always ever unsafe, so not of high importance here? But in principle you are right.

Should be done in 7188ec9 modulo style issues.

nomeata · 2026-01-15T17:13:22Z

Am I reading this right that it doesn't distinguish between a normal definition and a singly-recursive definition? It seems that of that's the case, import information is lost. I assume that's why Lean.Declaration is explicit in where the mutual groups are. But maybe lean forgets that information so it's hard to reproduce the declaration here?

nomeata · 2026-01-15T17:25:16Z

Hmm, the Kernel certainly doesn’t seem to remember whether a declaration came from a .mutualDefnDecl or not, so by the time we have a ConstantInfo this information is lost.

Ah! But the kernel treats any unsafe declaration as recursive, even if not in a mutual block. Odd. But not partial declarations.

I find it confusing.

In any case, I think I’m leaning towards an export format that more closely matches Lean.Declaration here, and with a dedicated .mutual tag that is only used when Lean.Declaration.mutualDefnDecl would be used (namely when its unsafe or partial and all is not a singleton). This way parsers for checkers who do not support this can just skip the whole line. But I don't feel strongly about it.

ammkrn · 2026-01-15T18:20:29Z

In any case, I think I’m leaning towards an export format that more closely matches Lean.Declaration here, and with a dedicated .mutual tag that is only used when Lean.Declaration.mutualDefnDecl would be used (namely when its unsafe or partial and all is not a singleton). This way parsers for checkers who do not support this can just skip the whole line. But I don't feel strongly about it.

I have no issue with that. To the earlier question, I think examination of all (specifically whether there's more than one name in there) would be the context clue.

Adds a separate metadata field for the format version, since it's not necessarily the same as the exporter version. For example a performance fix in the exporter might justify an exporter version bump, but not a format version bump.

Tries to export `Nat` on the appearance of a nat literal, and Char.ofNat and String.ofList on the appearance of a string literal.

ammkrn · 2026-01-01T09:07:01Z

When ready, will close#3 (also see that issue for relevant discussion).

The format is described in format_ndjson and the README has been updated accordingly, along with the recommended command for invocation; the old README recommended invoking lake exe, which will not correctly set up the lake env in the most common use case, something like exporting mathlib.

hargoniX · 2026-01-07T13:30:44Z

+Expr.lit (Literal.strVal)
+```
+{
+ "lit": {


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)]

Thanks, I've pushed a correction for the format specification.

hargoniX · 2026-01-07T14:45:44Z

+ "levelParams": Array<integer>,
+ "type": integer,
+ "value": integer,
+ "hints": Array<"opaque" | "abbrev" | integer>


This is also incorrectly documented afaict?

Corrects two errors in the format specification for string literals and reducibility hints.

Correct a typo of `deBruijnIndex`

ammkrn · 2026-01-09T16:13:08Z

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

nomeata · 2026-01-09T16:35:24Z

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.)

Modifies the export procedure and format to export the components of an inductive declaration (the inductive specification(s), constructors, and recursors) together. Consumers are generally going to want to find these related declarations anyway, and with the introduction of the auxiliary `.rec_<N>` recursors motivated by nested inductive support, (in my opinion) this is a more comprehensible format.

ammkrn · 2026-01-13T14:29:54Z

I've added one commit 50db814 to implement the change mentioned elsewhere, packaging related elements of an inductive declaration.

nomeata · 2026-01-13T14:42:57Z

Great! Are declarations now following the Lean.Declaration type consistently, so that a lean-using importer can parse to that type directly?

Hmm, it seems we now have a somewhat odd mix of Lean.Declaration and Lean.ConstantInfo. But if its a “best of both worlds” mix it’s maybe fine?

ammkrn · 2026-01-13T15:01:25Z

Great! Are declarations now following the Lean.Declaration type consistently, so that a lean-using importer can parse to that type directly?
Hmm, it seems we now have a somewhat odd mix of Lean.Declaration and Lean.ConstantInfo. But if its a “best of both worlds” mix it’s maybe fine?

I'm not sure how one would be able to parse anything directly regardless of format since (a) we're using integer pointers and (b) it was already suggested that we make simplifying cuts that would prevent direct parsing, like removing "deBruijnIndex" and changing "binderName".

Lean.Declaration only includes what's strictly necessary for a "full" kernel implementation to do the work of type checking; for example it expects the consumer to both construct and check recursors. The very first exporter implementation followed that pattern.

In the previous round of format changes, it was decided that the exporter should include additional information (like "targets" for the recursors and rec rules, Eq/Quot declarations, etc.). With this additional info it's much easier to bootstrap new checkers, implement certain memory optimizations, and have things like parallel checkers.

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.

nomeata · 2026-01-13T15:22:08Z

I didn’t mean “parse generically”, but I meant “parse export to List Lean.Declaration” (so field name changes or indirections are not a blocker).

But thanks for the historical perspective, agreed on that count.

nomeata · 2026-01-15T12:24:36Z

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.

These are always ever unsafe, so not of high importance here? But in principle you are right.

Exports elements of mutual theorem and def/opaque blocks together.

ammkrn · 2026-01-15T16:50:45Z

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.
These are always ever unsafe, so not of high importance here? But in principle you are right.

Should be done in 7188ec9 modulo style issues.

nomeata · 2026-01-15T17:13:22Z

Am I reading this right that it doesn't distinguish between a normal definition and a singly-recursive definition? It seems that of that's the case, import information is lost. I assume that's why Lean.Declaration is explicit in where the mutual groups are. But maybe lean forgets that information so it's hard to reproduce the declaration here?

nomeata · 2026-01-15T17:25:16Z

Hmm, the Kernel certainly doesn’t seem to remember whether a declaration came from a .mutualDefnDecl or not, so by the time we have a ConstantInfo this information is lost.

Ah! But the kernel treats any unsafe declaration as recursive, even if not in a mutual block. Odd. But not partial declarations.

I find it confusing.

In any case, I think I’m leaning towards an export format that more closely matches Lean.Declaration here, and with a dedicated .mutual tag that is only used when Lean.Declaration.mutualDefnDecl would be used (namely when its unsafe or partial and all is not a singleton). This way parsers for checkers who do not support this can just skip the whole line. But I don't feel strongly about it.

ammkrn · 2026-01-15T18:20:29Z

In any case, I think I’m leaning towards an export format that more closely matches Lean.Declaration here, and with a dedicated .mutual tag that is only used when Lean.Declaration.mutualDefnDecl would be used (namely when its unsafe or partial and all is not a singleton). This way parsers for checkers who do not support this can just skip the whole line. But I don't feel strongly about it.

I have no issue with that. To the earlier question, I think examination of all (specifically whether there's more than one name in there) would be the context clue.

Adds a separate metadata field for the format version, since it's not necessarily the same as the exporter version. For example a performance fix in the exporter might justify an exporter version bump, but not a format version bump.

Tries to export `Nat` on the appearance of a nat literal, and Char.ofNat and String.ofList on the appearance of a string literal.

ammkrn · 2026-01-01T09:07:01Z

When ready, will close#3 (also see that issue for relevant discussion).

The format is described in format_ndjson and the README has been updated accordingly, along with the recommended command for invocation; the old README recommended invoking lake exe, which will not correctly set up the lake env in the most common use case, something like exporting mathlib.

hargoniX · 2026-01-07T13:30:44Z

+Expr.lit (Literal.strVal)
+```
+{
+ "lit": {


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)]

Thanks, I've pushed a correction for the format specification.

hargoniX · 2026-01-07T14:45:44Z

+ "levelParams": Array<integer>,
+ "type": integer,
+ "value": integer,
+ "hints": Array<"opaque" | "abbrev" | integer>


This is also incorrectly documented afaict?

Corrects two errors in the format specification for string literals and reducibility hints.

Correct a typo of `deBruijnIndex`

ammkrn · 2026-01-09T16:13:08Z

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

nomeata · 2026-01-09T16:35:24Z

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.)

Modifies the export procedure and format to export the components of an inductive declaration (the inductive specification(s), constructors, and recursors) together. Consumers are generally going to want to find these related declarations anyway, and with the introduction of the auxiliary `.rec_<N>` recursors motivated by nested inductive support, (in my opinion) this is a more comprehensible format.

ammkrn · 2026-01-13T14:29:54Z

I've added one commit 50db814 to implement the change mentioned elsewhere, packaging related elements of an inductive declaration.

nomeata · 2026-01-13T14:42:57Z

Great! Are declarations now following the Lean.Declaration type consistently, so that a lean-using importer can parse to that type directly?

Hmm, it seems we now have a somewhat odd mix of Lean.Declaration and Lean.ConstantInfo. But if its a “best of both worlds” mix it’s maybe fine?

ammkrn · 2026-01-13T15:01:25Z

Great! Are declarations now following the Lean.Declaration type consistently, so that a lean-using importer can parse to that type directly?
Hmm, it seems we now have a somewhat odd mix of Lean.Declaration and Lean.ConstantInfo. But if its a “best of both worlds” mix it’s maybe fine?

I'm not sure how one would be able to parse anything directly regardless of format since (a) we're using integer pointers and (b) it was already suggested that we make simplifying cuts that would prevent direct parsing, like removing "deBruijnIndex" and changing "binderName".

Lean.Declaration only includes what's strictly necessary for a "full" kernel implementation to do the work of type checking; for example it expects the consumer to both construct and check recursors. The very first exporter implementation followed that pattern.

In the previous round of format changes, it was decided that the exporter should include additional information (like "targets" for the recursors and rec rules, Eq/Quot declarations, etc.). With this additional info it's much easier to bootstrap new checkers, implement certain memory optimizations, and have things like parallel checkers.

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.

nomeata · 2026-01-13T15:22:08Z

I didn’t mean “parse generically”, but I meant “parse export to List Lean.Declaration” (so field name changes or indirections are not a blocker).

But thanks for the historical perspective, agreed on that count.

nomeata · 2026-01-15T12:24:36Z

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.

These are always ever unsafe, so not of high importance here? But in principle you are right.

Exports elements of mutual theorem and def/opaque blocks together.

ammkrn · 2026-01-15T16:50:45Z

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.
These are always ever unsafe, so not of high importance here? But in principle you are right.

Should be done in 7188ec9 modulo style issues.

nomeata · 2026-01-15T17:13:22Z

Am I reading this right that it doesn't distinguish between a normal definition and a singly-recursive definition? It seems that of that's the case, import information is lost. I assume that's why Lean.Declaration is explicit in where the mutual groups are. But maybe lean forgets that information so it's hard to reproduce the declaration here?

nomeata · 2026-01-15T17:25:16Z

Hmm, the Kernel certainly doesn’t seem to remember whether a declaration came from a .mutualDefnDecl or not, so by the time we have a ConstantInfo this information is lost.

Ah! But the kernel treats any unsafe declaration as recursive, even if not in a mutual block. Odd. But not partial declarations.

I find it confusing.

In any case, I think I’m leaning towards an export format that more closely matches Lean.Declaration here, and with a dedicated .mutual tag that is only used when Lean.Declaration.mutualDefnDecl would be used (namely when its unsafe or partial and all is not a singleton). This way parsers for checkers who do not support this can just skip the whole line. But I don't feel strongly about it.

ammkrn · 2026-01-15T18:20:29Z

In any case, I think I’m leaning towards an export format that more closely matches Lean.Declaration here, and with a dedicated .mutual tag that is only used when Lean.Declaration.mutualDefnDecl would be used (namely when its unsafe or partial and all is not a singleton). This way parsers for checkers who do not support this can just skip the whole line. But I don't feel strongly about it.

I have no issue with that. To the earlier question, I think examination of all (specifically whether there's more than one name in there) would be the context clue.

Adds a separate metadata field for the format version, since it's not necessarily the same as the exporter version. For example a performance fix in the exporter might justify an exporter version bump, but not a format version bump.

Tries to export `Nat` on the appearance of a nat literal, and Char.ofNat and String.ofList on the appearance of a string literal.

ammkrn · 2026-01-01T09:07:01Z

When ready, will close#3 (also see that issue for relevant discussion).

The format is described in format_ndjson and the README has been updated accordingly, along with the recommended command for invocation; the old README recommended invoking lake exe, which will not correctly set up the lake env in the most common use case, something like exporting mathlib.

hargoniX · 2026-01-07T13:30:44Z

+Expr.lit (Literal.strVal)
+```
+{
+ "lit": {


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)]

Thanks, I've pushed a correction for the format specification.

hargoniX · 2026-01-07T14:45:44Z

+ "levelParams": Array<integer>,
+ "type": integer,
+ "value": integer,
+ "hints": Array<"opaque" | "abbrev" | integer>


This is also incorrectly documented afaict?

Corrects two errors in the format specification for string literals and reducibility hints.

Correct a typo of `deBruijnIndex`

ammkrn · 2026-01-09T16:13:08Z

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

nomeata · 2026-01-09T16:35:24Z

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.)

Modifies the export procedure and format to export the components of an inductive declaration (the inductive specification(s), constructors, and recursors) together. Consumers are generally going to want to find these related declarations anyway, and with the introduction of the auxiliary `.rec_<N>` recursors motivated by nested inductive support, (in my opinion) this is a more comprehensible format.

ammkrn · 2026-01-13T14:29:54Z

I've added one commit 50db814 to implement the change mentioned elsewhere, packaging related elements of an inductive declaration.

nomeata · 2026-01-13T14:42:57Z

Great! Are declarations now following the Lean.Declaration type consistently, so that a lean-using importer can parse to that type directly?

Hmm, it seems we now have a somewhat odd mix of Lean.Declaration and Lean.ConstantInfo. But if its a “best of both worlds” mix it’s maybe fine?

ammkrn · 2026-01-13T15:01:25Z

Great! Are declarations now following the Lean.Declaration type consistently, so that a lean-using importer can parse to that type directly?
Hmm, it seems we now have a somewhat odd mix of Lean.Declaration and Lean.ConstantInfo. But if its a “best of both worlds” mix it’s maybe fine?

I'm not sure how one would be able to parse anything directly regardless of format since (a) we're using integer pointers and (b) it was already suggested that we make simplifying cuts that would prevent direct parsing, like removing "deBruijnIndex" and changing "binderName".

Lean.Declaration only includes what's strictly necessary for a "full" kernel implementation to do the work of type checking; for example it expects the consumer to both construct and check recursors. The very first exporter implementation followed that pattern.

In the previous round of format changes, it was decided that the exporter should include additional information (like "targets" for the recursors and rec rules, Eq/Quot declarations, etc.). With this additional info it's much easier to bootstrap new checkers, implement certain memory optimizations, and have things like parallel checkers.

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.

nomeata · 2026-01-13T15:22:08Z

I didn’t mean “parse generically”, but I meant “parse export to List Lean.Declaration” (so field name changes or indirections are not a blocker).

But thanks for the historical perspective, agreed on that count.

nomeata · 2026-01-15T12:24:36Z

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.

These are always ever unsafe, so not of high importance here? But in principle you are right.

Exports elements of mutual theorem and def/opaque blocks together.

ammkrn · 2026-01-15T16:50:45Z

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.
These are always ever unsafe, so not of high importance here? But in principle you are right.

Should be done in 7188ec9 modulo style issues.

nomeata · 2026-01-15T17:13:22Z

Am I reading this right that it doesn't distinguish between a normal definition and a singly-recursive definition? It seems that of that's the case, import information is lost. I assume that's why Lean.Declaration is explicit in where the mutual groups are. But maybe lean forgets that information so it's hard to reproduce the declaration here?

nomeata · 2026-01-15T17:25:16Z

Hmm, the Kernel certainly doesn’t seem to remember whether a declaration came from a .mutualDefnDecl or not, so by the time we have a ConstantInfo this information is lost.

Ah! But the kernel treats any unsafe declaration as recursive, even if not in a mutual block. Odd. But not partial declarations.

I find it confusing.

In any case, I think I’m leaning towards an export format that more closely matches Lean.Declaration here, and with a dedicated .mutual tag that is only used when Lean.Declaration.mutualDefnDecl would be used (namely when its unsafe or partial and all is not a singleton). This way parsers for checkers who do not support this can just skip the whole line. But I don't feel strongly about it.

ammkrn · 2026-01-15T18:20:29Z

In any case, I think I’m leaning towards an export format that more closely matches Lean.Declaration here, and with a dedicated .mutual tag that is only used when Lean.Declaration.mutualDefnDecl would be used (namely when its unsafe or partial and all is not a singleton). This way parsers for checkers who do not support this can just skip the whole line. But I don't feel strongly about it.

I have no issue with that. To the earlier question, I think examination of all (specifically whether there's more than one name in there) would be the context clue.

Adds a separate metadata field for the format version, since it's not necessarily the same as the exporter version. For example a performance fix in the exporter might justify an exporter version bump, but not a format version bump.

Tries to export `Nat` on the appearance of a nat literal, and Char.ofNat and String.ofList on the appearance of a string literal.

ammkrn · 2026-01-01T09:07:01Z

When ready, will close#3 (also see that issue for relevant discussion).

The format is described in format_ndjson and the README has been updated accordingly, along with the recommended command for invocation; the old README recommended invoking lake exe, which will not correctly set up the lake env in the most common use case, something like exporting mathlib.

hargoniX · 2026-01-07T13:30:44Z

+Expr.lit (Literal.strVal)
+```
+{
+ "lit": {


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)]

Thanks, I've pushed a correction for the format specification.

hargoniX · 2026-01-07T14:45:44Z

+ "levelParams": Array<integer>,
+ "type": integer,
+ "value": integer,
+ "hints": Array<"opaque" | "abbrev" | integer>


This is also incorrectly documented afaict?

Corrects two errors in the format specification for string literals and reducibility hints.

Correct a typo of `deBruijnIndex`

ammkrn · 2026-01-09T16:13:08Z

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

nomeata · 2026-01-09T16:35:24Z

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.)

Modifies the export procedure and format to export the components of an inductive declaration (the inductive specification(s), constructors, and recursors) together. Consumers are generally going to want to find these related declarations anyway, and with the introduction of the auxiliary `.rec_<N>` recursors motivated by nested inductive support, (in my opinion) this is a more comprehensible format.

ammkrn · 2026-01-13T14:29:54Z

I've added one commit 50db814 to implement the change mentioned elsewhere, packaging related elements of an inductive declaration.

nomeata · 2026-01-13T14:42:57Z

Great! Are declarations now following the Lean.Declaration type consistently, so that a lean-using importer can parse to that type directly?

Hmm, it seems we now have a somewhat odd mix of Lean.Declaration and Lean.ConstantInfo. But if its a “best of both worlds” mix it’s maybe fine?

ammkrn · 2026-01-13T15:01:25Z

Great! Are declarations now following the Lean.Declaration type consistently, so that a lean-using importer can parse to that type directly?
Hmm, it seems we now have a somewhat odd mix of Lean.Declaration and Lean.ConstantInfo. But if its a “best of both worlds” mix it’s maybe fine?

I'm not sure how one would be able to parse anything directly regardless of format since (a) we're using integer pointers and (b) it was already suggested that we make simplifying cuts that would prevent direct parsing, like removing "deBruijnIndex" and changing "binderName".

Lean.Declaration only includes what's strictly necessary for a "full" kernel implementation to do the work of type checking; for example it expects the consumer to both construct and check recursors. The very first exporter implementation followed that pattern.

In the previous round of format changes, it was decided that the exporter should include additional information (like "targets" for the recursors and rec rules, Eq/Quot declarations, etc.). With this additional info it's much easier to bootstrap new checkers, implement certain memory optimizations, and have things like parallel checkers.

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.

nomeata · 2026-01-13T15:22:08Z

I didn’t mean “parse generically”, but I meant “parse export to List Lean.Declaration” (so field name changes or indirections are not a blocker).

But thanks for the historical perspective, agreed on that count.

nomeata · 2026-01-15T12:24:36Z

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.

These are always ever unsafe, so not of high importance here? But in principle you are right.

Exports elements of mutual theorem and def/opaque blocks together.

ammkrn · 2026-01-15T16:50:45Z

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.
These are always ever unsafe, so not of high importance here? But in principle you are right.

Should be done in 7188ec9 modulo style issues.

nomeata · 2026-01-15T17:13:22Z

Am I reading this right that it doesn't distinguish between a normal definition and a singly-recursive definition? It seems that of that's the case, import information is lost. I assume that's why Lean.Declaration is explicit in where the mutual groups are. But maybe lean forgets that information so it's hard to reproduce the declaration here?

nomeata · 2026-01-15T17:25:16Z

Hmm, the Kernel certainly doesn’t seem to remember whether a declaration came from a .mutualDefnDecl or not, so by the time we have a ConstantInfo this information is lost.

Ah! But the kernel treats any unsafe declaration as recursive, even if not in a mutual block. Odd. But not partial declarations.

I find it confusing.

In any case, I think I’m leaning towards an export format that more closely matches Lean.Declaration here, and with a dedicated .mutual tag that is only used when Lean.Declaration.mutualDefnDecl would be used (namely when its unsafe or partial and all is not a singleton). This way parsers for checkers who do not support this can just skip the whole line. But I don't feel strongly about it.

ammkrn · 2026-01-15T18:20:29Z

In any case, I think I’m leaning towards an export format that more closely matches Lean.Declaration here, and with a dedicated .mutual tag that is only used when Lean.Declaration.mutualDefnDecl would be used (namely when its unsafe or partial and all is not a singleton). This way parsers for checkers who do not support this can just skip the whole line. But I don't feel strongly about it.

I have no issue with that. To the earlier question, I think examination of all (specifically whether there's more than one name in there) would be the context clue.

Adds a separate metadata field for the format version, since it's not necessarily the same as the exporter version. For example a performance fix in the exporter might justify an exporter version bump, but not a format version bump.

Tries to export `Nat` on the appearance of a nat literal, and Char.ofNat and String.ofList on the appearance of a string literal.

ammkrn · 2026-01-01T09:07:01Z

When ready, will close#3 (also see that issue for relevant discussion).

The format is described in format_ndjson and the README has been updated accordingly, along with the recommended command for invocation; the old README recommended invoking lake exe, which will not correctly set up the lake env in the most common use case, something like exporting mathlib.

hargoniX · 2026-01-07T13:30:44Z

+Expr.lit (Literal.strVal)
+```
+{
+ "lit": {


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)]

Thanks, I've pushed a correction for the format specification.

hargoniX · 2026-01-07T14:45:44Z

+ "levelParams": Array<integer>,
+ "type": integer,
+ "value": integer,
+ "hints": Array<"opaque" | "abbrev" | integer>


This is also incorrectly documented afaict?

Corrects two errors in the format specification for string literals and reducibility hints.

Correct a typo of `deBruijnIndex`

ammkrn · 2026-01-09T16:13:08Z

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

nomeata · 2026-01-09T16:35:24Z

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.)

Modifies the export procedure and format to export the components of an inductive declaration (the inductive specification(s), constructors, and recursors) together. Consumers are generally going to want to find these related declarations anyway, and with the introduction of the auxiliary `.rec_<N>` recursors motivated by nested inductive support, (in my opinion) this is a more comprehensible format.

ammkrn · 2026-01-13T14:29:54Z

I've added one commit 50db814 to implement the change mentioned elsewhere, packaging related elements of an inductive declaration.

nomeata · 2026-01-13T14:42:57Z

Great! Are declarations now following the Lean.Declaration type consistently, so that a lean-using importer can parse to that type directly?

Hmm, it seems we now have a somewhat odd mix of Lean.Declaration and Lean.ConstantInfo. But if its a “best of both worlds” mix it’s maybe fine?

ammkrn · 2026-01-13T15:01:25Z

Great! Are declarations now following the Lean.Declaration type consistently, so that a lean-using importer can parse to that type directly?
Hmm, it seems we now have a somewhat odd mix of Lean.Declaration and Lean.ConstantInfo. But if its a “best of both worlds” mix it’s maybe fine?

I'm not sure how one would be able to parse anything directly regardless of format since (a) we're using integer pointers and (b) it was already suggested that we make simplifying cuts that would prevent direct parsing, like removing "deBruijnIndex" and changing "binderName".

Lean.Declaration only includes what's strictly necessary for a "full" kernel implementation to do the work of type checking; for example it expects the consumer to both construct and check recursors. The very first exporter implementation followed that pattern.

In the previous round of format changes, it was decided that the exporter should include additional information (like "targets" for the recursors and rec rules, Eq/Quot declarations, etc.). With this additional info it's much easier to bootstrap new checkers, implement certain memory optimizations, and have things like parallel checkers.

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.

nomeata · 2026-01-13T15:22:08Z

I didn’t mean “parse generically”, but I meant “parse export to List Lean.Declaration” (so field name changes or indirections are not a blocker).

But thanks for the historical perspective, agreed on that count.

nomeata · 2026-01-15T12:24:36Z

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.

These are always ever unsafe, so not of high importance here? But in principle you are right.

Exports elements of mutual theorem and def/opaque blocks together.

ammkrn · 2026-01-15T16:50:45Z

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.
These are always ever unsafe, so not of high importance here? But in principle you are right.

Should be done in 7188ec9 modulo style issues.

nomeata · 2026-01-15T17:13:22Z

Am I reading this right that it doesn't distinguish between a normal definition and a singly-recursive definition? It seems that of that's the case, import information is lost. I assume that's why Lean.Declaration is explicit in where the mutual groups are. But maybe lean forgets that information so it's hard to reproduce the declaration here?

nomeata · 2026-01-15T17:25:16Z

Hmm, the Kernel certainly doesn’t seem to remember whether a declaration came from a .mutualDefnDecl or not, so by the time we have a ConstantInfo this information is lost.

Ah! But the kernel treats any unsafe declaration as recursive, even if not in a mutual block. Odd. But not partial declarations.

I find it confusing.

In any case, I think I’m leaning towards an export format that more closely matches Lean.Declaration here, and with a dedicated .mutual tag that is only used when Lean.Declaration.mutualDefnDecl would be used (namely when its unsafe or partial and all is not a singleton). This way parsers for checkers who do not support this can just skip the whole line. But I don't feel strongly about it.

ammkrn · 2026-01-15T18:20:29Z

In any case, I think I’m leaning towards an export format that more closely matches Lean.Declaration here, and with a dedicated .mutual tag that is only used when Lean.Declaration.mutualDefnDecl would be used (namely when its unsafe or partial and all is not a singleton). This way parsers for checkers who do not support this can just skip the whole line. But I don't feel strongly about it.

I have no issue with that. To the earlier question, I think examination of all (specifically whether there's more than one name in there) would be the context clue.

Adds a separate metadata field for the format version, since it's not necessarily the same as the exporter version. For example a performance fix in the exporter might justify an exporter version bump, but not a format version bump.

Tries to export `Nat` on the appearance of a nat literal, and Char.ofNat and String.ofList on the appearance of a string literal.

ammkrn · 2026-01-01T09:07:01Z

When ready, will close#3 (also see that issue for relevant discussion).

The format is described in format_ndjson and the README has been updated accordingly, along with the recommended command for invocation; the old README recommended invoking lake exe, which will not correctly set up the lake env in the most common use case, something like exporting mathlib.

hargoniX · 2026-01-07T13:30:44Z

+Expr.lit (Literal.strVal)
+```
+{
+ "lit": {


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)]

Thanks, I've pushed a correction for the format specification.

hargoniX · 2026-01-07T14:45:44Z

+ "levelParams": Array<integer>,
+ "type": integer,
+ "value": integer,
+ "hints": Array<"opaque" | "abbrev" | integer>


This is also incorrectly documented afaict?

Corrects two errors in the format specification for string literals and reducibility hints.

Correct a typo of `deBruijnIndex`

ammkrn · 2026-01-09T16:13:08Z

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

nomeata · 2026-01-09T16:35:24Z

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.)

Modifies the export procedure and format to export the components of an inductive declaration (the inductive specification(s), constructors, and recursors) together. Consumers are generally going to want to find these related declarations anyway, and with the introduction of the auxiliary `.rec_<N>` recursors motivated by nested inductive support, (in my opinion) this is a more comprehensible format.

ammkrn · 2026-01-13T14:29:54Z

I've added one commit 50db814 to implement the change mentioned elsewhere, packaging related elements of an inductive declaration.

nomeata · 2026-01-13T14:42:57Z

Great! Are declarations now following the Lean.Declaration type consistently, so that a lean-using importer can parse to that type directly?

Hmm, it seems we now have a somewhat odd mix of Lean.Declaration and Lean.ConstantInfo. But if its a “best of both worlds” mix it’s maybe fine?

ammkrn · 2026-01-13T15:01:25Z

Great! Are declarations now following the Lean.Declaration type consistently, so that a lean-using importer can parse to that type directly?
Hmm, it seems we now have a somewhat odd mix of Lean.Declaration and Lean.ConstantInfo. But if its a “best of both worlds” mix it’s maybe fine?

I'm not sure how one would be able to parse anything directly regardless of format since (a) we're using integer pointers and (b) it was already suggested that we make simplifying cuts that would prevent direct parsing, like removing "deBruijnIndex" and changing "binderName".

Lean.Declaration only includes what's strictly necessary for a "full" kernel implementation to do the work of type checking; for example it expects the consumer to both construct and check recursors. The very first exporter implementation followed that pattern.

In the previous round of format changes, it was decided that the exporter should include additional information (like "targets" for the recursors and rec rules, Eq/Quot declarations, etc.). With this additional info it's much easier to bootstrap new checkers, implement certain memory optimizations, and have things like parallel checkers.

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.

nomeata · 2026-01-13T15:22:08Z

I didn’t mean “parse generically”, but I meant “parse export to List Lean.Declaration” (so field name changes or indirections are not a blocker).

But thanks for the historical perspective, agreed on that count.

nomeata · 2026-01-15T12:24:36Z

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.

These are always ever unsafe, so not of high importance here? But in principle you are right.

Exports elements of mutual theorem and def/opaque blocks together.

ammkrn · 2026-01-15T16:50:45Z

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.
These are always ever unsafe, so not of high importance here? But in principle you are right.

Should be done in 7188ec9 modulo style issues.

nomeata · 2026-01-15T17:13:22Z

Am I reading this right that it doesn't distinguish between a normal definition and a singly-recursive definition? It seems that of that's the case, import information is lost. I assume that's why Lean.Declaration is explicit in where the mutual groups are. But maybe lean forgets that information so it's hard to reproduce the declaration here?

nomeata · 2026-01-15T17:25:16Z

Hmm, the Kernel certainly doesn’t seem to remember whether a declaration came from a .mutualDefnDecl or not, so by the time we have a ConstantInfo this information is lost.

Ah! But the kernel treats any unsafe declaration as recursive, even if not in a mutual block. Odd. But not partial declarations.

I find it confusing.

In any case, I think I’m leaning towards an export format that more closely matches Lean.Declaration here, and with a dedicated .mutual tag that is only used when Lean.Declaration.mutualDefnDecl would be used (namely when its unsafe or partial and all is not a singleton). This way parsers for checkers who do not support this can just skip the whole line. But I don't feel strongly about it.

ammkrn · 2026-01-15T18:20:29Z

In any case, I think I’m leaning towards an export format that more closely matches Lean.Declaration here, and with a dedicated .mutual tag that is only used when Lean.Declaration.mutualDefnDecl would be used (namely when its unsafe or partial and all is not a singleton). This way parsers for checkers who do not support this can just skip the whole line. But I don't feel strongly about it.

I have no issue with that. To the earlier question, I think examination of all (specifically whether there's more than one name in there) would be the context clue.

Adds a separate metadata field for the format version, since it's not necessarily the same as the exporter version. For example a performance fix in the exporter might justify an exporter version bump, but not a format version bump.

Tries to export `Nat` on the appearance of a nat literal, and Char.ofNat and String.ofList on the appearance of a string literal.

ammkrn · 2026-01-01T09:07:01Z

When ready, will close#3 (also see that issue for relevant discussion).

The format is described in format_ndjson and the README has been updated accordingly, along with the recommended command for invocation; the old README recommended invoking lake exe, which will not correctly set up the lake env in the most common use case, something like exporting mathlib.

hargoniX · 2026-01-07T13:30:44Z

+Expr.lit (Literal.strVal)
+```
+{
+ "lit": {


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)]

Thanks, I've pushed a correction for the format specification.

hargoniX · 2026-01-07T14:45:44Z

+ "levelParams": Array<integer>,
+ "type": integer,
+ "value": integer,
+ "hints": Array<"opaque" | "abbrev" | integer>


This is also incorrectly documented afaict?

Corrects two errors in the format specification for string literals and reducibility hints.

Correct a typo of `deBruijnIndex`

ammkrn · 2026-01-09T16:13:08Z

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

nomeata · 2026-01-09T16:35:24Z

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.)

Modifies the export procedure and format to export the components of an inductive declaration (the inductive specification(s), constructors, and recursors) together. Consumers are generally going to want to find these related declarations anyway, and with the introduction of the auxiliary `.rec_<N>` recursors motivated by nested inductive support, (in my opinion) this is a more comprehensible format.

ammkrn · 2026-01-13T14:29:54Z

I've added one commit 50db814 to implement the change mentioned elsewhere, packaging related elements of an inductive declaration.

nomeata · 2026-01-13T14:42:57Z

Great! Are declarations now following the Lean.Declaration type consistently, so that a lean-using importer can parse to that type directly?

Hmm, it seems we now have a somewhat odd mix of Lean.Declaration and Lean.ConstantInfo. But if its a “best of both worlds” mix it’s maybe fine?

ammkrn · 2026-01-13T15:01:25Z

Great! Are declarations now following the Lean.Declaration type consistently, so that a lean-using importer can parse to that type directly?
Hmm, it seems we now have a somewhat odd mix of Lean.Declaration and Lean.ConstantInfo. But if its a “best of both worlds” mix it’s maybe fine?

I'm not sure how one would be able to parse anything directly regardless of format since (a) we're using integer pointers and (b) it was already suggested that we make simplifying cuts that would prevent direct parsing, like removing "deBruijnIndex" and changing "binderName".

Lean.Declaration only includes what's strictly necessary for a "full" kernel implementation to do the work of type checking; for example it expects the consumer to both construct and check recursors. The very first exporter implementation followed that pattern.

In the previous round of format changes, it was decided that the exporter should include additional information (like "targets" for the recursors and rec rules, Eq/Quot declarations, etc.). With this additional info it's much easier to bootstrap new checkers, implement certain memory optimizations, and have things like parallel checkers.

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.

nomeata · 2026-01-13T15:22:08Z

I didn’t mean “parse generically”, but I meant “parse export to List Lean.Declaration” (so field name changes or indirections are not a blocker).

But thanks for the historical perspective, agreed on that count.

nomeata · 2026-01-15T12:24:36Z

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.

These are always ever unsafe, so not of high importance here? But in principle you are right.

Exports elements of mutual theorem and def/opaque blocks together.

ammkrn · 2026-01-15T16:50:45Z

Looking at Lean.Declaration, maybe it's worth it to similarly group mutual definitions as well.
These are always ever unsafe, so not of high importance here? But in principle you are right.

Should be done in 7188ec9 modulo style issues.

nomeata · 2026-01-15T17:13:22Z

Am I reading this right that it doesn't distinguish between a normal definition and a singly-recursive definition? It seems that of that's the case, import information is lost. I assume that's why Lean.Declaration is explicit in where the mutual groups are. But maybe lean forgets that information so it's hard to reproduce the declaration here?

nomeata · 2026-01-15T17:25:16Z

Hmm, the Kernel certainly doesn’t seem to remember whether a declaration came from a .mutualDefnDecl or not, so by the time we have a ConstantInfo this information is lost.

Ah! But the kernel treats any unsafe declaration as recursive, even if not in a mutual block. Odd. But not partial declarations.

I find it confusing.

In any case, I think I’m leaning towards an export format that more closely matches Lean.Declaration here, and with a dedicated .mutual tag that is only used when Lean.Declaration.mutualDefnDecl would be used (namely when its unsafe or partial and all is not a singleton). This way parsers for checkers who do not support this can just skip the whole line. But I don't feel strongly about it.

ammkrn · 2026-01-15T18:20:29Z

In any case, I think I’m leaning towards an export format that more closely matches Lean.Declaration here, and with a dedicated .mutual tag that is only used when Lean.Declaration.mutualDefnDecl would be used (namely when its unsafe or partial and all is not a singleton). This way parsers for checkers who do not support this can just skip the whole line. But I don't feel strongly about it.

I have no issue with that. To the earlier question, I think examination of all (specifically whether there's more than one name in there) would be the context clue.

Adds a separate metadata field for the format version, since it's not necessarily the same as the exporter version. For example a performance fix in the exporter might justify an exporter version bump, but not a format version bump.

Tries to export `Nat` on the appearance of a nat literal, and Char.ofNat and String.ofList on the appearance of a string literal.

Transition to ndjson export format
c840756

ammkrn force-pushed the json_output branch from 8707984 to c840756Compare January 2, 2026 23:53

hargoniX reviewed Jan 7, 2026
View reviewed changes

fix: correct ndjson format specification
eb4d3b7
Corrects two errors in the format specification for string literals and reducibility hints.

hargoniX reviewed Jan 7, 2026
View reviewed changes

Comment threadformat_ndjson.md Outdated

hargoniX mentioned this pull request Jan 7, 2026
feat: JSON format parser #12
Closed

fix: correct typo in ndjson format spec
6bdcc85
Correct a typo of `deBruijnIndex`

nomeata reviewed Jan 8, 2026
View reviewed changes

Comment threadExport.lean Outdated
Comment threadExport.lean Outdated

ammkrn force-pushed the json_output branch from 7dd4105 to 51c7971Compare January 9, 2026 16:04

chore: namespace backrefs, abbreviate some attrs
e581cf2
+ Namespaces backreferences from a generic "i" to "in", "il", and "ie" for name, level, and expr. + Abbreviates some json attribute names

ammkrn force-pushed the json_output branch from 51c7971 to e581cf2Compare January 9, 2026 16:17

nomeata reviewed Jan 13, 2026
View reviewed changes

Comment threadExport.lean Outdated

nomeata reviewed Jan 14, 2026
View reviewed changes

Comment threadExport.lean

nomeata mentioned this pull request Jan 15, 2026
[RFC] Switch to JSON #3
Closed

feat: export elements of mutual thm/defs together
7188ec9
Exports elements of mutual theorem and def/opaque blocks together.

ammkrn added 2 commits January 16, 2026 07:37

feat: Add metadata field for format version
7e89abb
Adds a separate metadata field for the format version, since it's not necessarily the same as the exporter version. For example a performance fix in the exporter might justify an exporter version bump, but not a format version bump.

fix: try to export Nat/String declarations for lit
f54fd09
Tries to export `Nat` on the appearance of a nat literal, and Char.ofNat and String.ofList on the appearance of a string literal.

hargoniX merged commit 4f1e55e into leanprover:masterJan 23, 2026
1 check passed

Transition to ndjson export format
c840756

ammkrn force-pushed the json_output branch from 8707984 to c840756Compare January 2, 2026 23:53

hargoniX reviewed Jan 7, 2026
View reviewed changes

fix: correct ndjson format specification
eb4d3b7
Corrects two errors in the format specification for string literals and reducibility hints.

hargoniX reviewed Jan 7, 2026
View reviewed changes

Comment threadformat_ndjson.md Outdated

hargoniX mentioned this pull request Jan 7, 2026
feat: JSON format parser #12
Closed

fix: correct typo in ndjson format spec
6bdcc85
Correct a typo of `deBruijnIndex`

nomeata reviewed Jan 8, 2026
View reviewed changes

Comment threadExport.lean Outdated
Comment threadExport.lean Outdated

ammkrn force-pushed the json_output branch from 7dd4105 to 51c7971Compare January 9, 2026 16:04

chore: namespace backrefs, abbreviate some attrs
e581cf2
+ Namespaces backreferences from a generic "i" to "in", "il", and "ie" for name, level, and expr. + Abbreviates some json attribute names

ammkrn force-pushed the json_output branch from 51c7971 to e581cf2Compare January 9, 2026 16:17

nomeata reviewed Jan 13, 2026
View reviewed changes

Comment threadExport.lean Outdated

nomeata reviewed Jan 14, 2026
View reviewed changes

Comment threadExport.lean

nomeata mentioned this pull request Jan 15, 2026
[RFC] Switch to JSON #3
Closed

feat: export elements of mutual thm/defs together
7188ec9
Exports elements of mutual theorem and def/opaque blocks together.

ammkrn added 2 commits January 16, 2026 07:37

feat: Add metadata field for format version
7e89abb
Adds a separate metadata field for the format version, since it's not necessarily the same as the exporter version. For example a performance fix in the exporter might justify an exporter version bump, but not a format version bump.

fix: try to export Nat/String declarations for lit
f54fd09
Tries to export `Nat` on the appearance of a nat literal, and Char.ofNat and String.ofList on the appearance of a string literal.

hargoniX merged commit 4f1e55e into leanprover:masterJan 23, 2026
1 check passed

Transition to ndjson export format
c840756

ammkrn force-pushed the json_output branch from 8707984 to c840756Compare January 2, 2026 23:53

hargoniX reviewed Jan 7, 2026
View reviewed changes

fix: correct ndjson format specification
eb4d3b7
Corrects two errors in the format specification for string literals and reducibility hints.

hargoniX reviewed Jan 7, 2026
View reviewed changes

Comment threadformat_ndjson.md Outdated

hargoniX mentioned this pull request Jan 7, 2026
feat: JSON format parser #12
Closed

fix: correct typo in ndjson format spec
6bdcc85
Correct a typo of `deBruijnIndex`

nomeata reviewed Jan 8, 2026
View reviewed changes

Comment threadExport.lean Outdated
Comment threadExport.lean Outdated

ammkrn force-pushed the json_output branch from 7dd4105 to 51c7971Compare January 9, 2026 16:04

chore: namespace backrefs, abbreviate some attrs
e581cf2
+ Namespaces backreferences from a generic "i" to "in", "il", and "ie" for name, level, and expr. + Abbreviates some json attribute names

ammkrn force-pushed the json_output branch from 51c7971 to e581cf2Compare January 9, 2026 16:17

nomeata reviewed Jan 13, 2026
View reviewed changes

Comment threadExport.lean Outdated

nomeata reviewed Jan 14, 2026
View reviewed changes

Comment threadExport.lean

nomeata mentioned this pull request Jan 15, 2026
[RFC] Switch to JSON #3
Closed

feat: export elements of mutual thm/defs together
7188ec9
Exports elements of mutual theorem and def/opaque blocks together.

ammkrn added 2 commits January 16, 2026 07:37

feat: Add metadata field for format version
7e89abb
Adds a separate metadata field for the format version, since it's not necessarily the same as the exporter version. For example a performance fix in the exporter might justify an exporter version bump, but not a format version bump.

fix: try to export Nat/String declarations for lit
f54fd09
Tries to export `Nat` on the appearance of a nat literal, and Char.ofNat and String.ofList on the appearance of a string literal.

hargoniX merged commit 4f1e55e into leanprover:masterJan 23, 2026
1 check passed

Transition to ndjson export format
c840756

ammkrn force-pushed the json_output branch from 8707984 to c840756Compare January 2, 2026 23:53

hargoniX reviewed Jan 7, 2026
View reviewed changes

fix: correct ndjson format specification
eb4d3b7
Corrects two errors in the format specification for string literals and reducibility hints.

hargoniX reviewed Jan 7, 2026
View reviewed changes

Comment threadformat_ndjson.md Outdated

hargoniX mentioned this pull request Jan 7, 2026
feat: JSON format parser #12
Closed

fix: correct typo in ndjson format spec
6bdcc85
Correct a typo of `deBruijnIndex`

nomeata reviewed Jan 8, 2026
View reviewed changes

Comment threadExport.lean Outdated
Comment threadExport.lean Outdated

ammkrn force-pushed the json_output branch from 7dd4105 to 51c7971Compare January 9, 2026 16:04

chore: namespace backrefs, abbreviate some attrs
e581cf2
+ Namespaces backreferences from a generic "i" to "in", "il", and "ie" for name, level, and expr. + Abbreviates some json attribute names

ammkrn force-pushed the json_output branch from 51c7971 to e581cf2Compare January 9, 2026 16:17

nomeata reviewed Jan 13, 2026
View reviewed changes

Comment threadExport.lean Outdated

nomeata reviewed Jan 14, 2026
View reviewed changes

Comment threadExport.lean

nomeata mentioned this pull request Jan 15, 2026
[RFC] Switch to JSON #3
Closed

feat: export elements of mutual thm/defs together
7188ec9
Exports elements of mutual theorem and def/opaque blocks together.

ammkrn added 2 commits January 16, 2026 07:37

feat: Add metadata field for format version
7e89abb
Adds a separate metadata field for the format version, since it's not necessarily the same as the exporter version. For example a performance fix in the exporter might justify an exporter version bump, but not a format version bump.

fix: try to export Nat/String declarations for lit
f54fd09
Tries to export `Nat` on the appearance of a nat literal, and Char.ofNat and String.ofList on the appearance of a string literal.

hargoniX merged commit 4f1e55e into leanprover:masterJan 23, 2026
1 check passed

Transition to ndjson export format
c840756

ammkrn force-pushed the json_output branch from 8707984 to c840756Compare January 2, 2026 23:53

hargoniX reviewed Jan 7, 2026
View reviewed changes

fix: correct ndjson format specification
eb4d3b7
Corrects two errors in the format specification for string literals and reducibility hints.

hargoniX reviewed Jan 7, 2026
View reviewed changes

Comment threadformat_ndjson.md Outdated

hargoniX mentioned this pull request Jan 7, 2026
feat: JSON format parser #12
Closed

fix: correct typo in ndjson format spec
6bdcc85
Correct a typo of `deBruijnIndex`

nomeata reviewed Jan 8, 2026
View reviewed changes

Comment threadExport.lean Outdated
Comment threadExport.lean Outdated

ammkrn force-pushed the json_output branch from 7dd4105 to 51c7971Compare January 9, 2026 16:04

chore: namespace backrefs, abbreviate some attrs
e581cf2
+ Namespaces backreferences from a generic "i" to "in", "il", and "ie" for name, level, and expr. + Abbreviates some json attribute names

ammkrn force-pushed the json_output branch from 51c7971 to e581cf2Compare January 9, 2026 16:17

nomeata reviewed Jan 13, 2026
View reviewed changes

Comment threadExport.lean Outdated

nomeata reviewed Jan 14, 2026
View reviewed changes

Comment threadExport.lean

nomeata mentioned this pull request Jan 15, 2026
[RFC] Switch to JSON #3
Closed

feat: export elements of mutual thm/defs together
7188ec9
Exports elements of mutual theorem and def/opaque blocks together.

ammkrn added 2 commits January 16, 2026 07:37

feat: Add metadata field for format version
7e89abb
Adds a separate metadata field for the format version, since it's not necessarily the same as the exporter version. For example a performance fix in the exporter might justify an exporter version bump, but not a format version bump.

fix: try to export Nat/String declarations for lit
f54fd09
Tries to export `Nat` on the appearance of a nat literal, and Char.ofNat and String.ofList on the appearance of a string literal.

hargoniX merged commit 4f1e55e into leanprover:masterJan 23, 2026
1 check passed

Transition to ndjson export format
c840756

ammkrn force-pushed the json_output branch from 8707984 to c840756Compare January 2, 2026 23:53

hargoniX reviewed Jan 7, 2026
View reviewed changes

fix: correct ndjson format specification
eb4d3b7
Corrects two errors in the format specification for string literals and reducibility hints.

hargoniX reviewed Jan 7, 2026
View reviewed changes

Comment threadformat_ndjson.md Outdated

hargoniX mentioned this pull request Jan 7, 2026
feat: JSON format parser #12
Closed

fix: correct typo in ndjson format spec
6bdcc85
Correct a typo of `deBruijnIndex`

nomeata reviewed Jan 8, 2026
View reviewed changes

Comment threadExport.lean Outdated
Comment threadExport.lean Outdated

ammkrn force-pushed the json_output branch from 7dd4105 to 51c7971Compare January 9, 2026 16:04

chore: namespace backrefs, abbreviate some attrs
e581cf2
+ Namespaces backreferences from a generic "i" to "in", "il", and "ie" for name, level, and expr. + Abbreviates some json attribute names

ammkrn force-pushed the json_output branch from 51c7971 to e581cf2Compare January 9, 2026 16:17

nomeata reviewed Jan 13, 2026
View reviewed changes

Comment threadExport.lean Outdated

nomeata reviewed Jan 14, 2026
View reviewed changes

Comment threadExport.lean

nomeata mentioned this pull request Jan 15, 2026
[RFC] Switch to JSON #3
Closed

feat: export elements of mutual thm/defs together
7188ec9
Exports elements of mutual theorem and def/opaque blocks together.

ammkrn added 2 commits January 16, 2026 07:37

feat: Add metadata field for format version
7e89abb
Adds a separate metadata field for the format version, since it's not necessarily the same as the exporter version. For example a performance fix in the exporter might justify an exporter version bump, but not a format version bump.

fix: try to export Nat/String declarations for lit
f54fd09
Tries to export `Nat` on the appearance of a nat literal, and Char.ofNat and String.ofList on the appearance of a string literal.

hargoniX merged commit 4f1e55e into leanprover:masterJan 23, 2026
1 check passed

Transition to ndjson export format
c840756

ammkrn force-pushed the json_output branch from 8707984 to c840756Compare January 2, 2026 23:53

hargoniX reviewed Jan 7, 2026
View reviewed changes

fix: correct ndjson format specification
eb4d3b7
Corrects two errors in the format specification for string literals and reducibility hints.

hargoniX reviewed Jan 7, 2026
View reviewed changes

Comment threadformat_ndjson.md Outdated

hargoniX mentioned this pull request Jan 7, 2026
feat: JSON format parser #12
Closed

fix: correct typo in ndjson format spec
6bdcc85
Correct a typo of `deBruijnIndex`

nomeata reviewed Jan 8, 2026
View reviewed changes

Comment threadExport.lean Outdated
Comment threadExport.lean Outdated

ammkrn force-pushed the json_output branch from 7dd4105 to 51c7971Compare January 9, 2026 16:04

chore: namespace backrefs, abbreviate some attrs
e581cf2
+ Namespaces backreferences from a generic "i" to "in", "il", and "ie" for name, level, and expr. + Abbreviates some json attribute names

ammkrn force-pushed the json_output branch from 51c7971 to e581cf2Compare January 9, 2026 16:17

nomeata reviewed Jan 13, 2026
View reviewed changes

Comment threadExport.lean Outdated

nomeata reviewed Jan 14, 2026
View reviewed changes

Comment threadExport.lean

nomeata mentioned this pull request Jan 15, 2026
[RFC] Switch to JSON #3
Closed

feat: export elements of mutual thm/defs together
7188ec9
Exports elements of mutual theorem and def/opaque blocks together.

ammkrn added 2 commits January 16, 2026 07:37

feat: Add metadata field for format version
7e89abb
Adds a separate metadata field for the format version, since it's not necessarily the same as the exporter version. For example a performance fix in the exporter might justify an exporter version bump, but not a format version bump.

fix: try to export Nat/String declarations for lit
f54fd09
Tries to export `Nat` on the appearance of a nat literal, and Char.ofNat and String.ofList on the appearance of a string literal.

hargoniX merged commit 4f1e55e into leanprover:masterJan 23, 2026
1 check passed

Transition to ndjson export format
c840756

ammkrn force-pushed the json_output branch from 8707984 to c840756Compare January 2, 2026 23:53

hargoniX reviewed Jan 7, 2026
View reviewed changes

fix: correct ndjson format specification
eb4d3b7
Corrects two errors in the format specification for string literals and reducibility hints.

hargoniX reviewed Jan 7, 2026
View reviewed changes

Comment threadformat_ndjson.md Outdated

hargoniX mentioned this pull request Jan 7, 2026
feat: JSON format parser #12
Closed

fix: correct typo in ndjson format spec
6bdcc85
Correct a typo of `deBruijnIndex`

nomeata reviewed Jan 8, 2026
View reviewed changes

Comment threadExport.lean Outdated
Comment threadExport.lean Outdated

ammkrn force-pushed the json_output branch from 7dd4105 to 51c7971Compare January 9, 2026 16:04

chore: namespace backrefs, abbreviate some attrs
e581cf2
+ Namespaces backreferences from a generic "i" to "in", "il", and "ie" for name, level, and expr. + Abbreviates some json attribute names

ammkrn force-pushed the json_output branch from 51c7971 to e581cf2Compare January 9, 2026 16:17

nomeata reviewed Jan 13, 2026
View reviewed changes

Comment threadExport.lean Outdated

nomeata reviewed Jan 14, 2026
View reviewed changes

Comment threadExport.lean

nomeata mentioned this pull request Jan 15, 2026
[RFC] Switch to JSON #3
Closed

feat: export elements of mutual thm/defs together
7188ec9
Exports elements of mutual theorem and def/opaque blocks together.

ammkrn added 2 commits January 16, 2026 07:37

feat: Add metadata field for format version
7e89abb
Adds a separate metadata field for the format version, since it's not necessarily the same as the exporter version. For example a performance fix in the exporter might justify an exporter version bump, but not a format version bump.

fix: try to export Nat/String declarations for lit
f54fd09
Tries to export `Nat` on the appearance of a nat literal, and Char.ofNat and String.ofList on the appearance of a string literal.

hargoniX merged commit 4f1e55e into leanprover:masterJan 23, 2026
1 check passed

Uh oh!

Conversation

ammkrn commented Jan 1, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ammkrn commented Jan 9, 2026

Uh oh!

nomeata commented Jan 9, 2026• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

ammkrn commented Jan 13, 2026

Uh oh!

nomeata commented Jan 13, 2026• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ammkrn commented Jan 13, 2026

Uh oh!

nomeata commented Jan 13, 2026

Uh oh!

Uh oh!

nomeata commented Jan 15, 2026

Uh oh!

ammkrn commented Jan 15, 2026

Uh oh!

nomeata commented Jan 15, 2026

Uh oh!

nomeata commented Jan 15, 2026

Uh oh!

ammkrn commented Jan 15, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

ammkrn commented Jan 1, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ammkrn commented Jan 9, 2026

Uh oh!

nomeata commented Jan 9, 2026• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

ammkrn commented Jan 13, 2026

Uh oh!

nomeata commented Jan 13, 2026• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ammkrn commented Jan 13, 2026

Uh oh!

nomeata commented Jan 13, 2026

Uh oh!

nomeata commented Jan 9, 2026•
edited
Loading

nomeata commented Jan 13, 2026•
edited
Loading

nomeata commented Jan 9, 2026•
edited
Loading

nomeata commented Jan 13, 2026•
edited
Loading

nomeata commented Jan 9, 2026•
edited
Loading

nomeata commented Jan 13, 2026•
edited
Loading