I've put a workaround in for the problem I mentioned, and can now reproduce your out of memory issue. It might be easier to debug while streaming to the parser by watching exactly what is growing more than it should be, rather than throw the whole file at it so it thinks about it for a while then keels over (the slowness is almost certainly another symptom of the same problem. Something's wrong, there's no fundamental reason why a general purpose parser-generator shouldn't be able to handle set.mm).
> I haven't looked at your code yet, but did you get a chance to try and run mine? Yes. It's your nearley parser and moo lexer I was trying to get working via streaming. > I also need to be better at writing instructions It's a well laid out npm project - thanks, but I didn't need instructions, they're always almost identical. e.g. for mine git clone https://github.com/Antony74/mm-streaming-parser.git cd mm-streaming-parser npm install npm start Best regards, Antony On Sun, Dec 4, 2022 at 1:49 AM sgoto <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/CAO2BRF9KmT3knRTuhcfwkqGGnGYm_b_5B17o9JQQZJy7HRSGdQ%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%2BB7Lq68TQqJPcB98aBRapApOOR0_g9dAJokuJAisZ%3Dv7Q%40mail.gmail.com.
