Add metamath-knife to automated checks

[jkingdon]

This is mostly for the usage check, but while we're here run a verify too.

The result is that metamath-knife runs and gives the same result I'm seeing locally. Which I think means that metamath/metamath-knife#118 has a bug, or exposes a bug which was there, or something. Once we can figure out what is going on there and fix it, we should be able to get passing tests on this pull request.

Fixes #3250.

[tirix]

That's interesting!
I've created a PR to fix this specific issue, but this will not help in the case of definitional checks.

[tirix]

The re-run passed with the new version of metamath-knife, and I've logged an issue in metamath-knife to track the strange behaviour.

[jkingdon]

I've logged an issue in metamath-knife to track the strange behaviour.

I saw different strange behavior with iset.mm but apparently the same fix dealt with it (with respect to --verify-usage anyway: as you point out, the problem may still be there for the definitional checks).

[tirix]

Three remarks:

• this check covers the same thing, with the same implementation, as smm3 (smetamath-rs), so the smm3 check could/should be removed.
• metamath-knife includes a discouraged file generation which is waaay faster than metamath-exe's. It would ease github's server loads and accelerate our CI to move it.
• metamath-knife has also -t and -m options, for typesetting and markup checks. They are also fast, and cover a bit more than other checkers. You could add it to the -v of this PR.

[jkingdon]

I guess I'll merge this now and leave the door open for future pull requests for those other issues. They all sound reasonable to me (not that I really know enough about metamath-knife to know whether any of them would be controversial or present any difficulties). But I don't see any particular need to do everything at once.