Karl Palmskog (Jun 15 2020 at 19:02): 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.
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
Maxime Dénès (Jun 15 2020 at 19:17):It was more like 4 million LoC
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.
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
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.
Pierre-Marie Pédrot (Jun 15 2020 at 21:27):we do have people versioning automatically generated code, don't we?
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
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.
Enrico Tassi (Jun 15 2020 at 21:41):(these project make the poor coq_makefile/coqdep choke)
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
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: Apr 20 2024 at 02:40 UTC