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. (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.
[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 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/99d2acfa-69ae-4beb-8fb4-7b5d01a7ad18n%40googlegroups.com.
