> I'm still not clear on the difference between running metamath-knife with
--verify and without, but I am very satisfied with this outcome, and
grateful for your assistance.
Running with --verify makes metamath-knife act like a traditional verifier:
it checks correctness of the metamath theorems
Thanks for looking at that, Mario, that's really helpful. I have added
hyperfine to the metamath-cmds container (it's in github, I'll push to
dockerhub later). The 'warm up' functionality is particularly useful as
--verify seems particularly susceptible to cold starts. I've taken some
As far as I know and last I checked, metamath-knife can check set.mm in
sub-one-second with verification enabled, and about half a second with
verification disabled. It's possible that things have changed due to the
growth of set.mm?
Just checked again:
$ cargo build --release
$ hyperfine -w 2
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
