Transition to ndjson export format

[ammkrn]

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]

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

[ammkrn]

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

[hargoniX]

This is also incorrectly documented afaict?

[ammkrn]

Ditto.

[ammkrn]

The open comments should be resolved, and I believe I addressed the remaining points in #10

[nomeata]

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

[ammkrn]

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

[nomeata]

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]

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]

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]

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.

[ammkrn]

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]

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]

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]

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.