On Sun, Feb 19, 2023 at 1:05 PM Mario Carneiro <[email protected]> wrote:
> I don't see those as competing goals at all. They play different roles: > for browsing you would ideally have some server supplying only the required > information to render a specific proof, and for a proof assistant (and to > some extent a search tool as well) you want to have the whole database > available, > Cool, the need for a streaming parsers to stems entirely from the use of monolithic .mm files, which I have doubted the architectural soundness of, but if you're pointing out that they serve proof assistant users particularly well, but proof explorer users particularly badly, then yes, there's definitely room for both server and client side JSON long term. Especially if we can agree on a particular format, and I'm flexible about that because I'm not very far along. > a streaming parser can only save you a factor of 2 if we assume that > theorems of interest are sampled uniformly. > I'm particularly concerned about not trying the patience of newcomers, and as they tend to start by looking at how we've formalised propositional logic, I was anticipating a substantially greater value-proposition than might be implied by speed up of x2 on average ;-) On Sun, Feb 19, 2023 at 7:19 PM David A. Wheeler <[email protected]> wrote: > > I expect to have a proposal for a JSON format - just a parse tree of a > .mm file, really - early next month if not sooner. > > I think the more interesting case is a JSON format for a *single* proof. > So how about if I was to offer you the parse tree of a .mmp file, instead of the parse tree of a .mm file? That's very much on my roadmap, but I had to start with .mm because I don't believe the code for generating .mmp files exists on the JavaScript platform yet. (Glauco's Yamma doesn't have it yet, and Igor's proof assistant doesn't use them or save any intermediate format I'm aware of). Best regards, Antony -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAJ48g%2BC7T3i%2BnTJ9E%3DeVK_Phz_dLoxbHtAUU2yRri_Pe%2BnNEbQ%40mail.gmail.com.
