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/CAJ48g%2BDr3_z5Ewptd6M9PJYRBLqBrRNAiTX3EFvwaXrq4HxxNw%40mail.gmail.com.
