checkmm.cpp

[Antony Bartlett]

I've figured out the main reason why checkmm.cpp (Eric Schmidt, 2010) is slower than my 2022 TypeScript port 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 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 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

[Eric Schmidt]

I wrote checkmm.cpp before C++11 was finished and so did not use the unordered_set/map from the standard library. I think it might be worthwhile to make this improvement in the version used in the CI pipeline.