metamath-exe does not use multithreading, but 30 seconds is not an unusually long time if you aren't paying close attention to memory management. I'm not sure what language you are using but this is probably where I would look for additional gains. Things like creating a very large number of small strings during parsing often leads to a performance cost like that.
On Fri, Oct 10, 2025 at 2:55 PM Marlo Bruder <[email protected]> wrote: > Hello metamath community, > > I had a question about verifiers, specifically: How long should it take > for a verifier to verify set.mm? Right now my verifier takes about 30 > seconds to verify set.mm, which is too long for my application (since the > verifier has to run every time you open a database in my proof assistant). > Using metamath-exe, verifying set.mm only takes about 5 seconds, so > faster speed is definitely possible. I have already optimized my verifier > code quite a lot and at this point the only improvement appears to be > adding multi-threading. Does anyone know whether metamath-exe uses > multi-threading? Or is my code simply too slow? > > Thanks for any answers in advance! > > Best regards, > Marlo Bruder > > -- > 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/06b8fa17-bdbb-40ce-ac78-910de280159en%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/06b8fa17-bdbb-40ce-ac78-910de280159en%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSv-dK6yHVTzcc5ae8mXB09rSAZBYoDp2YgJw6Zm4fX3Jw%40mail.gmail.com.
