Stream: Coq devs & plugin devs

Topic: lines of code in Coq's CI


view this post on Zulip Karl Palmskog (Jun 15 2020 at 19:02):

Is there an easy way to get the number of lines of code of all projects in Coq's CI? For example, as calculated by coqwc or cloc? I know that as per August 2019, there was around 2,2 million lines of code (as stated on p. 51 in Théo's thesis), and am interested in if there has been significant growth since then.

view this post on Zulip Maxime Dénès (Jun 15 2020 at 19:17):

I did it some time ago by manually checking out all repos and using git ls-files IIRC

view this post on Zulip Maxime Dénès (Jun 15 2020 at 19:17):

It was more like 4 million LoC

view this post on Zulip Emilio Jesús Gallego Arias (Jun 15 2020 at 19:48):

make ci-all -j 8 will give you a complete checkout in _build_ci, after that use your favorite tool ; yup, we should improve our CI management system as the above will also try to build all the CI.

view this post on Zulip Karl Palmskog (Jun 15 2020 at 21:22):

@Emilio Jesús Gallego Arias could one theoretically set up something like OMDoc exporting (using Sacerdoti Coen's plugin) for all CI projects without a ton of work? E.g., make it an optional trigger? I think this is what MKM people (Rabe) are asking in some emails I exchanged with them

view this post on Zulip Karl Palmskog (Jun 15 2020 at 21:26):

it could make Coq look good if we (have the possibility to) continually spit out "interoperable representations" of 4 million+ Coq LOC, e.g., for major releases. In contrast, since the OPAM repo takes time to update after a new major release, we currently look bad if people turn to that.

view this post on Zulip Pierre-Marie Pédrot (Jun 15 2020 at 21:27):

we do have people versioning automatically generated code, don't we?

view this post on Zulip Karl Palmskog (Jun 15 2020 at 21:35):

interesting in any case that Coq's CI doesn't have far to be double the size of Isabelle's AFP though (if the 4M figure is correct), current AFP stats say 2.5M LOC

view this post on Zulip Enrico Tassi (Jun 15 2020 at 21:41):

IIRC we have projects that have hundreds of automatically generated .v files... if we count these it's a slippery slope.

view this post on Zulip Enrico Tassi (Jun 15 2020 at 21:41):

(these project make the poor coq_makefile/coqdep choke)

view this post on Zulip Karl Palmskog (Jun 15 2020 at 21:44):

if one does theory exporting, there will be plenty of other chokepoints, e.g., Claudio et al mention specifically some incredibly big proof term in odd-order

view this post on Zulip Karl Palmskog (Jun 15 2020 at 21:46):

in software engineering, there is "test suite minimization", and some analogue is probably needed for Coq to make all that stuff work out


Last updated: Oct 16 2021 at 01:03 UTC