Hi Glauco, Thank you very much for sharing your code.
> Please, consider it is my first Typescript (and Node.js) project, so expect weird code :-) You've got nothing at all to worry about there. It's clear from your coding style that you're an experienced developer, even though this is your first time with node/ts (your OO style suggests to me your main language from other projects is probably Java). Also, to paraphrase something Voltaire actually never said, I may occasionally disagree with the way you code something, but I will defend to the death your right as a hobbyist programmer to code things in whatever way you please. So if I do make suggestions, I'll endeavour to be constructive, and you're of course free to take or leave whatever advice I may offer. > Since you are there, you can also try the extension, I guess :-) (if you know mmj2, you should feel at home) Yes, I would like to see your extension running. That would be cool all by itself, but also I find it helps me understand code better sometimes if I can see it running. I'm afraid I'm not familiar with mmj2. Now according to your instructions: - Run `npm install` in this folder. This installs all necessary npm modules in both the client and server folder - Open an .mmp file (this triggers the extension) However, when I install your project and run Visual Studio Code, I don't see any new extension, nothing noticeably special has changed when I open a .mm file, and I'm unsure what a .mmp file is and there don't seem to be any in your repository. Sorry for not being able to figure this out. > The grammar created (for my local set.mm file) has 1624 rules (but 3 are for working vars) So the grammar updates itself programmatically as it finds certain constructs in the .mm file? That's pretty cool, I'm looking forward to seeing what the output parse tree (AST) looks like. I did notice when I was browsing your code that the grammar is set programmatically - there's no Nearley file with the .ne extension. That's cool, but it does make it slightly harder to pop the parser out of your project and into one of my own, like I already did with Samuel's parser. The first step would be to change this line to point at your repo rather than his https://github.com/Antony74/mm-streaming-parser/blob/main/package.json#L17 then I would have to update the beginning of this script to create one of your parsers instead of one of Samuel's https://github.com/Antony74/mm-streaming-parser/blob/main/src/index.ts Hmm... interesting... I imagine I could probably figure that out... Using a git repo as an npm package, by the way, is only intended as a temporary measure, to identify and test the reusability of code before publishing it (in this case your parser) as a separate package. Ideally you would be involved in such a process, and your yamma package, Samuel, myself, and others, would all become potential users of such a package, and I'm someway off proposing any such thing. I only mention it because you might not have come across the use of a git repo as an npm package, and I think it's important to understand it's not good practice, except temporarily for development purposes. mm-streaming-parser is intended as a simple example of how to get piecemeal updates from the fetch api and pass them into a Nearley parser. It's always good when writing web content to be able to display something before everything has loaded, but this is a pressing concern with Metamath content because of how set.mm is structured as a single monolithic file (I believe this has been raised relatively recently in another thread), and particularly once we've gone past the proof we're currently interested in, it seems a shame to have to wait for the rest of the file to download. Best regards, Antony On Sun, Dec 4, 2022 at 5:46 PM Glauco <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/a866821c-bd11-4f13-a32e-d772ee93a098n%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%2BBzTRtucYgNF3PL8%2BbLWRdtbT%3DVwC1Ouc_WAp3cSckOOg%40mail.gmail.com.
