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).
For Metamath, my approach would be to look at tokens in `.mm` files and count $a for axioms and $p for theorems. Is this reasonable or is there a better way? -- 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/114dd184-396f-4759-a386-828b86089418n%40googlegroups.com.
