From 52323b6a2614a4feec0b8e4d0bac41e2312f36e9 Mon Sep 17 00:00:00 2001 From: Lionel Rieg <lionel.rieg@univ-grenoble-alpes.fr> Date: Fri, 30 Apr 2021 23:01:26 +0200 Subject: [PATCH] Adding a metrics.txt file summaring line counts + updating .gitignore The metrics file should rather be generated... --- .gitignore | 1 + metrics.txt | 34 ++++++++++++++++++++++++++++++++++ 2 files changed, 35 insertions(+) create mode 100644 metrics.txt diff --git a/.gitignore b/.gitignore index f3d48613..cdc85f1d 100644 --- a/.gitignore +++ b/.gitignore @@ -18,6 +18,7 @@ package.tgz .nia.cache .nra.cache .coqdeps.d +.Makefile.d makefile Makefile makefile.bak diff --git a/metrics.txt b/metrics.txt new file mode 100644 index 00000000..1e456d16 --- /dev/null +++ b/metrics.txt @@ -0,0 +1,34 @@ +Formalization LOC (coqwc on spec + proof) +=============================================== +Util ++-- Coqlib & Co 2385 ++-- FSets + FMaps 4033 ++-- MMultiset 5807 +Core 1000 +Spaces ++-- Continuous spaces (R, R^2, etc.) 4490 ++-- Discrete spaces (graphs, ring, grid) 686 +Observations ++-- Multiset 293 ++-- Set 265 ++-- Other 68 +Models ++-- Rigid/flexible + equivalence 275 ++-- Continuous/discrete graphs 1187 +Case Studies ++-- Gathering + +-- common part 1407 + +-- Impossibility (R + general) 2029 + +-- SSYNC, R 1388 + +-- SSYNC, R^2 2307 + +-- Peleg + flexible 1293 + +-- Viglietta 407 ++-- Convergence + +-- Impossibility 578 + +-- Algorithm 170 ++-- Exploration + +-- Impossibility 474 + +-- Tower 203 ++-- Life-line 1592 +=============================================== +Total 31462 -- GitLab