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 -- "target/release/metamath-knife -v set.mm" Benchmark 1: target/release/metamath-knife -v set.mm Time (mean ± σ): 1.367 s ± 0.052 s [User: 1.280 s, System: 0.085 s] Range (min … max): 1.307 s … 1.464 s 10 runs $ hyperfine -w 2 -- "target/release/metamath-knife set.mm" Benchmark 1: target/release/metamath-knife set.mm Time (mean ± σ): 199.7 ms ± 13.7 ms [User: 151.8 ms, System: 47.4 ms] Range (min … max): 185.6 ms … 236.6 ms 15 runs so a bit more than a second now, and without verification it's even less than I remember, probably because the default profile has more things disabled than there used to be. On Sat, Mar 16, 2024 at 5:59 PM Antony Bartlett <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/CAJ48g%2BASabinmU590eC41US0So42YSeuMdbR0GUwenj0P1Fd%2Bw%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJStBxNPJ04LwojKHnof-PZRnCBNTebgO9fd1U%2BpM%3DecujQ%40mail.gmail.com.
