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 #135

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).

jkingdon commented 9 months ago

The build is failing, partly due to https://github.com/metamath/set.mm/pull/3527 but also for a few things which changed between set.mm's master and develop.

digama0 commented 9 months ago

cc: @tirix, the grammar parsing is failing

tirix commented 9 months ago

The minimal example provided by @digama0 in #137 helped me to propose one fix in #138. Unfortunately this is still not enough for successfully parsing set.mm in the develop branch. The best way would be to do a dichotomy between master and develop, find since when it broke, and what was added at that time. I might have a try this weekend.

jkingdon commented 9 months ago

Now that #138 is merged we may be able to unblock this change (let me figure out how to re-open it or if not I'll fall back to making a new one).