Hi Mario, Thanks! I didn't attempt to optimize for speed or use any parallelism, and on an older 32GB RAM laptop using a recent set.mm I'm seeing ~145,000 lines/second / 8 MB/second, with all of set.mm handled in about 5 seconds using a single core. (That's with Zig 0.7.1 in release-fast mode.)
My main goal is actually doing stuff (parsing statements, and use that for definition checking and 'modular Metamath'), and it is not about raw performance, so smm3 / Rust is still the best there probably. :-) That said, I do want to see how parallelism improves things. As I said, any feedback is welcome. Groetjes, <>< Marnix Op wo 5 mei 2021 om 16:59 schreef Mario Carneiro <[email protected]>: > Exciting! How is the performance? I would guess that a Zig verifier could > compete with the best. > > On Wed, May 5, 2021 at 10:51 AM Marnix Klooster <[email protected]> > wrote: > >> Hello all, >> >> In case anyone is interested, I'm not sure but I don't think I announced >> this earlier: Since almost a year I've been working on and mostly-off on a >> Metamath verifier in Zig (https://ziglang.org). And today I've reached >> the milestone of supporting the last missing feature (except for allowing >> '?' in a proof, which is not really important for me yet). >> >> The code is at https://github.com/marnix/zigmmverify; any feedback is >> welcome. >> >> Groetjes, >> <>< >> Marnix >> -- >> Marnix Klooster >> [email protected] >> >> -- >> 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 on the web visit >> https://groups.google.com/d/msgid/metamath/CAF7V2P_C7QcKP8b_rxvEO6e5uXTMpS6gySU-iVCiqLD1gCW5qQ%40mail.gmail.com >> <https://groups.google.com/d/msgid/metamath/CAF7V2P_C7QcKP8b_rxvEO6e5uXTMpS6gySU-iVCiqLD1gCW5qQ%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 on the web visit > https://groups.google.com/d/msgid/metamath/CAFXXJSvqg4vHT%2B4HmaBhHSMCTdE0-EX0vRyVr6_tn%3DYFGgJmGA%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAFXXJSvqg4vHT%2B4HmaBhHSMCTdE0-EX0vRyVr6_tn%3DYFGgJmGA%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- Marnix Klooster [email protected] -- 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 on the web visit https://groups.google.com/d/msgid/metamath/CAF7V2P_PM0_JE7zMQ61rFOYgX-RzUQc4RKqvLDAirE9SFwaBhg%40mail.gmail.com.
