From ba61dfd69504ec6263a9dee9931d93adeb6f3142 Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Mon, 7 Jul 2025 21:52:08 +0200 Subject: Initialize repository --- explorer/.gitignore | 2 + explorer/generate.sh | 140 +++++++++++++++++++++++++++++++++++++++++++++++++ explorer/tree.sh | 17 ++++++ explorer/upload-new.sh | 16 ++++++ 4 files changed, 175 insertions(+) create mode 100644 explorer/.gitignore create mode 100755 explorer/generate.sh create mode 100755 explorer/tree.sh create mode 100755 explorer/upload-new.sh (limited to 'explorer') diff --git a/explorer/.gitignore b/explorer/.gitignore new file mode 100644 index 0000000..94529d8 --- /dev/null +++ b/explorer/.gitignore @@ -0,0 +1,2 @@ +dest/ +dest-*/ 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 " + + + + $file + + + +
+
+

Verified Interpreters for Dynamic Languages

+ with Applications to the Nix Expression Language +
+
+ Rocq Mechanization + Commit $commit +
+
+
+ +
' >> "$destfile" + python -m pygments -fhtml -lcoq -Oanchorlinenos,linenos,linespans=line "$file" >> "$destfile" + echo ' +
+
+ + +' >> "$destfile" +done 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 @@ +#!/bin/bash + +tree -J ../theories -P "*.v" | jq --arg "current" "$1" -r ' + ("../" * ($current | [ scan("/+") ] | length)) as $prefix | + def make_item_link(prefix): + (if $current == prefix + .name then " class=\"current\"" else "" end) as $extra | + "\(.name | @html)"; + def handle_item(prefix): + if .type == "directory" then + "
  • \(.name | @html)
    • " + else + "
  • \(make_item_link(prefix))
    • " + end; + .[0].contents | map(handle_item("")) | add +' 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 @@ +#!/bin/bash + +set -eu +set -o pipefail + +commit="$(git rev-parse --short HEAD)" + +[ -e "dest-$commit" ] && { + echo "Revision $commit may have already been uploaded. Delete the directory dest-$commit to force re-upload."; + exit 1 +} + +./generate.sh +mv dest "dest-$commit" +mcli cp --recursive --checksum sha256 dest-$commit/* s3-default-par/verified-dyn-lang-interp/$commit/theories/ +echo "Base URL (for \\rocqbaseurl): https://s3.fr-par.scw.cloud/verified-dyn-lang-interp/$commit/" -- cgit v1.2.3