Thanks for the useful suggestions, everyone. After quickly looking into both profiling and multi-threading, I decided that multi-threading seemed like the easier approach and now I've got the time below 4 seconds. I guess the mystery of why my verifier is taking so long can be solved by someone else once my proof assistant is published.
Best regards, Marlo Bruder On Friday, October 10, 2025 at 6:11:09 PM UTC+2 [email protected] wrote: > Don't aim at metamath.exe level of performance, it's the fastest > single-threaded verifier available (with only the multi-threaded > metamath-knife outperforming it). Aim at mmverifier.py or one of the > checkmm programs if you want respectable. > > And yes, use a profiler. It's potentially a waste of time > optimising until you can see which part of your program is slow. In spite > of the fact I should have known better, I recently made that mistake > initially when looking at the performance of checkmm.cpp. And yes it was > string-related. It usually is, especially with verifiers and the tens of > millions of tokens in set.mm. > > Best regards, > > Antony > > > On Fri, Oct 10, 2025 at 2:41 PM Matthew House <[email protected]> > wrote: > >> 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 >> >> <https://groups.google.com/d/msgid/metamath/CADBQv9bbBeKDBMnPVs-t5vPZu%2BXMTGPjQs1YXHi1xQDpPrwBqw%40mail.gmail.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/2c080bed-05c4-4f8d-b40f-3980a189fe4dn%40googlegroups.com.
