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/CAFXXJSutmGfpMZAEHT4D%3DAFhDUbh20EpuhvZuHO1N6r3g7SXCQ%40mail.gmail.com.
