Post #2479120
2026-05-09 20:15 UTC
@olynch@mathstodon.xyz @MartinEscardo@mathstodon.xyz I do, but I'm not sure how relevant it is to your interest in parsing. The verifier I'm calling the slow one is https://github.com/metamath/metamath-exe and the one I'm calling the fast one is https://github.com/metamath/metamath-knife . The number one reason for the difference in speed, as I understand it, is that metamath-exe is single threaded (having been written before typical users had more than one processor) and metamath-knife is multi threaded.
Replies (1)
-
@soaproot@sfba.social 2026-05-09 20:23
@olynch@mathstodon.xyz @MartinEscardo@mathstodon.xyz The error handling which is different is that if I take any theorem and remove the distinct variable constraint ($d), metamath-knife says 'Disjoint variable constraint violated' and no further details. metamath-exe gives 'Variables "A" and "f" do not have a disjoint variable requirement in the assertion being proved' (and likewise for every pair of variables missing the constraint).