> 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. P.S. Still it would be interesting to compare that with Coq or Agda. -- 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/7a533c4d-a924-44d8-b738-fbe1b8cb18f1n%40googlegroups.com.
