From ba61dfd69504ec6263a9dee9931d93adeb6f3142 Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Mon, 7 Jul 2025 21:52:08 +0200
Subject: Initialize repository

---
 cloc-rocq.sh | 150 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 150 insertions(+)
 create mode 100755 cloc-rocq.sh

(limited to 'cloc-rocq.sh')

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)
+'
-- 
cgit v1.2.3