Hi Antony, if I remember correctly, my first implementation was going n^2, because I used something like
tokens = tokens.slice(1) and linesToParse = linesToParse.slice(1) Are you still experiencing the non-linear behavior? (as a first step, I would look into your 'nexttoken' function) I'm a complete newbie to Typescript and Node.js and my first parser (without verification) took 10 minutes to parse set.mm Then I looked into Node.js profiling: https://nodejs.org/en/docs/guides/simple-profiling/ used with flame graphs https://github.com/brendangregg/FlameGraph and it was enough to spot the .slice(1) problem: the parse time (without verification) went down from 10 minutes to 5 seconds. You may wish to try those two profiling tools in your project. I've not published the parser, yet. It's a "component" of a larger project (a TypeScript language server for mmp files). Unfortunately, the .mm parse logic is distributed in several files: - the parser is a class with a dedicated file (it has a couple of bare-bones parse methods, one synchronous and one asynchronous) - the verifier is a class living in its own file - a tokenizer (every symbol is annotated with a "Range", info needed for producing meaningful language server diagnostics) lives in its own file - every mm statement type has its own class (with its own methods); in particular, I have a BlockStatement class that has several properties and methods, used by the parser/verifier (and it lives in yet another file) - the parser also generates a theory specific grammar for Nearly.js (a general purpose Early parser); and GrammarManager.ts is yet another file I have zero experience in managing a github repository, that's why I prefer to get as close as possible to a "production" level, before publishing the repository on github. HTH Glauco Il giorno domenica 8 maggio 2022 alle 18:11:26 UTC+2 [email protected] ha scritto: > Hi Glauco, > > > I've written a TypeScript parser/verifier (one for .mm and one for .mmp > format) along the lines of mmverify.py > > Can I see, please? My interest is that I may have almost completed a port > of Eric Schmidt's C++ checkmm verifier to TypeScript > > https://github.com/Antony74/checkmm-ts > > (I say "may" because I previously attempted this in 2019 and had a problem > with the performance not being linear compared to the original. It passed > the test suite for all the smaller files, but had I left it running on > set.mm I'm not sure whether it would have completed yet). > > Best regards, > > Antony > > > On Sun, May 8, 2022 at 1:17 PM Glauco <[email protected]> wrote: > >> I can't find test.mm , but I'm using this old post to keep mmverify.py >> 'issues' in one place. >> >> I've written a TypeScript parser/verifier (one for .mm and one for .mmp >> format) along the lines of mmverify.py , and I noticed that both my >> verifier (and mmverify.py) don't catch an error that metamat.exe instead >> does. >> >> If you remove the line >> >> vx.wal $f setvar x $. >> >> from the block of >> >> wal $a wff A. x ph $. >> >> mmverify.py doesn't rise an error (of course, the first theorem that uses >> wal, that is trujust, will rise an error). >> >> Instead, metamath.exe, when reading set.mm (then, even before 'verify >> proof *' ) returns this error: >> >> The source has 200287 statements; 2648 are $a and 39659 are $p. >> >> ?Error on line 23725 of file "set.mm" at statement 4161, label "wal", >> type >> "$a": >> wal $a wff A. x ph $. >> ^ >> This variable does not occur in any active "$e" or "$f" hypothesis. All >> variables in "$a" and "$p" statements must appear in at least one such >> hypothesis. >> >> ?Error on line 23725 of file "set.mm" at statement 4161, label "wal", >> type >> "$a": >> wal $a wff A. x ph $. >> The variable "x" does not appear in an active "$f" statement. >> >> 2 errors were found. >> >> >> I've not looked at the spec in the metamath book, yet, to see if actually >> any var is required to have a kind (when used in assertions). >> >> If I'm not wrong, other verifiers are "based" on mmverify.mm , so I >> decided to write this post. >> >> Glauco >> >> >> >> -- >> 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/d6dd174f-b563-4adb-ad06-5c2531e0520en%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/d6dd174f-b563-4adb-ad06-5c2531e0520en%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/eac1f30f-8b88-41fc-9119-9be56731e3b0n%40googlegroups.com.
