On Sun, Dec 4, 2022 at 5:46 PM Glauco <[email protected]> wrote:
> 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 > Yes, if I've read the Yamma source code correctly, you parse assertions (i.e. axioms, definitions, and the part of the proof that asserts the thing being proved). The rules for how assertions are constructed are contained in the mm file itself, which is why your grammar rules are dynamically created when the mm file is parsed. The mm parser itself is hand coded, not Nearley-generated. That's what took me a while to figure out even though it's all there in your email, and why I first said I was investigating your parsers, then later said I'm writing my own based upon Nearley and EBNF at the back of the Metamath book. Sorry for any consternation I might have caused while I was trying to get myself orientated around a parsing strategy. > 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. No, it's the size of the file it's parsing, not the size of the grammar, that I'm saying may be problematic. I'm making progress on the issues I outlined in my 4th Jan email, but it's still too early to tell. You're unlikely to see the issue Sam and I have reported even if you (possibly inadvisably) try to keep the parse tree for every assertion in set.mm in memory. Best regards, Antony -- 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%2BAAPPUEOy00DP23Ku1F2439-Eqck6Sw7YktwjLzkeDQmg%40mail.gmail.com.
