Looks like Isabelle authors are saying the AFP is larger than the
released OPAM repo (which seems doubtful to me, given that even Coq's CI is larger than the AFP in terms of LOC):
We build a non-synthetic dataset from the largest repository of mechanised proofs
we have mined arguably the largest publicly-hosted repository of mechanised [...] proofs: the Achieve of Formal Proofs (AFP)
Hem, when I write "arguably" or "to the best of my knowledge" I really mean "I didn't have time to dig deeper" ;-)
well, it's unqualified "largest" in the abstract. It seems they are using "number of lemmas" as the metric, and they have around 204k. It shouldn't be too hard to get this measure for, say, all
released packages compatible with 8.11. For comparison, our dataset of MC 1.9.0 and around 20 more projects using MC had around 24k lemmas.
I'm not defending their claim, but I believe it is much harder for an Isabelle user than for you to extract such a figure from Coq. Even the "released" thing is Coq specific I guess.
Claudio Sacerdoti Coen's dataset of 49 opam packages shortly after 8.9.0 release apparently had ~48k lemmas (Besides MC itself with ~8k lemmas, doesn't seem to overlap much with our dataset)
@Karl Palmskog actually once we make a bit of progress on https://github.com/coq/coq/issues/9232 we could consider it a repos
I'm following the same model there than https://github.com/ocamllabs/duniverse
@Emilio Jesús Gallego Arias yes, that would allow very good snapshots of currently building Coq projects. But one also needs to make sure lemmas are counted the same. For example, we basically used
VernacStartTheoremProof in the AST, which works well for MC, but perhaps not for other less conventional projects like UniMath
in Isabelle they at least have a super-clear boundary between theorems and definitions, not so much here. For example, one could say that anything built with tactics counts as a theorem.
in any case, it's very clear we need something like this, probably for all of: Coq's CI,
@Emilio Jesús Gallego Arias ironically, the "universe" of Coq developments is likely not to exist due to universe constraints
I guess it may the largest with some claim of coherence...?
but shouldn't "duniverse" be ok, like Russell switched from "set" to "class", e.g., number n is defined as the class of all sets with n members. Unfortunately, I think that some Coq projects in
released etc. contain untrue admits...
@Enrico Tassi also, what do you think of the terminology of declarative vs. procedural/tactic proofs (Isabelle paper goes all in on "declarative")? In my mind, many MC proofs mix what Isabelle users would call declarative and tactic-based reasoning...
I'm not a big fan of the word declarative, I've never grasped completely when something stops being operational and becomes declarative. Eg
rewrite is what?
I prefer to say "forward steps" or "readable steps", in contrast to "operational" or "procedural" (all the rest). In particular the former kind of steps is something a non expert can read, while the latter is not. Under the wishful thinking that one day we will have super-fancy-stable automation, the portion of proofs made of "operational" code should shrink, while the rest should stay the same. In some sense "readable steps" are "for a human". This is hard to see in tiny proofs of 5 lines, but becomes very visible in large proofs.
Last, I don't think a tactic is necessarily in one of the two categories, it is more about how you use it. In particular
have H : property is readable,
have /view[thing /boom ->] := proof_term (more term) is procedural, and
have /pdivP[p pr_p p_dv_m1]: 1 < m! + 1. is a middle ground.
Last updated: Aug 19 2022 at 19:03 UTC