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
On Thu, Oct 16, 2025 at 2:07 PM Mario Carneiro <[email protected]> wrote:
>
>
> On Fri, Oct 10, 2025, 18:11 Antony Bartlett <[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).
>>
>
> I believe this is not true, metamath-knife is faster single-threaded than
> metamath.exe. The main point of the paragraph is true though.
>
> --
> 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/CAFXXJSu4XfV3UhA%2BeeuZUF0t2bF16Z8t%2BSxOd%3DL8XH7-peUyUg%40mail.gmail.com
> <https://groups.google.com/d/msgid/metamath/CAFXXJSu4XfV3UhA%2BeeuZUF0t2bF16Z8t%2BSxOd%3DL8XH7-peUyUg%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%2BCaYWxrfaEjehkDz1NqayQuFVY09yhPB0kGLi8j7kCSFA%40mail.gmail.com.
