Misleading error message "No contribution comment"

metamath / metamath-knife

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.

Apache License 2.0

25 stars 9 forks source link

Misleading error message "No contribution comment" #125

Closed avekens closed 9 months ago

avekens commented 9 months ago

I made a typo in the date contained in "(Contributed by ...)", which was not detected by metamath.exe, verify markup. metamath-knife, however, detected it, but gave a misleading error message:

/target/release/metamath-knife --verify \ warning: No contribution comment --> ./set.mm:505703:5 | 505703 | satf0 $p |- ( (/) Sat (/) ) = ( rec ( ( f e. _V |-> ( f u. | ----- No (Contributed by...) provided for this statement

There was a (Contributed by...), but it was erroneous...

avekens commented 9 months ago

The error message could/should be changed to "Missing or malformed contribution comment" as proposed by @tirix in https://github.com/metamath/set.mm/pull/3497