On Mon, Oct 13, 2025 at 10:24 PM Antony Bartlett <[email protected]> wrote:
> I thought I'd made a mistake when I said metamath.exe was the fastest > single-threaded verifier the other day, because when I double-checked, mmj2 > has always been slightly faster. However, judging by how it fits nearly > seven seconds of user run-time into a total run time of 3.1 seconds, I'd > suggest it must be multi-threaded. So by a complete fluke, I may have been > correct about metamath.exe! > Nope, mmj2 is single-threaded, as is basically every verifier. metamath-knife / smm3 is the only verifier that has attempted to be multithreaded, it is quite complicated to do correctly. (That's not to say that it is only using one core; the Java runtime environment itself is multithreaded, e.g. in the garbage collector, so that may explain some parallelism. But mmj2 source code does not attempt to do anything with threads except to run the UI.) -- 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/CAFXXJSsY3CnrkpNm3-kMJvDqCZRzLM8Mp2PPGABOgQ%3DqzaumVg%40mail.gmail.com.
