Success with Hmm, metamath-test, and metamath-docker

[Antony Bartlett]

Further to my previous emails, I have managed to get Hmm (the Haskell Metamath verifier) working with the metamath-cmds docker container.

https://github.com/Antony74/metamath-docker/commit/2cad5ad3748d5ed4bf869b7eb32ef46539485a07

However, within the container I have commented it from the metamath-test suite, because it does not pass the test demo0-includer.mm, and doesn't quite seem to be able to handle the latest set.mm well either.

I have tidied up metamath-docker's use of metamath-test, so it only has to override one file in order to run and pass the full suite of tests.  I have opened two pull requests on the metamath-test repository, one for test naming consistency, the other to update the script for metamath-knife (which it still knows as smetamath).

https://github.com/david-a-wheeler/metamath-test/pull/4

https://github.com/david-a-wheeler/metamath-test/pull/5

I have pushed the latest docker image with Hmm, the metamath-test improvements, and a new benchmarking script, to Dockerhub, so you can get and run it with

docker run -it akb74/metamath-cmds

I have no further activities planned with Hmm or metamath-test.  Next I plan to look at the claim that there is a large and easily addressed performance inefficiency in checkmm.cpp.

Hope this is helpful.  Thanks again to Mario for his assistance.

    Best regards,

        Antony