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.