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/CAJ48g%2BAwQD7mgSfDSokaXctbaiGsLi7UNpSmf%2B_3j1PPbCnpmg%40mail.gmail.com.
