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. On Saturday, September 20, 2025 at 2:11:58 PM UTC-6 [email protected] wrote:
> 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/96c1fa02-d2c0-4e4e-8de0-558daed1ef0bn%40googlegroups.com.
