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, or at least all the signatures of all the theorems and the body for the current theorem. Especially when you consider how these things scale asymptotically, it is clear that the dependencies for one proof will be a lot less than the entirety of the file, and a streaming parser can only save you a factor of 2 if we assume that theorems of interest are sampled uniformly. For example I don't think wikipedia is sending a compressed archive of the whole project on every page load - it only sends the data for the current article, as well as server-side json blurbs for link hovers (https://en.wikipedia.org/wiki/Wikipedia:Tools/Navigation_popups). But when someone clicks the "start proof mode" button they will have an expectation that there will be a startup cost, so it is easy to justify loading set.mm and a streaming parser still helps for making that experience better.
On Sun, Feb 19, 2023 at 5:43 AM Antony Bartlett <[email protected]> wrote: > On Sat, Feb 18, 2023 at 11:04 PM Mario Carneiro <[email protected]> wrote: > >> Even if you have a highly optimized mm verifier, you can't get around the >> fact that you need to send some 30 MB over the wire before you can do >> anything. >> > > Just to recap a few things from other threads, back in November, Samuel > Goto demonstrated a dynamic (client-side) proof explorer here > > https://code.sgo.to/2022/11/26/2p2e4.html > > It does indeed take some time to load while a set.mm is sent over the > wire. Hence the subsequent discussion of "streaming parsers", which would > allow for the page to render as soon as the bit of set.mm that we're > interested in has loaded rather than waiting for the whole thing. (or a > verifier could be running on whatever part of the file is available, > successively as it's chunks download) > > (Igor Ieskov's web-based proof assistant loads locally saved files, so > doesn't have the same load time problem). > > 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. > > demo0.mm currently looks like this as JSON: > https://github.com/Antony74/mmparsers/blob/main/examples/demo0.mm.json > and the TypeScript types look like this: > https://github.com/Antony74/mmparsers/blob/main/src/mmParser/mmParseTree.ts > and I plan on writing a JSON schema too, but haven't started on that yet. > > And I'm not proposing anything until I have a working parser! - after > which getting the streaming working may take a little longer. > > Whether this proves popular, or whether I turn out to be its only adoptee, > it's impossible to say, but I wouldn't be at all sorry to see the streaming > parser superseded by some sort of server side JSON if that's what you're > mulling over. > > 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%2BBXDYisz8C%3DvWkOLEUj7V%2BoeCwONqL0m4bDdKZ%2B3EvaEg%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAJ48g%2BBXDYisz8C%3DvWkOLEUj7V%2BoeCwONqL0m4bDdKZ%2B3EvaEg%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSuT8-PEGsQFeQav5kB0hJrtR5YXHB5qRmpGwd55KWyDVQ%40mail.gmail.com.
