Command line tools in Docker

[Antony Bartlett]

I have created a Docker image containing the set.mm repository and a number of command line tools

• metamath.exe
• checkmm
• metamath-knife
• mmj2
• mmverify.py

Plus a few of my own (checkmm-ts, prettier-plugin-mm (beta), alt-mm (beta)).

If you have Docker installed, you can download and run it with the following command

    docker run -it akb74/metamath-cmds

Which is good at the moment, but likely to date quickly (think how often set.mm gets updated), and it seems like overkill at this stage to have it updating automatically.  So in future it might make more sense to use the git repository and follow the instructions there.

    https://github.com/Antony74/metamath-docker

I think this will probably be of some interest, and possibly convenience, but even I would be hard pressed to say what value or utility it brings at the moment.  Of the two fully featured programs there, only metamath.exe is intended to be used from the command line.  I think you can get at most of mmj2's functionality from the command line, but in a manner that's intended for automation rather than command line use, and we can't start its powerful graphical user interface from this Docker container.  The other programs are validators, so the main use might be to compare them.  This is not a good place to produce benchmarks however, due to the overhead of running them inside a Docker container.  I will give some timings below, however.

I'm not sure about this, but the Dockerfile arguably might represent formal instructions for installing the command line tools that can quickly and conveniently be verified as working (or broken).  (that sounds like a good idea... where have I heard that before? ;-).  As such it might be worth consulting if you get stuck installing a metamath program.

The first question I have to ask is: are there any important metamath command line tools that I've missed? (I got the list from the Travis builds on the set.mm repo).

My second question is: have I succeeded in obtaining all the command line tools correctly from their official released sources?  In particular metamath-knife, mmverify.py, and mmj2 are cloned from github.  Exactly details of what I've used can be found in the Dockerfile https://github.com/Antony74/metamath-docker/blob/main/Dockerfile

I think it's also worth noting that metamath.exe as obtained from us.metamath.org/downloads does not appear to have been updated this year (and as such still lists Norm's email address for tech support in a couple of places).

Finally, here are the timing's I promised.  All the runs I've done have been in the same ballpark, but if I wanted to be precise I suppose I should have done this a number of times and taken averages.

I have a Windows 11 Asus laptop (Intel core i7 1.3GHz, 8GB RAM)

Natively it runs checkmm-ts on set.mm in 9.8s

0.7s - metamath-knife

7s - mmj2

8.4s - metamath.exe

11.2s - checkmm-ts

35.5s - checkmm

51.3s - mmverify.py

For work I have a MacOS Big Sur MacBook Pro (2.4 GHz 8-Core Intel Core i9, 32GB RAM)

Natively it runs checkmm-ts on set.mm in 9.6s

0.6s - metamath-knife

6.4s - mmj2

6.7s - metamath.exe

11.7s - checkmm-ts

32.2s - mmverify.py

33.1s - checkmm

    Best regards,

        Antony