Automate SVG rendering in MkDocs

.github/workflows/ghcjs.yml

@@ -73,6 +73,7 @@ jobs:
           folder: dist
           target-folder: ${{ github.ref_name }}
           clean: false
+          single-commit: true
 
       - name: "📘 Publish JS \"binaries\""
         if: ${{ github.ref_name == 'main' && github.event_name == 'push' }}
@@ -81,3 +82,4 @@ jobs:
           token: ${{ secrets.GITHUB_TOKEN }}
           folder: dist
           clean: false
+          single-commit: true

.github/workflows/haddock.yml

@@ -59,3 +59,4 @@ jobs:
           github_token: ${{ secrets.GITHUB_TOKEN }}
           folder: dist/haddock
           target-folder: haddock
+          single-commit: true

.github/workflows/mkdocs.yml

@@ -17,6 +17,13 @@ jobs:
       - name: 📥 Checkout repository
         uses: actions/checkout@v3
 
+      - name: 🔨 Install rzk proof assistant
+        uses: jaxxstorm/action-install-gh-release@v1.10.0
+        with:
+          repo: fizruk/rzk
+          tag: v0.4.1
+          rename-to: rzk
+
       - name: 🔨 Build MkDocs
         uses: Tiryoh/actions-mkdocs@v0
         with:
@@ -37,6 +44,7 @@ jobs:
           folder: dist
           target-folder: ${{ github.ref_name }}
           clean: false
+          single-commit: true
 
       - name: 📘 Publish Generated MkDocs
         if: ${{ github.ref_name == 'main' }}
@@ -45,3 +53,4 @@ jobs:
           github_token: ${{ secrets.GITHUB_TOKEN }}
           folder: dist
           clean: false
+          single-commit: true

.gitignore

@@ -27,3 +27,5 @@ cabal.project.local~
 docs/site
 result
 .direnv
+venv
+__pycache__

docs/custom_theme/main.html

@@ -17,5 +17,11 @@
       hljs.addPlugin(new CopyButtonPlugin());
       hljs.highlightAll();
     </script>
+    <style>
+      svg.tope {
+        float: right;
+        clear: both;
+      }
+    </style>
     {{ super() }}
 {% endblock %}

docs/generate_svgs.py

@@ -0,0 +1,45 @@
+import re
+import logging
+import subprocess
+
+from mkdocs.structure.pages import Page
+from mkdocs.structure.files import Files
+from mkdocs.config.defaults import MkDocsConfig
+
+
+logger = logging.getLogger('mkdocs')
+rzk_code_block = re.compile(r'(^```\s*rzk[^\n]*\s+(.*?)\s+^```)', flags=re.MULTILINE | re.DOTALL)
+svg_element = re.compile(r'^(<svg.*?</svg>)', flags=re.MULTILINE | re.DOTALL)
+rzk_installed = True
+
+try:
+    # Capture output to prevent logging usage
+    subprocess.run('rzk', capture_output=True)
+except FileNotFoundError:
+    logger.warn('Rzk executable not found')
+    rzk_installed = False
+
+
+def on_page_markdown(md: str, page: Page, config: MkDocsConfig, files: Files) -> str:
+    if not rzk_installed: return md
+    # Some snippets can depend on terms defined in previous snippets, so we need to store them all
+    previous_snippets = ['#lang rzk-1\n#set-option "render" = "svg"\n\n']
+    # Since each snippet will contain previous ones, the previously printed SVGs should not be repeated
+    previous_svgs: set[str] = set()
+    code_blocks = rzk_code_block.findall(md)
+    for (fenced_block, code) in code_blocks:
+        previous_snippets.append(code.replace('#lang rzk-1', ''))
+        full_code = '\n'.join(previous_snippets).encode()
+        process = subprocess.run('rzk typecheck', capture_output=True, input=full_code)
+        if process.returncode != 0: continue
+
+        output = process.stderr.decode()
+        svgs: list[str] = svg_element.findall(output)
+        # One snippet might have more than one diagram, so we shouldn't just use svgs[-1]
+        # However, there is probably a more efficient way than iterating over all matches everytime
+        for svg in svgs:
+            if svg in previous_svgs: continue
+            previous_svgs.add(svg)
+            md = md.replace(fenced_block, svg + '\n\n' + fenced_block)
+
+    return md

docs/mkdocs.yml

@@ -25,3 +25,6 @@ theme:
   custom_dir: custom_theme/
 extra_css:
   - https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.7.0/styles/default.min.css
+
+hooks:
+  - generate_svgs.py

docs/requirements.txt

@@ -1 +1,2 @@
+mkdocs
 python-markdown-math

rzk/src/Rzk/TypeCheck.hs

@@ -2936,7 +2936,7 @@ renderCube
   -> (String -> Maybe RenderObjectData)
   -> String
 renderCube camera rotY renderDataOf' = unlines $ filter (not . null)
-  [ "<svg class=\"zoom\" style=\"float: right\" viewBox=\"-175 -200 350 375\" width=\"150\" height=\"150\">"
+  [ "<svg class=\"zoom tope\" viewBox=\"-175 -200 350 375\" width=\"150\" height=\"150\">"
   , intercalate "\n"
       [ "  <path d=\"M " <> show x1 <> " " <> show y1
                 <> " L " <> show x2 <> " " <> show y2