On Sun, May 9, 2021 at 10:18 AM vvs <[email protected]> wrote: > it has quite competitive performance. It's not quite as impressive as >> smm3, but it can compile set.mm in 10-12 seconds so I'm quite happy with >> it. >> > > Benchmarking is a murky business, it pretty much depends on the system. > I've got 39.5s (mm-lean4) vs. 18s (canonical metamath). Just for the > record, not that I really care. Proving results about MM here is much more > important, IMHO. >
Actually there was a bug in the original version, it wasn't checking DV conditions correctly. The correct code has more loops in the hottest part of the code, so it impacted performance quite a bit; I currently get about 17 seconds on set.mm (vs 9.8 seconds for metamath.exe), which actually seems pretty close to your numbers if we assume your system just has a lower clock speed than mine. > -- 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/CAFXXJStcG7EqgKdQAEq4EJWqtrYPD8M0XzHDQ9GW%2BJ5xcOW4_A%40mail.gmail.com.
