Oops, that was the wrong link, I meant to point to https://www.mediawiki.org/wiki/Page_Previews . (I investigated how this feature is implemented a while ago, with an eye for doing something similar for theorem references.)
On Sun, Feb 19, 2023 at 1:05 PM Mario Carneiro <di.g...@gmail.com> 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, 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 <a...@akb.me.uk> wrote: > >> On Sat, Feb 18, 2023 at 11:04 PM Mario Carneiro <di.g...@gmail.com> >> 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 metamath+unsubscr...@googlegroups.com. >> 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvRCXqXa5X%2B7%2B3SSEZ5A63P%2BeJLhmRcwuP_x8QE6EwdcQ%40mail.gmail.com.
