search

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

Fix set.mm check #143

Closed jkingdon closed 9 months ago

jkingdon commented 9 months ago

First of all, use the develop branch rather than the master branch because the latter is rather old and we haven't been using it.

Second of all, add --verify-markup and --parse-typesetting so that we run more of the checks (including most notably the ones which the set.mm automated checks enable).

This pull request replaces #135 which was the first attempt at this.

jkingdon commented 9 months ago

I also cherry-picked over @digama0 's change with respect to \r\n line endings (which I looked over fairly quickly; the basic concept of allowing a variety of line endings seems plausible to me).