[ fix agda#2086 ] new web deployment strategy (agda#2147)

jamesmckinna · Nov 4, 2023 · 222c238 · 222c238
1 parent 6e375c2
commit 222c238
Show file tree

Hide file tree

Showing 5 changed files with 66 additions and 1 deletion.
diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
@@ -75,7 +75,7 @@ jobs:
              || '${{ github.base_ref }}' == 'master' ]]; then
             # Pick Agda version for master
             echo "AGDA_COMMIT=tags/v2.6.4" >> $GITHUB_ENV;
-            echo "AGDA_HTML_DIR=html" >> $GITHUB_ENV
+            echo "AGDA_HTML_DIR=html/master" >> $GITHUB_ENV
           elif [[ '${{ github.ref }}' == 'refs/heads/experimental' \
                || '${{ github.base_ref }}' == 'experimental' ]]; then
             # Pick Agda version for experimental
@@ -125,6 +125,7 @@ jobs:
         run: cabal update
 
       - name: Install alex & happy
+        if: steps.cache-cabal.outputs.cache-hit != 'true'
         run: |
           ${{ env.CABAL_INSTALL }} alex
           ${{ env.CABAL_INSTALL }} happy
@@ -177,6 +178,9 @@ jobs:
           rm -f '${{ env.AGDA_HTML_DIR }}'/*.css
           ${{ env.AGDA }} --html --html-dir ${{ env.AGDA_HTML_DIR }} index.agda
 
+          cp travis/* .
+          ./landing.sh
+
       - name: Deploy HTML
         uses: JamesIves/[email protected]
         if: ${{ success() && env.AGDA_DEPLOY }}

diff --git a/travis/agda-logo.svg b/travis/agda-logo.svg
diff --git a/travis/landing-bottom.html b/travis/landing-bottom.html
@@ -0,0 +1,4 @@
+      </ul>
+    </div>
+  </body>
+</html>
diff --git a/travis/landing-top.html b/travis/landing-top.html
@@ -0,0 +1,24 @@
+<html>
+
+  <head>
+    <title>Documention for the Agda standard library</title>
+  </head>
+
+  <body>
+
+    <div id="container" style="width:50%;min-width:500px;margin:auto">
+      <img src="agda-logo.svg" style="width:80px;float:right" />
+      <h1>Documention for the Agda standard library</h1>
+
+      <hr />
+
+      <h2>Development versions</h2>
+
+      <ul>
+        <li><a href="master">master</a></li>
+        <li><a href="experimental">experimental</a></li>
+      </ul>
+
+      <h2>Released versions</h2>
+
+      <ul>
diff --git a/travis/landing.sh b/travis/landing.sh
@@ -0,0 +1,17 @@
+set -eu
+set -o pipefail
+
+rm html/index.html
+
+cat landing-top.html >> landing.html
+
+find html/ -name "index.html" \
+  | grep -v "master\|experimental" \
+  | sort -r \
+  | sed 's|html/\([^\/]*\)/index.html|        <li><a href="\1">\1</a></li>|g' \
+  >> landing.html
+
+cat landing-bottom.html >> landing.html
+
+mv landing.html html/index.html
+mv agda-logo.svg html/
-Original file line number
+Diff line change
@@ -0,0 +1,4 @@
+          </ul>
+        </div>
+      </body>
+    </html>