search

metamath / metamath-knife

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.
Apache License 2.0
26 stars 11 forks source link

Wrong error message for an unknown label referenced in a comment #146

Closed tirix closed 11 months ago

tirix commented 11 months ago

Metamath-knife complains about an "undeclared token in $v or $c statement" in case an unknown label is referenced in a comment:

Run metamath-knife/target/release/metamath-knife --verify \
warning: Undeclared token 'swrdccatin12lem3'
      --> ./set.mm:1[5](https://github.com/metamath/set.mm/actions/runs/6571260854/job/17850078984?pr=3577#step:6:6)0830:42
       |
150830 |     $( Lemma for ~ pfxccatin12lem2 and ~ swrdccatin12lem3 .  (Contributed by
       |                                          ---------------- This token was not declared in any $v or $c statement
       |
1 diagnostics issued.
Error: Process completed with exit code 1.

Metamath-exe has a better wording:

?Warning: The label token "swrdccatin12lem3" (referenced in comment of
statement "pfxccatin12lem2c") is not a $a or $p statement label.