I'd suggest profiling the verifier to see what's taking up the most time while it works. Without data, we can keep arguing over different qualities ad nauseam. Sometimes the solution is simpler and less expected than it first appears.
Matthew House On Fri, Oct 10, 2025, 9:07 AM Marlo Bruder <[email protected]> wrote: > Hi Mario, > > interesting. I use Rust and the only time a new String is created is when > a substitution result is pushed onto the stack, at which point creating a > new String is pretty much unavoidable, right? At all other points I'm > working with &str, which do not allocate any additional memory. > > Best regards, > Marlo Bruder > > On Friday, October 10, 2025 at 2:58:34 PM UTC+2 [email protected] wrote: > >> 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/1d4f4328-92e2-46e3-aca0-042fe909306dn%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/1d4f4328-92e2-46e3-aca0-042fe909306dn%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/CADBQv9bbBeKDBMnPVs-t5vPZu%2BXMTGPjQs1YXHi1xQDpPrwBqw%40mail.gmail.com.
