Thanks Glauco, > (as a first step, I would look into your 'nexttoken' function)
Nice guess, you had me wondering! But having tried it the performance of nexttoken() seems nicely linear, and I had to give it ten million tokens before I noticed it taking time. https://github.com/Antony74/checkmm-ts/commit/cbccfd3305266531d11258a8e35ef909fd858b91 My latest port is not quite ready to parse an mm file, so I don't know if I'm going to experience non-linear behaviour this time or not, and I didn't manage to isolate the source of my problem last time round. Maybe what I ported std::set to was a problem, maybe it was something else. My instinct is that this time it will be fine, but if it isn't then I intend to get to the bottom of it! The main reason I started again is that I'm a better TypeScript programmer than I was in 2019 and I don't feel like my original attempt at a port was sufficiently faithful to checkmm.cpp. > I'm a complete newbie to Typescript and Node.js That's cool, I was too once! I might have a slight advantage in that I also use this tech-stack in my professional work. > 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. github specifically, or version control in general? Once you get used to version control, you'll never want to do anything without it again! I'm expecting the port to be some multiple slower than the original, by the way - speed isn't that important to me, having a very expressive language which can create programs that can be accessed from pretty much any device is what I like. Best regards, Antony On Mon, May 9, 2022 at 8:39 PM Glauco <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/eac1f30f-8b88-41fc-9119-9be56731e3b0n%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%2BCG03ALHk_oxvwVcpYwOnbxZbnd2_QaU0Mvs2YGgEn8vQ%40mail.gmail.com.
