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 @@
+#!/bin/bash
+cloc --by-file ./theories --include-ext=v --json | jq -r '
+        def categories: {
+                "./theories/lambda/operational.v": {
+                        component: "(2) LambdaLang",
+                        category1: "(1) Operational semantics",
+                        category2: "General",
+                },
+                "./theories/lambda/operational_props.v": {
+                        component: "(2) LambdaLang",
+                        category1: "(1) Operational semantics",
+                        category2: "Properties",
+                },
+                "./theories/lambda/interp.v": {
+                        component: "(2) LambdaLang",
+                        category1: "(2) Interpreter",
+                        category2: "General",
+                },
+                "./theories/lambda/interp_proofs.v": {
+                        component: "(2) LambdaLang",
+                        category1: "(2) Interpreter",
+                        category2: "Theorem + proofs",
+                },
+                "./theories/dynlang/operational.v": {
+                        component: "(3) DynLang",
+                        category1: "(1) Operational semantics",
+                        category2: "General",
+                },
+                "./theories/dynlang/operational_props.v": {
+                        component: "(3) DynLang",
+                        category1: "(1) Operational semantics",
+                        category2: "Properties",
+                },
+                "./theories/dynlang/interp.v": {
+                        component: "(3) DynLang",
+                        category1: "(2) Interpreter",
+                        category2: "General",
+                },
+                "./theories/dynlang/interp_proofs.v": {
+                        component: "(3) DynLang",
+                        category1: "(2) Interpreter",
+                        category2: "Theorem + proofs",
+                },
+                "./theories/dynlang/equiv.v": {
+                        component: "(3) DynLang",
+                        category1: "(4) Extra",
+                        category2: "Equivalence with LambdaLang",
+                },
+                "./theories/evallang/operational.v": {
+                        component: "(4) EvalLang",
+                        category1: "(1) Operational semantics",
+                        category2: "General",
+                },
+                "./theories/evallang/operational_props.v": {
+                        component: "(4) EvalLang",
+                        category1: "(1) Operational semantics",
+                        category2: "Properties",
+                },
+                "./theories/evallang/interp.v": {
+                        component: "(4) EvalLang",
+                        category1: "(2) Interpreter",
+                        category2: "General",
+                },
+                "./theories/evallang/interp_proofs.v": {
+                        component: "(4) EvalLang",
+                        category1: "(2) Interpreter",
+                        category2: "Theorem + proofs",
+                },
+                "./theories/evallang/tests.v": {
+                        component: "(4) EvalLang",
+                        category1: "(3) Tests",
+                        category2: "General",
+                },
+                "./theories/nix/floats.v": {
+                        component: "(5) NixLang",
+                        category1: "(4) Extra",
+                        category2: "General",
+                },
+                "./theories/nix/operational.v": {
+                        component: "(5) NixLang",
+                        category1: "(1) Operational semantics",
+                        category2: "General",
+                },
+                "./theories/nix/operational_props.v": {
+                        component: "(5) NixLang",
+                        category1: "(1) Operational semantics",
+                        category2: "Properties",
+                },
+                "./theories/nix/notations.v": {
+                        component: "(5) NixLang",
+                        category1: "(4) Extra",
+                        category2: "General",
+                },
+                "./theories/nix/interp.v": {
+                        component: "(5) NixLang",
+                        category1: "(2) Interpreter",
+                        category2: "General",
+                },
+                "./theories/nix/interp_proofs.v": {
+                        component: "(5) NixLang",
+                        category1: "(2) Interpreter",
+                        category2: "Theorem + proofs",
+                },
+                "./theories/nix/tests.v": {
+                        component: "(5) NixLang",
+                        category1: "(3) Tests",
+                        category2: "General",
+                },
+                "./theories/nix/wp.v": {
+                        component: "(5) NixLang",
+                        category1: "(4) Extra",
+                        category2: "General",
+                },
+                "./theories/nix/wp_examples.v": {
+                        component: "(5) NixLang",
+                        category1: "(4) Extra",
+                        category2: "General",
+                },
+                "./theories/utils.v": {
+                        component: "(1) Shared",
+                        category1: "General",
+                        category2: "General",
+                },
+                "./theories/res.v": {
+                        component: "(1) Shared",
+                        category1: "General",
+                        category2: "General",
+                },
+        };
+        def add_cat_data:
+                { key, value: ({loc: .value.code} + categories[.key]) };
+        def categorize_by(key):
+                group_by(.value[key]) | map({ key: .[0].value[key], value: . }) | from_entries;
+        def spaces: if . == 0 then "" else " " + (. - 1 | spaces) end;
+        def pretty(ind):
+                if (. | type) == "number" then
+                        . | tostring
+                else
+                        to_entries | reduce .[] as $item (""; . + "\n" + (ind | spaces) + $item.key + ": " + ($item.value | pretty(ind + 2)))
+                end;
+        .SUM.code as $sum | del(.header, .SUM) | with_entries(add_cat_data) | to_entries
+        | categorize_by("component") | map_values(categorize_by("category1"))
+        | map_values(map_values(categorize_by("category2") | map_values(map(.value.loc) | add)))
+        | map_values(map_values(. + { TOTAL: to_entries | map(.value) | add }))
+        | map_values(. + { TOTAL: to_entries | map(.value.TOTAL) | add })
+        | . + { TOTAL: to_entries | map(.value.TOTAL) | add }
+        | if .TOTAL == $sum then . else error("internal error: calculated total \(.TOTAL) does not match provided sum \($sum)") end
+        | "Lines of code for the different parts of the Rocq development:" + pretty(0)
+'

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
	3	cloc --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	'