Thanks Glauco. I'll try to fix this in mmverify.py next week (I'm currently away from my main computer), as well as the problem mentioned in the original post about the infinite loop in case of a non-closed comment. For the latter, it is probably sufficient to replace " while tok != '$)' " with " while tok and tok != '$)' ". This would avoid the infinite loop, but would ignore a non-closing comment at the end of a file. There are a few similar cases with other statements. These could be fixed by handling "EOF" separately. There is also a problem when a file inclusion statement is followed by some text in the same line. So mmverify.py may currently accept some files which should be rejected, but I think it does not reject correct files (with complete proofs).
By the way: you were looking for a place to keep such issues. A natural choice is https://github.com/david-a-wheeler/mmverify.py/issues Benoît On Sunday, May 8, 2022 at 5:08:39 PM UTC+2 [email protected] wrote: > Thanks for asking about this. > > Here's a pull request to add this case to the metamath-exe testsuite: > https://github.com/metamath/metamath-exe/pull/83 > On 5/8/22 05:17, Glauco 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/37b49d2e-54a5-470b-8b9a-bb366790cff0n%40googlegroups.com.
