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 -- 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%2BAST1FoZmfjKTmBJ5e9h20FOoh2OX4PnCn31yDAYFamdw%40mail.gmail.com.
