metamath-cmds is a docker image where I've collected a number of metamath command line tools together for convenience (metamath.exe, metamath-knife, mmj2, checkmm, checkmm-ts, mmverify.py).
Today I have updated this image, so if you run docker run -it akb74/metamath-cmds you will be in a command line which has all the latest versions of these tools and the latest set.mm. However, the last time I did this was two years ago, so most of the time you'd be better off following the instructions in the github repository https://github.com/Antony74/metamath-docker Today I have also added metamath-test ( https://github.com/david-a-wheeler/metamath-test) to the commands available. This is a useful collection of good .mm files which a verifier is expected to pass, and bad .mm files which a verifier is expected to fail. I had to patch my copy of the test harness considerably to get it to run in the metamath-cmds container, some of which is due to the environment, but additionally I think the suite itself may be a little out of date? Finally, I have a question about metamath-knife. In order for the test suite to pass, you have to set the --verify parameter. However, if you do that, it seems metamath-knife loses much of its fabled speed. So I'm wondering in what sense metamath-knife can be considered a sub-one-second verifier if it doesn't pass the test suite in this mode? Sorry if that sounds impertinent, I'd just like to understand the distinction, I'm sure it's doing the most important checks really fast. Thanks, Best regards, Antony -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAJ48g%2BASabinmU590eC41US0So42YSeuMdbR0GUwenj0P1Fd%2Bw%40mail.gmail.com.
