Hi Antony, here https://github.com/glacode/yamma/blob/master/server/src/grammar/GrammarManager.ts I'm creating the grammar rules for set.mm that I will then use for diagnostics, unification, etc. for .mmp files The rules are for Nearly.js The grammar created (for my local set.mm file) has 1624 rules (but 3 are for working vars), so I'm pretty sure, Nearly.js has no problem with large-ish grammars.
I've never used moo: in the same folder you can see a bunch of lexers / tokenizer that implement the required interface. Maybe you can try with one of those. Since you are there, you can also try the extension, I guess :-) (if you know mmj2, you should feel at home) Please, consider it is my first Typescript (and Node.js) project, so expect weird code :-) Glauco Il giorno sabato 3 dicembre 2022 alle 22:43:36 UTC+1 [email protected] ha scritto: > > 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 > > 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: > > 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/a866821c-bd11-4f13-a32e-d772ee93a098n%40googlegroups.com.
