I've figured out the main reason why checkmm.cpp <https://us.metamath.org/other.html#verifiers> (Eric Schmidt, 2010) is slower than my 2022 TypeScript <https://www.npmjs.com/package/checkmm>port <https://www.npmjs.com/package/checkmm> of it. About twice as slow last time I posted benchmarks.
JavaScript objects are hashmaps with O(1) get/put average complexity (and an O(n) worse-case). checkmm.cpp is using ordered std::set and std::map with an O(log(n)) get/put complexity. (Myth of RAM <https://www.ilikebigbits.com/2014_04_21_myth_of_ram_1.html> notwithstanding, as mentioned here by Mario in 2022) That matters when we're looking up a theorem amongst the many in set.mm. If I change the most important lookups to std::unordered_set and std::unordered_map... https://github.com/Antony74/checkmm-ts/commit/e6e2f46b3514d8688cc6af796f82d6f59aeae098 ...It still hasn't caught up, but I've closed the gap substantially, *Benchmark 1*: metamath-knife --verify set.mm Time (*mean* ± σ): *641.1 ms* ± 3.4 ms [User: 586.5 ms, System: 54.6 ms] Range (min … max): 637.8 ms … 647.6 ms 10 runs *Benchmark 1*: echo -e "LoadFile,set.mm\nVerifyProof,*" > params.txt && mmj2 -f params.txt Time (*mean* ± σ): * 3.125 s* ± 0.020 s [User: 6.873 s, System: 0.270 s] Range (min … max): 3.094 s … 3.152 s 10 runs *Benchmark 1*: metamath "READ set.mm" "VERIFY PROOF *" "exit" Time (*mean* ± σ): * 3.932 s* ± 0.050 s [User: 3.768 s, System: 0.163 s] Range (min … max): 3.872 s … 4.028 s 10 runs *Benchmark 1*: checkmm set.mm Time (*mean* ± σ): * 6.132 s* ± 0.049 s [User: 7.250 s, System: 0.300 s] Range (min … max): 6.075 s … 6.243 s 10 runs *Benchmark 1*: checkmmc set.mm Time (*mean* ± σ): * 7.739 s* ± 0.147 s [User: 6.493 s, System: 1.246 s] Range (min … max): 7.520 s … 7.964 s 10 runs *Benchmark 1*: python3 mmverify.py set.mm Time (*mean* ± σ): *19.726 s* ± 0.185 s [User: 19.535 s, System: 0.190 s] Range (min … max): 19.557 s … 20.079 s 10 runs Benchmarks generated with the Metamath command line tools <https://github.com/Antony74/metamath-docker/tree/main> I have in Docker. I've been mulling it over for a while, because much as I love TypeScript, I know it's not faster than C++. I thought it was going to turn out to be reference-counted vs. garbage-collected strings, to be honest, and I thought I could do something about that, but it wasn't, and this is what I found when I finally got around to looking at it. The other thing I've been mulling over is creating a collection of .mm files which provide full code coverage of checkmm-ts (one file for each of the seventy or so error messages, and maybe four for happy paths). They could then be run against other verifiers too. I haven't looked at starting this, but I thought it was worth mentioning in light of other recent conversations about enhancing the test suite. 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 visit https://groups.google.com/d/msgid/metamath/CAJ48g%2BBNT6KQMGEgQb73U%2BQNTH-g%2B%2BviK-XmM2xcLge%2B97dwtA%40mail.gmail.com.
