Thank you for the suggestions. Yes, it can occur that keywords are in a comment, but that is consistent with other ITPs. As I am counting definitions + axioms in one bin, $a seems fine.
I agree with Mario that the compressed proofs are the right ones to count, though LOC is not too helpful of a metric. (apologies if you receive multiple responses, my first response never appeared (?)) On Friday, 6 June 2025 at 01:59:07 UTC+2 [email protected] wrote: > I think uncompressing is not really a good idea for this test, that just > bloats the file, and for comparison with other ITPs this would not be a > fair comparison, you would need to similarly pretty print the proof terms > there. I think the metric of LOC of the regular file (which in our case > means proofs are in compressed blocks) is the closest we have to a measure > here, representing approximately how much human typing went into the proof. > (Humans don't type the compressed proof of course, but the text they do > type, in a proof assistant like mmj2, is probably around a similar order of > magnitude to the compressed proof.) > > Besides, I don't think it matters much since the 1M cutoff was simply used > to select the systems to consider, and the numbers which are reported are > not about LOC but about number of theorems and definitions. > > On Thu, Jun 5, 2025 at 9:11 PM 'David A. Wheeler' via Metamath < > [email protected]> wrote: > >> >> >> > On Jun 5, 2025, at 11:56 AM, 'Fabian Huch' via Metamath < >> [email protected]> wrote: >> > >> > I am currently creating a comparison of large libraries of ITPs. I am >> only considering libraries with more than 1M (nonempty) LOC, of which I >> know (in alphabetical order): ACL2, HOL4, Isabelle, Lean, Metamath, Mizar, >> PVS, Rocq. >> > To that end, I want to approximate the number of definitions (incl. >> axioms; excl. abbreviations, instances, fixed values/constants, examples) >> and proven proper theorems (excl. automatically generated ones) by simple >> analysis of the sources (without running the system). >> >> Quick clarification: I didn't actually uncompress these databases (set.mm >> etc.) >> and measure their uncompressed length. That said, >> I'm pretty confident that uncompressed set.mm and iset.mm would be >1M >> just >> from eyeballing them. >> I'm not as sure about nf.mm and ql.mm, though that's plausible. >> >> If it's vital, I could uncompress and measure them. However, there's a >> *reason* >> we normally work with compressed proofs :-). Most other systems like Lean >> and Isabelle >> are happy with statements like "blast" that say "go rediscover the proof" >> without >> actually showing the steps. A fundamental differentiator about >> Metamath is that it *never* skips proof steps, so its proofs have steps >> others >> would skip over. That doesn't mean we hate other systems, but it's >> important >> to understand that is a key differentiator: *all* steps of a proof are >> always included. >> >> By "uncompress" I simply mean the sequence of statements used in each >> proof. >> If we truly uncompressed the proofs to show what humans can consider >> (that is, showing the resulting statement after each proof step), all 4 >> of those >> databases would *trivially* clear 1M lines, even if we skipped the syntax >> ("non-essential") >> proof steps that are in the database. >> >> (This is a resend, sorry if you got this twice.) >> >> --- David A. Wheeler >> >> -- >> 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/AC0905B3-1FBE-4113-AB63-2A3E370E2D6F%40dwheeler.com >> . >> > -- 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/1e413b6e-b50d-4c14-aeab-2ce283a198d9n%40googlegroups.com.
