Repository navigation
[RFC] Switch to JSON #3
Description
Activity
Fwiw I'm not opposed to the idea; while the current format is really easy to write a parser for, JSON would certainly be more accessible for people/projects that don't want to write a parser in the first place. I haven't looked deeply into the name escaping issue yet, but I'll take your word for it that it's a potential source of problems.
I'm interested to see what you come up with.
JSON has a quite complicated spec with lots of extensions which aren't implemented exactly the same (or strictly according to the spec) by different libraries.
Perhaps something slightly more limited and more standardized would be better? (Ideally one would also use a formally verified parser, which after searching for a bit I'm still not quite sure about the status of for JSON)
Perhaps a subset of JSON would work? (Which one would specify separately for the purpose of lean4export.)
I'm not sure what you are referring to, JSON is an exceedingly simple format. The only part I'm aware of tricky bits in json is for representation of large integers and floating point, but I don't think these are likely to be issues since we don't need floats at all and it is unlikely for numbers to get that large except when representing lean bignums, and string encoding these solves the problem completely.
All I'm saying is that there isn't an ironclad standard for how to parse JSON and many (also "standard") parser implementations differ. Some examples: here.
I thought maybe it's important for this export format to have an ironclad standard. Am I wrong? I guess it's also reasonable to say something like "let the parser fail on exported valid lean proofs in extremely rare cases (e.g. if they contain too big numbers), let it crash on malformed input, let it output whatever it wants, the kernel will check everything in the end and that's all that matters".
All I'm saying is that there isn't an ironclad standard for how to parse JSON and many (also "standard") parser implementations differ. Some examples: here.
This is not true. What that page shows is that there exist multiple documents that specify JSON, and parsers sometimes accept more or less than the spec due to implementation limits or "extensions". I don't see why any of this matters, I think you should be more specific.
Regarding having an ironclad standard, I'm not seeing anything here which prevents having such. But this is a proof format, which means that it actually doesn't matter if there are edge cases which are interpreted oddly, because proof checkers are allowed to spuriously fail for implementation limits reasons or even just not liking the shape of the proof. That's a quality-of-implementation issue, not a correctness issue.
Reacted by Adomas Baliuka, Tristan F.-R. and SgI thought maybe it's important for this export format to have an ironclad standard. Am I wrong?
No, you are not wrong. I don't think anyone wants to allow spurious errors to be introduced by a poorly designed serialization format.
With this shared goal in mind, I maintain that imperfect serialization formats, such as JSON, are fine for all pragmatic purposes, provided their shortcomings are dealt with by the serializer - in this case lean4export.
Moreover, "ironclad" serialization formats are rarely truly ironclad. Even the most strictly specified, such as BER/DER - widely used in public key cryptography systems - are replete with deliberately non-conformant implementations. Example: RustCrypto/formats#779.
Finally, the advantages of an export format that can be understood by practically every programming language far outweigh the downsides. Sure, using JSON makes ambiguity and/or invalidity possible, though unlikely. The principal advantage of JSON (or TOML, my preferred format) is ease of implementation. I am optimistic that making it easy to get started will result in more implementations, which will result in more scrutiny of the proof terms constructed by Lean. A more diverse set of kernels will necessarily result in more scrutiny of the serializer itself. By this logic, JSON is a reasonable candidate.
I'm going to be moving forward with this since it's currently an issue in mathlib as mentioned previously; here's an initial pass for what the object layout might look like as markdown and as an (llm derived) json spec. I'm assuming the norm will be ndjson.
This follows Lean's rules for JSON serialization of inductives (the ones used by the deriving handlers) with the exception that one layer of
valbureaucracy for theConstantValitems is removed.LGTM
What about migrating to something like EDN? I don't think you can bypass parser writing that way (much smaller userbase), but it does have better type semantics; should be less ambiguous
My assumption is that people will want to stick with JSON unless you're aware of any existing ambiguity concerns that might be an issue (if so, please share them). On the bright side the exporter is very small, so it should be easy to fork in order to support different formats.
How concrete is this proposal here? Do we already know how much larger exports of, say, mathlib get, and whether parsing is slower or faster?
How concrete is this proposal here? Do we already know how much larger exports of, say, mathlib get, and whether parsing is slower or faster?
At full verbosity using this the output is basically twice the size. I'm not opposed to having a "compact" flag for using shortened property/field names. I don't speak for Lean or the FRO, but since this is the semi-official export tool, I would assume the desire is for something legible that's not going to break, at least as the default output.
How concrete is this proposal here?
I think we're all open to suggestions if you have some.
My gut feeling likes the old format, but for no good reason, and factor 2 seems reasonable, so no complaints from my side.
The main reason I'm asking is if I'd build tools that consume the exported format, if I should simply ignore the old format because it's going to be replaced real soon now, or if this is more a mid-term project here and I shouldn't wait for it.
My gut feeling likes the old format, but for no good reason, and factor 2 seems reasonable, so no complaints from my side.
The main reason I'm asking is if I'd build tools that consume the exported format, if I should simply ignore the old format because it's going to be replaced real soon now, or if this is more a mid-term project here and I shouldn't wait for it.
You should probably ignore the old (current) format, because it's incapable of exporting mathlib releases after the introduction of library_note2, and there are no plans to patch it. In addition to the identifier/string issue, it's not really capable of exporting mdata expressions which at least one user has credibly expressed interest in doing.
The fork I linked in my previous message should more or less work right now. I need to finish writing a new parser, probably make some changes to the exporter in response to whatever is going to come up in testing, and then I'll file a PR.
Reacted by Joachim Breitner9 remaining items
Two of other things I noticed:
* why do Level.max/imax take their arguments as an array as opposed to everything else? * I do not understand how to recover an mdata node with the currently used serialization mechanism. The resulting JSON seems entirely unrecoverable to the original format to me in the general case.Perhaps I should have disclosed earlier, but I have no idea what the proposed use cases are for
mdatain the export file and didn't think very hard about what to do with it. I have no objection to changing the layout and have no input on what a better format might be, other than maybe using the same integer based referencing for the name part of the KVMap keys.max/imax use an array because they're the only elements that have anonymous constructor arguments and I was (at least initially) trying to stick to what Lean was doing.
Reacted by Joachim BreitnerI think it would be best to keep
mdatabecause it changes the expr hash. There was recently a change to removenonDepfrom export to fix the same issue there but I don't think stripping mdata from oleans is reasonable, so I think the checker should just support mdata and do nothing with it (treat it like an identity function which eagerly unfolds in whnf).I think the checker should just support mdata and do nothing with it (treat it like an identity function which eagerly unfolds in whnf).
right, which is also what the official kernel does.
OTOH, it seems a bit overkill to define a stable format for the whole algebra of mdatas, including KVMap and Syntax(!), when for the envisioned applications of the export format we have no use for this. This also means that the format will not be stable across version of lean that only change the MData. And, at least ideally, the expression hash is an implementation detail that shouldn’t have relevance for an external stable proof representation.
I can deal with mdata potentially being included in the default output, but if that's going to be the case I would really prefer to retain a flag to get an export with no mdata. FWIW I do not intend to support mdata in the rust checker.
Reacted by Joachim Breitner@ammkrn, from reading your rust parser it seems that you assume that the indices in the JSON file are used in a strictly increasing contiguous fashion. Is that an invariant you wanted to be part of the format, or was that just an implemenation shortcut in the parser for now?
(Requiring them to be in increasing order may simplify some export-to-export-format transformation tools, e.g. tools that filter the environment.)Off the top of my head I'm pretty sure I can make changes to accommodate indices that appear out of order, but non-contiguous might be tougher. The current setup arises pretty naturally out of the way the exporter currently works and is a nice sanity check for consumers, but maybe you had some kind of parallelism in mind?
I do have one more change I'd like to push that tries to ensure the elements of an inductive declaration (inductive, constructors, recursors) are exported together.
It may or may not also be worth it to have something that tries to export the relevant
NatandStringdeclarations on the first appearance of a nat or string literal. It's technically possible to export anExpr.lit _before the appropriate types are declared; users may expect that in any lean module using a literal (in a project that also has the requisite Nat/String declarations somewhere) that they're always going to get the "fast" kernel behavior, but that's not necessarily the case.I'm hesitant to make such rules part of the export format requirements. It seems that checkers (at least lean4checker and lean4lean) already do a topological sort after parsing.
I think it's reasonable to have a literal without any further operations in an export, at least if you don't do any operations with it.
This is probably bike shedding dangerous corner, given that it's mostly relevant for artificially short exports.
I agree that it's reasonable for an exported environment to have a literal without anything else, the idea is that if environment to be exported has the relevant String/Nat declarations AND they are able to be exported prior to any Expr.lit items, it might be advantageous for the exporter to do that.
I'm hesitant to make such rules part of the export format requirements. It seems that checkers (at least lean4checker and lean4lean) already do a topological sort after parsing.
To the extent this is not about the literals, in the interest of helping any consumer software stay as small as possible, I think when we have to answer the question of "should the exporter be responsible for this or the type checker", the default answer should be the exporter. Even if the type checker has to do something to ensure an invariant/order/whatever has been done properly, it's generally going to be smaller than if it had to do the thing itself.
I can change the export format for inductives to reflect the fact that they should be exported together, I think something like this is probably better anyway, especially for complex mutual/nested declarations:
{ "inductive": { "inductInfos": [..] "ctorInfos": [..] "recInfos": [..] } }If we are going that direction then one could argue that really the entries of the export should be modeled after Lean.Declaration, and really reflect what’s being passed to the kernel, and not what comes out of it. For example, there should be no
recInfo, as that’s something that the kernel produces based on theinductDecl.But that’s turning into a much bigger change than just the replacement of the textual format
JFTR, there was some discussion over at #10 (comment) where @ammkrn made good arguments why the slighly redundant format is better. Instead of going from
List Lena.ConstantInfotoList Lean.Declarationall the way, his proposed format is a combination of the two that combines the best of both worlds, which is convenient for different consumers.Looks like we are converging?
What about versioning? The proposed metadata has fields for tool versions, but should we add a field for the format version itself, so that future changes to the format can get a version, and parsers can implement backwards compatibility?
I think it is fine yes.
The concrete syntax of the export format is troublesome to parse, being a homegrown textual format with a heavy reliance on newline separators and with lots of "clever" sequence encodings. Moreover, the encoding of names is unquoted, which is just plain wrong in the presence of names with escaped characters, because these names can include arbitrary characters, including newlines, keywords and everything else - a classic SQL injection attack.
I propose we drop this ad hoc encoding entirely and switch to a JSON-based format. This is much easier to get right, and libraries for doing the parsing are numerous (but it's also feasible to write the parser directly).