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.
