#!/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
