On Wed, Dec 21, 2022 at 4:03 PM Samuel Goto <[email protected]> wrote:
> Just to report back on this thread: > > (a) I did start the process within my company to apply the appropriate > open source licenses to my JS verifier. It takes some time, but should be > fine. I'll report back. > Ok, just to report back on this thread, I did manage to get this pushed out as an open source project. Here it goes: https://github.com/google/metamath.js I'm still playing with the renderer, but here is a demo: https://google.github.io/metamath.js/ You can find more examples of me using this library for other sub-axiomatic systems here: https://code.sgo.to/ I also found the compression and decompression of proofs poorly documented, so I tried to encapsulate that into something that others would be able to use to debug their verifiers. > (b) I did manage to make my parser and lexer streamable [1] (I rewrote the > lexer as a state machine), which is good, but it made it substantially > slower (I used async/await in JS which I think creates a Promise for every > single token -- which likely is too much for set.mm's MB file), which is > bad. I have something else in mind that I wanted to try, which is different > than making the parser/lexer streamable, so I'll have to report back on > this too. > So, I did experiment with a bunch of different ways to accomplish a good and scalable mechanism to download, parse and verify metamath in the browser: an asynchronous parser, an asynchronous verifier, etc. At some point, I gave up on that approach and pursued another one: break down set.mm into smaller self-sufficient files, and process (download, paser and verify) it incrementally in the browser rather than as a whole. This led me to developing some modularization syntax for metamath, so that the theorems and axioms can be scoped per file, rather than within a large set.mm database file. It helped me write metamath for other things, so maybe that's something that you all would be curious/interested in (or maybe not). I'll write a bit more on what that looks like and why it makes processing metamath incrementally more easily (specially inside browsers) and report back to this group here. In the meantime, if you are curious about this and have the energy to read from source, you can probably see what I did here: https://github.com/google/metamath.js/blob/main/tests/compiler.js#L1093 > [1] > https://github.com/samuelgoto/metamath/blob/streams/tests/parser.js#L1016 > > On Tuesday, November 29, 2022 at 1:16:02 PM UTC-8 [email protected] wrote: > >> Yes, very impressive! And yes, I believe the client-side proof explorer >> does break new ground - I was edging in that direction, but quite slowly. >> Is the (React) source code for that around anywhere? I see you're trying >> to get it all streaming, presumably so you can parse and display proofs as >> soon as that part of the file is downloaded without having to wait for the >> whole thing to arrive (a download progress bar would be great too). All >> things I was planning to do eventually. >> >> Nice to see standard lexer and parsing tools in your verifier too. Would >> you consider adding a licence to the package.json file? It looks very >> reusable! >> >> Best regards, >> >> Antony >> >> On Tue, Nov 29, 2022 at 9:47 AM Samuel Goto <[email protected]> wrote: >> >>> Hey all, >>> >>> I accidentally ran into metamath and immediately fell in love with >>> the concept. I started building a parser, a verifier and some >>> visualizations to help me understand how and why it worked. >>> >>> It is not much different from what has already been posted before >>> (except, maybe, that's all done client-side on the web), but I figure you'd >>> all appreciate an independent parser, verifier and visualizer out there. >>> >>> So, here it goes: >>> >>> Source Code >>> https://github.com/samuelgoto/metamath >>> >>> Set.mm's client-side verification (takes ~1 min in my macbook m1) >>> https://code.sgo.to/2022/11/26/set.mm.html >>> >>> 2p2e4 Visualization (takes a while to load, but once it does, you >>> can navigate easily) >>> https://code.sgo.to/2022/11/26/2p2e4.html >>> >>> Hoffstader's systems: >>> https://code.sgo.to/2022/04/17/hofstadter-tq.html >>> https://code.sgo.to/2022/04/13/hofstadter-pq.html >>> https://code.sgo.to/2022/04/12/hofstadter-miu.html >>> >>> If you dig into my blog, you'll likely find why I ran into metamath >>> and why I find it so interesting: https://code.sgo.to/ >>> >>> Good stuff you all, >>> >>> Hope this helps, >>> >>> Sam >>> >>> >>> >>> -- >>> 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/23d122fd-021d-4e59-9281-b485d687c047n%40googlegroups.com >>> <https://groups.google.com/d/msgid/metamath/23d122fd-021d-4e59-9281-b485d687c047n%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> >> -- > You received this message because you are subscribed to a topic in the > Google Groups "Metamath" group. > To unsubscribe from this topic, visit > https://groups.google.com/d/topic/metamath/Db2WrDEOX-o/unsubscribe. > To unsubscribe from this group and all its topics, send an email to > [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/99d2acfa-69ae-4beb-8fb4-7b5d01a7ad18n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/99d2acfa-69ae-4beb-8fb4-7b5d01a7ad18n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- f u cn rd ths u cn b a gd prgmr ! -- 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/CAO2BRF-ziGzjdKRRN7dKwbRn%3D%2B5sahuo-c_mVkaga5UNGEu%3DSg%40mail.gmail.com.
