I also need to be better at writing instructions, but mine should work with a:
git clone https://github.com/samuelgoto/metamath cd metamath npm install npm test <-- this run all the tests, and they should pass, and the test parse set.mm with a couple of my parsers does this help? On Sat, Dec 3, 2022 at 2:10 PM sgoto <[email protected]> wrote: > > > On Sat, Dec 3, 2022 at 1:43 PM Antony Bartlett <[email protected]> wrote: > >> > Ah, yes, I'm trying to make it so that I can download, tokenize, parse >> and verify in a streaming fashion. That makes my code slightly different >> from most other verifiers. >> >> I had a go at this. You can see my attempt here: >> https://github.com/Antony74/mm-streaming-parser >> > > Oh, it would be really neat to make nearley able to parse set.mm! I had > to disable mine, because it ran out of memory and it was also taking too > long: > > https://github.com/samuelgoto/metamath/blob/main/tests/parser.js#L717 > > I wrote a recursive descendant parser which is much faster, but I don't > know how to make it streamable: > > https://github.com/samuelgoto/metamath/blob/main/tests/parser.js#L919 > > >> >> I'm getting an error >> >> set.mm downloaded 0.0MB/40.8MB >> C:\mm\mm-streaming-parser\node_modules\nearley\lib\nearley.js:295 >> var err = new Error(this.reportLexerError(e)); >> ^ >> Error: invalid syntax at line 22 col 1: >> > > I haven't looked at your code yet, but did you get a chance to try and run > mine? My nearley grammar may give you some help, as well as the testing > infrastructure I set up. Here is mine: > > https://github.com/samuelgoto/metamath/blob/main/src/parser.js#L30 > > And if you do manage to make this fast, I'd love to reuse it because > making nearley streamable is easy! > > >> >> 20 >> 21 >> 22 $( ! >> ^ >> 23 >> >> #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# >> 24 Metamath source file for logic and set theory >> Unexpected input (lexer error). Instead, I was expecting to see one of >> the following: >> >> This looks a lot like the following bug report >> https://github.com/kach/nearley/issues/575 >> >> The theory is that >> >> > nearley is probably able to handle streaming properly. But moo is not. >> >> Still, I feel like I was close. A streaming parser would solve all of >> the issues I was bemoaning here >> >> https://groups.google.com/g/metamath/c/mFrNOFa7n8c/m/HkYkyJMaBAAJ >> >> And makes it a concern of the parser rather than something we have to >> worry about, which would be lovely! >> >> Best regards, >> >> Antony >> >> On Sat, Dec 3, 2022 at 12:27 AM sgoto <[email protected]> wrote: >> >>> >>> >>> On Tue, Nov 29, 2022 at 1:16 PM Antony Bartlett <[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? >>>> >>> >>> The source code is available on my website (I don't obfuscate it) if you >>> are curious enough to dig into it, but I can probably make it more >>> accessible/reusable/decent if that's something that's desirable. >>> >>> Here it goes: https://code.sgo.to/static/mm.js >>> >>> Is that something of interest? >>> >>> 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). >>>> >>> >>> Ah, yes, I'm trying to make it so that I can download, tokenize, parse >>> and verify in a streaming fashion. That makes my code slightly different >>> from most other verifiers. >>> >>> I wrote a couple of parsers (a BNF parser and a recursive descendent >>> parser): surprisingly, that's taking up most of the time. Need to think a >>> bit more how to make my recursive descent parser be able to be a streaming >>> one. >>> >>> >>>> 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! >>>> >>>> >>> Ah, yes, will do! I just need to go through a few things but will get >>> back to you with an open source license here. Will report back! >>> >>> Cheers to you all, you guys rock, >>> >>> Sam >>> >>> >>>> 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/CAJ48g%2BBkK%2B2p%3D4K4wdwdZXZWx8kOqKMgz%3DHz9FderKFxCmKfpQ%40mail.gmail.com >>>> <https://groups.google.com/d/msgid/metamath/CAJ48g%2BBkK%2B2p%3D4K4wdwdZXZWx8kOqKMgz%3DHz9FderKFxCmKfpQ%40mail.gmail.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/CAO2BRF9MGjWefEO_ghxp_uHAmBrUTiYwxn36AXUE%2BQ415yLqCw%40mail.gmail.com >>> <https://groups.google.com/d/msgid/metamath/CAO2BRF9MGjWefEO_ghxp_uHAmBrUTiYwxn36AXUE%2BQ415yLqCw%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/CAJ48g%2BDWkJ8nS_k92TFcLH3zg%3DHbF6uzG6NCNuH%3D7Q21N%3DMmCg%40mail.gmail.com >> <https://groups.google.com/d/msgid/metamath/CAJ48g%2BDWkJ8nS_k92TFcLH3zg%3DHbF6uzG6NCNuH%3D7Q21N%3DMmCg%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> > > > -- > f u cn rd ths u cn b a gd prgmr ! > -- 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/CAO2BRF9KmT3knRTuhcfwkqGGnGYm_b_5B17o9JQQZJy7HRSGdQ%40mail.gmail.com.
