aboutsummaryrefslogtreecommitdiffstats
path: root/cloc-rocq.sh
diff options
context:
space:
mode:
authorRutger Broekhoff2025-07-07 21:52:08 +0200
committerRutger Broekhoff2025-07-07 21:52:08 +0200
commitba61dfd69504ec6263a9dee9931d93adeb6f3142 (patch)
treed6c9b78e50eeab24e0c1c09ab45909a6ae3fd5db /cloc-rocq.sh
downloadverified-dyn-lang-interp-ba61dfd69504ec6263a9dee9931d93adeb6f3142.tar.gz
verified-dyn-lang-interp-ba61dfd69504ec6263a9dee9931d93adeb6f3142.zip
Initialize repository
Diffstat (limited to 'cloc-rocq.sh')
-rwxr-xr-xcloc-rocq.sh150
1 files changed, 150 insertions, 0 deletions
diff --git a/cloc-rocq.sh b/cloc-rocq.sh
new file mode 100755
index 0000000..1019af3
--- /dev/null
+++ b/cloc-rocq.sh
@@ -0,0 +1,150 @@
1#!/bin/bash
2
3cloc --by-file ./theories --include-ext=v --json | jq -r '
4 def categories: {
5 "./theories/lambda/operational.v": {
6 component: "(2) LambdaLang",
7 category1: "(1) Operational semantics",
8 category2: "General",
9 },
10 "./theories/lambda/operational_props.v": {
11 component: "(2) LambdaLang",
12 category1: "(1) Operational semantics",
13 category2: "Properties",
14 },
15 "./theories/lambda/interp.v": {
16 component: "(2) LambdaLang",
17 category1: "(2) Interpreter",
18 category2: "General",
19 },
20 "./theories/lambda/interp_proofs.v": {
21 component: "(2) LambdaLang",
22 category1: "(2) Interpreter",
23 category2: "Theorem + proofs",
24 },
25 "./theories/dynlang/operational.v": {
26 component: "(3) DynLang",
27 category1: "(1) Operational semantics",
28 category2: "General",
29 },
30 "./theories/dynlang/operational_props.v": {
31 component: "(3) DynLang",
32 category1: "(1) Operational semantics",
33 category2: "Properties",
34 },
35 "./theories/dynlang/interp.v": {
36 component: "(3) DynLang",
37 category1: "(2) Interpreter",
38 category2: "General",
39 },
40 "./theories/dynlang/interp_proofs.v": {
41 component: "(3) DynLang",
42 category1: "(2) Interpreter",
43 category2: "Theorem + proofs",
44 },
45 "./theories/dynlang/equiv.v": {
46 component: "(3) DynLang",
47 category1: "(4) Extra",
48 category2: "Equivalence with LambdaLang",
49 },
50 "./theories/evallang/operational.v": {
51 component: "(4) EvalLang",
52 category1: "(1) Operational semantics",
53 category2: "General",
54 },
55 "./theories/evallang/operational_props.v": {
56 component: "(4) EvalLang",
57 category1: "(1) Operational semantics",
58 category2: "Properties",
59 },
60 "./theories/evallang/interp.v": {
61 component: "(4) EvalLang",
62 category1: "(2) Interpreter",
63 category2: "General",
64 },
65 "./theories/evallang/interp_proofs.v": {
66 component: "(4) EvalLang",
67 category1: "(2) Interpreter",
68 category2: "Theorem + proofs",
69 },
70 "./theories/evallang/tests.v": {
71 component: "(4) EvalLang",
72 category1: "(3) Tests",
73 category2: "General",
74 },
75 "./theories/nix/floats.v": {
76 component: "(5) NixLang",
77 category1: "(4) Extra",
78 category2: "General",
79 },
80 "./theories/nix/operational.v": {
81 component: "(5) NixLang",
82 category1: "(1) Operational semantics",
83 category2: "General",
84 },
85 "./theories/nix/operational_props.v": {
86 component: "(5) NixLang",
87 category1: "(1) Operational semantics",
88 category2: "Properties",
89 },
90 "./theories/nix/notations.v": {
91 component: "(5) NixLang",
92 category1: "(4) Extra",
93 category2: "General",
94 },
95 "./theories/nix/interp.v": {
96 component: "(5) NixLang",
97 category1: "(2) Interpreter",
98 category2: "General",
99 },
100 "./theories/nix/interp_proofs.v": {
101 component: "(5) NixLang",
102 category1: "(2) Interpreter",
103 category2: "Theorem + proofs",
104 },
105 "./theories/nix/tests.v": {
106 component: "(5) NixLang",
107 category1: "(3) Tests",
108 category2: "General",
109 },
110 "./theories/nix/wp.v": {
111 component: "(5) NixLang",
112 category1: "(4) Extra",
113 category2: "General",
114 },
115 "./theories/nix/wp_examples.v": {
116 component: "(5) NixLang",
117 category1: "(4) Extra",
118 category2: "General",
119 },
120 "./theories/utils.v": {
121 component: "(1) Shared",
122 category1: "General",
123 category2: "General",
124 },
125 "./theories/res.v": {
126 component: "(1) Shared",
127 category1: "General",
128 category2: "General",
129 },
130 };
131 def add_cat_data:
132 { key, value: ({loc: .value.code} + categories[.key]) };
133 def categorize_by(key):
134 group_by(.value[key]) | map({ key: .[0].value[key], value: . }) | from_entries;
135 def spaces: if . == 0 then "" else " " + (. - 1 | spaces) end;
136 def pretty(ind):
137 if (. | type) == "number" then
138 . | tostring
139 else
140 to_entries | reduce .[] as $item (""; . + "\n" + (ind | spaces) + $item.key + ": " + ($item.value | pretty(ind + 2)))
141 end;
142 .SUM.code as $sum | del(.header, .SUM) | with_entries(add_cat_data) | to_entries
143 | categorize_by("component") | map_values(categorize_by("category1"))
144 | map_values(map_values(categorize_by("category2") | map_values(map(.value.loc) | add)))
145 | map_values(map_values(. + { TOTAL: to_entries | map(.value) | add }))
146 | map_values(. + { TOTAL: to_entries | map(.value.TOTAL) | add })
147 | . + { TOTAL: to_entries | map(.value.TOTAL) | add }
148 | if .TOTAL == $sum then . else error("internal error: calculated total \(.TOTAL) does not match provided sum \($sum)") end
149 | "Lines of code for the different parts of the Rocq development:" + pretty(0)
150'
generated by cgit v1.2.3 (git 2.49.0) at 2025-10-13 20:47:49 +0000