aboutsummaryrefslogtreecommitdiffstats
path: root/explorer
diff options
context:
space:
mode:
authorRutger Broekhoff2025-07-07 21:52:08 +0200
committerRutger Broekhoff2025-07-07 21:52:08 +0200
commitba61dfd69504ec6263a9dee9931d93adeb6f3142 (patch)
treed6c9b78e50eeab24e0c1c09ab45909a6ae3fd5db /explorer
downloadverified-dyn-lang-interp-ba61dfd69504ec6263a9dee9931d93adeb6f3142.tar.gz
verified-dyn-lang-interp-ba61dfd69504ec6263a9dee9931d93adeb6f3142.zip
Initialize repository
Diffstat (limited to 'explorer')
-rw-r--r--explorer/.gitignore2
-rwxr-xr-xexplorer/generate.sh140
-rwxr-xr-xexplorer/tree.sh17
-rwxr-xr-xexplorer/upload-new.sh16
4 files changed, 175 insertions, 0 deletions
diff --git a/explorer/.gitignore b/explorer/.gitignore
new file mode 100644
index 0000000..94529d8
--- /dev/null
+++ b/explorer/.gitignore
@@ -0,0 +1,2 @@
1dest/
2dest-*/
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
3shopt -s globstar
4set -eu
5set -o pipefail
6
7rm -rf dest
8mkdir -p dest
9TREE="$(pwd)/tree.sh"
10destdir="$(pwd)/dest"
11commit="$(git rev-parse --short HEAD)"
12
13cd ../theories
14for 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"
140done
diff --git a/explorer/tree.sh b/explorer/tree.sh
new file mode 100755
index 0000000..1620d2d
--- /dev/null
+++ b/explorer/tree.sh
@@ -0,0 +1,17 @@
1#!/bin/bash
2
3tree -J ../theories -P "*.v" | jq --arg "current" "$1" -r '
4 ("../" * ($current | [ scan("/+") ] | length)) as $prefix |
5 def make_item_link(prefix):
6 (if $current == prefix + .name then " class=\"current\"" else "" end) as $extra |
7 "<a href=\"\($prefix)\(prefix)\(.name | @uri).html\"\($extra)>\(.name | @html)</a>";
8 def handle_item(prefix):
9 if .type == "directory" then
10 "<li>\(.name | @html)<ul>" +
11 (.name as $dir | .contents | map(handle_item("\(prefix)\($dir)/")) | add) +
12 "</ul></li>"
13 else
14 "<li>\(make_item_link(prefix))</li>"
15 end;
16 .[0].contents | map(handle_item("")) | add
17'
diff --git a/explorer/upload-new.sh b/explorer/upload-new.sh
new file mode 100755
index 0000000..7873aa2
--- /dev/null
+++ b/explorer/upload-new.sh
@@ -0,0 +1,16 @@
1#!/bin/bash
2
3set -eu
4set -o pipefail
5
6commit="$(git rev-parse --short HEAD)"
7
8[ -e "dest-$commit" ] && {
9 echo "Revision $commit may have already been uploaded. Delete the directory dest-$commit to force re-upload.";
10 exit 1
11}
12
13./generate.sh
14mv dest "dest-$commit"
15mcli cp --recursive --checksum sha256 dest-$commit/* s3-default-par/verified-dyn-lang-interp/$commit/theories/
16echo "Base URL (for \\rocqbaseurl): https://s3.fr-par.scw.cloud/verified-dyn-lang-interp/$commit/"
generated by cgit v1.2.3 (git 2.49.0) at 2025-12-16 18:21:45 +0000