Question about verifier speed

[Marlo Bruder]

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

[Mario Carneiro]

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.

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/06b8fa17-bdbb-40ce-ac78-910de280159en%40googlegroups.com.

[Marlo Bruder]

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

[Matthew House]

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

To view this discussion visit https://groups.google.com/d/msgid/metamath/1d4f4328-92e2-46e3-aca0-042fe909306dn%40googlegroups.com.

[Antony Bartlett]

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

To view this discussion visit https://groups.google.com/d/msgid/metamath/CADBQv9bbBeKDBMnPVs-t5vPZu%2BXMTGPjQs1YXHi1xQDpPrwBqw%40mail.gmail.com.

[Marlo Bruder]

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

[Mario Carneiro]

On Fri, Oct 10, 2025, 18:11 Antony Bartlett <a...@akb.me.uk> 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).

I believe this is not true, metamath-knife is faster single-threaded than metamath.exe. The main point of the paragraph is true though. 

[Antony Bartlett]

That's cool - it hadn't occurred to me that metamath-knife could be run single-threaded.   I believe, the command for this is:

metamath-knife --jobs 1 --verify set.mm

And oddly I'm not seeing any significant change in performance when I run it.  Indeed, the only way I can tell the --jobs parameter is doing anything at all is that I can slow it down by telling it to spawn an unreasonably large number of threads.

    Best regards,

        Antony

--

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 metamath+u...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/metamath/CAFXXJSu4XfV3UhA%2BeeuZUF0t2bF16Z8t%2BSxOd%3DL8XH7-peUyUg%40mail.gmail.com.