Karl Palmskog (Jun 29 2020 at 09:49): Karl Palmskog (Jun 29 2020 at 09:49):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):
Abstract:
We build a non-synthetic dataset from the largest repository of mechanised proofs
In text:
we have mined arguably the largest publicly-hosted repository of mechanised [...] proofs: the Achieve of Formal Proofs (AFP)
Enrico Tassi (Jun 29 2020 at 10:57):Hem, when I write "arguably" or "to the best of my knowledge" I really mean "I didn't have time to dig deeper" ;-)
Karl Palmskog (Jun 29 2020 at 10:58):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.
Enrico Tassi (Jun 29 2020 at 11:04):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.
Karl Palmskog (Jun 29 2020 at 11:05):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)
Emilio Jesús Gallego Arias (Jun 29 2020 at 11:07):@Karl Palmskog actually once we make a bit of progress on https://github.com/coq/coq/issues/9232 we could consider it a repos
Emilio Jesús Gallego Arias (Jun 29 2020 at 11:07):I'm following the same model there than https://github.com/ocamllabs/duniverse
Karl Palmskog (Jun 29 2020 at 11:09):@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
Karl Palmskog (Jun 29 2020 at 11:11):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.
Karl Palmskog (Jun 29 2020 at 11:15):in any case, it's very clear we need something like this, probably for all of: Coq's CI, released, duniverse
Pierre-Marie Pédrot (Jun 29 2020 at 11:44):@Emilio Jesús Gallego Arias ironically, the "universe" of Coq developments is likely not to exist due to universe constraints
Bas Spitters (Jun 29 2020 at 11:50):I guess it may the largest with some claim of coherence...?
Karl Palmskog (Jun 29 2020 at 11:53):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...
Karl Palmskog (Jun 29 2020 at 11:58):@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...
Enrico Tassi (Jun 30 2020 at 13:55):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: May 31 2023 at 02:31 UTC