1 files changed, 140 insertions, 0 deletions
diff --git a/explorer/generate.sh b/explorer/generate.sh
new file mode 100755
index 0000000..cf2b77a
--- /dev/null
+++ b/explorer/generate.sh
@@ -0,0 +1,140 @@
+#!/bin/bash
+shopt -s globstar
+set -eu
+set -o pipefail
+rm -rf dest
+mkdir -p dest
+TREE="$(pwd)/tree.sh"
+destdir="$(pwd)/dest"
+commit="$(git rev-parse --short HEAD)"
+cd ../theories
+for file in **/*.v; do
+        destfile="$destdir/$file.html"
+        mkdir -p "$(dirname "$destfile")"
+        echo "<!DOCTYPE html>
+        <html lang=\"en\">
+                <head>
+                        <meta charset=\"UTF-8\">
+                        <title>$file</title>
+                        <style>" >> "$destfile"
+        python -m pygments -S default -f html >> "$destfile"
+        echo "
+                        html { height: 100%; }
+                        body {
+                                font-family: sans-serif;
+                                margin: 0px;
+                                min-height: 100%;
+                                display: flex;
+                                flex-direction: column;
+                        }
+                        header {
+                                display: flex;
+                                padding: 0em 1em;
+                                border-bottom: 1px solid black;
+                        }
+                        nav {
+                                width: 200px;
+                                border-right: 1px solid black;
+                                min-height: 100%;
+                        }
+                        nav ul {
+                                list-style-type: none;
+                                padding-left: 1em;
+                        }
+                        nav ul:not(#top-dir) {
+                                border-left: 1px solid black;
+                        }
+                        nav li {
+                                font-family: monospace;
+                        }
+                        a { text-decoration: none; }
+                        a.current { font-weight: bold; }
+                        .row { display: flex; }
+                        .grow { flex-grow: 1; }
+                        .h1-like {
+                                display: block;
+                                margin-block: 0.67em;
+                                font-size: 2.00em;
+                                font-weight: bold;
+                        }
+                        #subtitle {
+                                display: block;
+                                margin-block: 0.83em;
+                                font-size: 1.50em;
+                        }
+                </style>
+        </head>
+        <body>
+                <header class=\"row\">
+                        <div class=\"grow\">
+                                <h1>Verified Interpreters for Dynamic Languages</h1>
+                                <span id=\"subtitle\">with Applications to the Nix Expression Language</span>
+                        </div>
+                        <div>
+                                <span class=\"h1-like\">Rocq Mechanization</span>
+                                <span>Commit $commit</span>
+                        </div>
+                </header>
+                <div class=\"row grow\">
+                        <nav>
+                                <ul id=\"top-dir\">
+" >> "$destfile"
+        $TREE "$file" >> "$destfile"
+        echo '
+                                </ul>
+                        </nav>
+                        <main class="grow">' >> "$destfile"
+        python -m pygments -fhtml -lcoq -Oanchorlinenos,linenos,linespans=line "$file" >> "$destfile"
+        echo '
+                        </main>
+                </div>
+                <script>
+                function highlightOne(lineno) {
+                        let el = document.getElementById("line-" + lineno);
+                        el.classList.add("hll");
+                }
+        
+                function scrollTo(lineno) {
+                        let el = document.getElementById("line-" + lineno);
+                        el.scrollIntoView();
+                }
+        
+                function highlight() {
+                        let frag = window.location.hash.substring(1);
+                        if (/^line-[0-9]+$/.test(frag)) {
+                                highlightOne(frag.substring(5));
+                                scrollTo(frag.substring(5));
+                        } else if (/^L[0-9]+$/.test(frag)) {
+                                highlightOne(frag.substring(1));
+                                scrollTo(frag.substring(1));
+                        } else if (/^L[0-9]+-L[0-9]+$/.test(frag)) {
+                                let matches = frag.match(/[0-9]+/g);
+                                let startLineno = Number(matches[0]);
+                                let endLineno = Number(matches[1]);
+                                for (let lineno = startLineno; lineno <= endLineno; lineno++) {
+                                        highlightOne(lineno);
+                                }
+                                scrollTo(startLineno);
+                        }
+                }
+        
+                function unhighlight() {
+                        for (const el of Array.from(document.getElementsByClassName("hll"))) {
+                                el.classList.remove("hll");
+                        }
+                }
+        
+                function rehighlight() {
+                        unhighlight();
+                        highlight();
+                }
+        
+                window.addEventListener("hashchange", rehighlight);
+                window.addEventListener("load", highlight);
+                </script>
+        </body>
+</html>' >> "$destfile"
+done

diff --git a/explorer/generate.sh b/explorer/generate.sh new file mode 100755 index 0000000..cf2b77a --- /dev/null +++ b/explorer/generate.sh
@@ -0,0 +1,140 @@
	1	#!/bin/bash
	2
	3	shopt -s globstar
	4	set -eu
	5	set -o pipefail
	6
	7	rm -rf dest
	8	mkdir -p dest
	9	TREE="$(pwd)/tree.sh"
	10	destdir="$(pwd)/dest"
	11	commit="$(git rev-parse --short HEAD)"
	12
	13	cd ../theories
	14	for file in */.v; do
	15	destfile="$destdir/$file.html"
	16	mkdir -p "$(dirname "$destfile")"
	17	echo "<!DOCTYPE html>
	18	<html lang=\"en\">
	19	<head>
	20	<meta charset=\"UTF-8\">
	21	<title>$file</title>
	22	<style>" >> "$destfile"
	23	python -m pygments -S default -f html >> "$destfile"
	24	echo "
	25	html { height: 100%; }
	26	body {
	27	font-family: sans-serif;
	28	margin: 0px;
	29	min-height: 100%;
	30	display: flex;
	31	flex-direction: column;
	32	}
	33	header {
	34	display: flex;
	35	padding: 0em 1em;
	36	border-bottom: 1px solid black;
	37	}
	38	nav {
	39	width: 200px;
	40	border-right: 1px solid black;
	41	min-height: 100%;
	42	}
	43	nav ul {
	44	list-style-type: none;
	45	padding-left: 1em;
	46	}
	47	nav ul:not(#top-dir) {
	48	border-left: 1px solid black;
	49	}
	50	nav li {
	51	font-family: monospace;
	52	}
	53	a { text-decoration: none; }
	54	a.current { font-weight: bold; }
	55	.row { display: flex; }
	56	.grow { flex-grow: 1; }
	57	.h1-like {
	58	display: block;
	59	margin-block: 0.67em;
	60	font-size: 2.00em;
	61	font-weight: bold;
	62	}
	63	#subtitle {
	64	display: block;
	65	margin-block: 0.83em;
	66	font-size: 1.50em;
	67	}
	68	</style>
	69	</head>
	70	<body>
	71	<header class=\"row\">
	72	<div class=\"grow\">
	73	<h1>Verified Interpreters for Dynamic Languages</h1>
	74	<span id=\"subtitle\">with Applications to the Nix Expression Language</span>
	75	</div>
	76	<div>
	77	<span class=\"h1-like\">Rocq Mechanization</span>
	78	<span>Commit $commit</span>
	79	</div>
	80	</header>
	81	<div class=\"row grow\">
	82	<nav>
	83	<ul id=\"top-dir\">
	84	" >> "$destfile"
	85	$TREE "$file" >> "$destfile"
	86	echo '
	87	</ul>
	88	</nav>
	89	<main class="grow">' >> "$destfile"
	90	python -m pygments -fhtml -lcoq -Oanchorlinenos,linenos,linespans=line "$file" >> "$destfile"
	91	echo '
	92	</main>
	93	</div>
	94	<script>
	95	function highlightOne(lineno) {
	96	let el = document.getElementById("line-" + lineno);
	97	el.classList.add("hll");
	98	}
	99
	100	function scrollTo(lineno) {
	101	let el = document.getElementById("line-" + lineno);
	102	el.scrollIntoView();
	103	}
	104
	105	function highlight() {
	106	let frag = window.location.hash.substring(1);
	107	if (/^line-[0-9]+$/.test(frag)) {
	108	highlightOne(frag.substring(5));
	109	scrollTo(frag.substring(5));
	110	} else if (/^L[0-9]+$/.test(frag)) {
	111	highlightOne(frag.substring(1));
	112	scrollTo(frag.substring(1));
	113	} else if (/^L[0-9]+-L[0-9]+$/.test(frag)) {
	114	let matches = frag.match(/[0-9]+/g);
	115	let startLineno = Number(matches[0]);
	116	let endLineno = Number(matches[1]);
	117	for (let lineno = startLineno; lineno <= endLineno; lineno++) {
	118	highlightOne(lineno);
	119	}
	120	scrollTo(startLineno);
	121	}
	122	}
	123
	124	function unhighlight() {
	125	for (const el of Array.from(document.getElementsByClassName("hll"))) {
	126	el.classList.remove("hll");
	127	}
	128	}
	129
	130	function rehighlight() {
	131	unhighlight();
	132	highlight();
	133	}
	134
	135	window.addEventListener("hashchange", rehighlight);
	136	window.addEventListener("load", highlight);
	137	</script>
	138	</body>
	139	</html>' >> "$destfile"
	140	done