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
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.
I did it some time ago by manually checking out all repos and using
git ls-files IIRC
It was more like 4 million LoC
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.
@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
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.
we do have people versioning automatically generated code, don't we?
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
IIRC we have projects that have hundreds of automatically generated .v files... if we count these it's a slippery slope.
(these project make the poor coq_makefile/coqdep choke)
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
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: Feb 02 2023 at 13:03 UTC