Add workflow for publishing Agda Metatheory site (#6223)

* Add workflow for publishing AGDA metatheory site

* wip

* wip

.github/workflows/plublish-metatheory-site.yml

@@ -0,0 +1,60 @@
+# This workflow publishes the Agda metatheory site to:
+#   https://intersectmbo.github.io/plutus/docs/metatheory/$version
+# Where $version should be a release version tag.
+# Optionally the $version branch can also be deployed to:
+#   https://intersectmbo.github.io/plutus/docs/metatheory/latest  
+
+name: ci
+
+on:
+  workflow_dispatch:
+    inputs:
+      version:
+        description: |
+          The release version tag. For example if $version == "1.29.0.0" then the 
+          current contents of the branch tagged "1.29.0.0" will be deployed to: 
+            https://intersectmbo.github.io/plutus/docs/metatheory/$version
+        required: true
+        type: string
+
+      latest: 
+        description: |
+          If true, then the $version branch will also be deployed to:
+            https://intersectmbo.github.io/plutus/docs/metatheory/latest
+          You want to leave this to true unless you are deploying old versions.
+        type: boolean
+        required: true 
+        default: true
+
+jobs:
+  deplopy-adga-metatheory-site:
+    name: "📚 Deplopy Adga Metatheory Site"
+    runs-on: [self-hosted, plutus-shared]
+    permissions:
+      contents: write
+    environment:
+      name: github-pages
+    steps:
+      - name: Checkout
+        uses: actions/checkout@main
+        with:
+          ref: ${{ inputs.version }}
+
+      - name: Build Site
+        run: nix build .#plutus-metatheory-site --out-link _site
+
+      - name: Deploy Site
+        uses: JamesIves/github-pages-deploy-action@main
+        with:
+          folder: _site
+          target-folder: docs/metatheory/${{ inputs.version }}
+          single-commit: true
+
+      - name: Deploy Latest
+        if: ${{ inputs.latest == true }}
+        uses: JamesIves/github-pages-deploy-action@main
+        with:
+          folder: _site
+          target-folder: docs/metatheory/latest
+          single-commit: true
+

nix/plutus-metatheory-site.nix

@@ -1,35 +1,61 @@
+# This file evaluates to a derivation that builds the AGDA metatheory
+# documentation site using Jekyll. The derivation also checks for broken links
+# in the generated HTML.
 { repoRoot, inputs, pkgs, system, lib }:
 
 let
 
-  # Doing this in two derivations so the call to agda is cached, since
-  # that's very slow. Makes it easier to iterate on the site build.
+  # This script can be useful if you are developing locally: it builds the site
+  # then checks for broken links and finally serves the site on localhost.
+  local-development = ''
+    cd plutus-metatheory
+    agda --html --html-highlight=auto --html-dir=html "src/index.lagda.md"
+    cp -R html/_layouts/ html/_site/
+    jekyll build --disable-disk-cache -s html -d html/_site
+    linkchecker html/_site --output failures
+    python3 -m http.server --directory html/_site 8002
+  '';
+
+  # We use two separate derivations to cache the slow Agda call, which makes it
+  # easier to iterate on the site build.
   plutus-metatheory-agda-html = pkgs.stdenv.mkDerivation {
     name = "plutus-metatheory-doc";
-    src = inputs.self + /plutus-metatheory;
+    src = lib.cleanSource (inputs.self + /plutus-metatheory);
     buildInputs = [ repoRoot.nix.agda-with-stdlib ];
+    dontInstall = true;
 
-    # Because of a quirk with jekyll, the _layouts folder must be in the same
-    # directory as the source folder.
+    # Jekyll requires the _layouts folder to be in the same directory as the
+    # source folder, so we copy it there to avoid issues.
     buildPhase = ''
       mkdir $out
       cp -R ${inputs.self + /plutus-metatheory/html/_layouts} $out
       agda --html --html-highlight=auto --html-dir="$out" "src/index.lagda.md"
     '';
-    dontInstall = true;
   };
 
   plutus-metatheory-site = pkgs.runCommand "plutus-metatheory-site"
     {
-      buildInputs = [ pkgs.jekyll ];
+      buildInputs = [ pkgs.jekyll pkgs.linkchecker ];
     }
     ''
       mkdir "$out"
-      # Disable the disk cache otherwise it tries to write to the source
+
+      # Prevent Jekyll from writing to the source directory by disabling its disk cache
       jekyll build \
         --disable-disk-cache \
         -s ${plutus-metatheory-agda-html} \
         -d "$out"
+
+      # Agda generates HTML files with href attributes containing absolute
+      # file:///nix/store/* URLs. All HTML files are located in the top-level
+      # build directory. The following command fixes all broken URLs.
+      find "$out" -name "*.html" | xargs sed -i -E \
+        's|href=\"file:///nix/store/.{32}-plutus-metatheory-site/([^\"]+)\"|href=\"\1\"|g'
+
+      if ! linkchecker "$out/index.html" --output failures; then
+        echo "Broken links found and printed above"
+        exit 1
+      fi
     '';
 in
 

plutus-metatheory/src/Type/RenamingSubstitution.lagda.md

@@ -239,7 +239,7 @@ ren-comp-VecList (xs ∷ xss) = cong₂ _∷_ (ren-comp-List xs) (ren-comp-VecLi
 
 A type substitution is a mapping of type variables to types. Much of this section
 mirrors functions in the Type section above, so the explainations and design intent
-are the same. There are [Fusion Proofs](markdown-header-fusion-proofs) below.
+are the same. There are [Fusion Proofs](#fusion-proofs) below.
 
 ```
 Sub : Ctx⋆ → Ctx⋆ → Set

plutus-metatheory/src/index.lagda.md

@@ -50,10 +50,10 @@ constants. The [`Type`](Type.html) module contains kinds, contexts and
 types. Types are intrinsically scoped and kinded and variables are
 represented using De Bruijn indices. Parallel renaming and
 substitution are implemented in the
-[`Type.RenamingSubstitution`](Type/RenamingSubstitution.html) module
+[`Type.RenamingSubstitution`](Type.RenamingSubstitution.html) module
 and they are shown to be satisfy the functor and relative monad laws
 respectively. Equality of types is specified in the
-[`Type.Equality`](Type/Equality.html) module. Equality serves as a
+[`Type.Equality`](Type.Equality.html) module. Equality serves as a
 specification of type computation and is used in the normalisation
 proof.