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.
