Stream: Miscellaneous

Topic: Size of proof repositories


view this post on Zulip 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)

view this post on Zulip 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" ;-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 29 2020 at 11:07):

I'm following the same model there than https://github.com/ocamllabs/duniverse

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bas Spitters (Jun 29 2020 at 11:50):

I guess it may the largest with some claim of coherence...?

view this post on Zulip 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...

view this post on Zulip 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...

view this post on Zulip 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: Aug 19 2022 at 19:03 UTC