PLT-282: Build the Agda doc site in CI (#5128)

* PLT-282: Build the Agda doc site in CI

The README link won't work until this is merged, but it should be fine
after that.

Definitely some improvements to be made to the site (it's unstyled!),
but I'll leave those for later.

* Revert path workaround

README.adoc

@@ -44,6 +44,8 @@ After setting it up you should just be able to depend on the `plutus` packages a
 
 The main documentation is located https://plutus.readthedocs.io/en/latest/[here].
 
+The latest documentation for the metatheory can be found https://ci.zw3rk.com/job/input-output-hk-plutus/master/x86_64-linux.plutus-metatheory-site/latest/download/1[here].
+
 === Talks
 
 - https://www.youtube.com/watch?v=MpWeg6Fg0t8[Functional Smart Contracts on Cardano (2020)]: an overview of the ideas behind the Plutus Platform.

nix/cells/plutus/library/make-plutus-shell.nix

@@ -104,6 +104,11 @@ inputs.std.lib.dev.mkShell {
       category = "docs";
       help = "nix build and serve the doc site on localhost:8002";
     }
+    {
+      package = pkgs.jekyll;
+      category = "docs";
+      help = "Static site builder, used for the metatheory documentation";
+    }
 
     {
       package = cell.packages.nixpkgs-fmt;

nix/cells/plutus/packages/default.nix

@@ -81,4 +81,6 @@
   scriv = import ./scriv.nix block;
 
   repo-root = import ./repo-root.nix block;
+
+  plutus-metatheory-site = import ./plutus-metatheory-site.nix block;
 }

nix/cells/plutus/packages/plutus-metatheory-site.nix

@@ -0,0 +1,29 @@
+{ inputs, cell }:
+
+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.
+  plutus-metatheory-agda-html = cell.library.pkgs.stdenv.mkDerivation {
+    name = "plutus-metatheory-doc";
+    src = inputs.self + /plutus-metatheory;
+    buildInputs = [ cell.packages.agda-with-stdlib ];
+    buildPhase = ''
+      mkdir "$out"
+      agda --html --html-highlight=auto --html-dir="$out" "src/index.lagda.md"
+    '';
+    dontInstall = true;
+  };
+  plutus-metatheory-site = cell.library.pkgs.runCommand "plutus-metatheory-site"
+    {
+      buildInputs = [ cell.library.pkgs.jekyll ];
+    }
+    ''
+      mkdir "$out"
+      # disable the disk cache otherwise it tries to write to the source
+      jekyll build \
+        --disable-disk-cache \
+        -s ${plutus-metatheory-agda-html} \
+        -d "$out"
+    '';
+in
+plutus-metatheory-site

plutus-metatheory/README.md

@@ -68,15 +68,20 @@ the same as for other plutus components, see the top-level [README](https://gith
 You can execute the plc-agda command like this:
 
 ```
-$ nix-shell
-$ cabal v2-run plc-agda
+$ cabal run plc-agda
 ```
 
 To run the tests you can execute:
 
 ```
-$ nix-shell
-$ cabal v2-test plutus-metatheory
+$ cabal test plutus-metatheory
+```
+
+To build the documentation as a static site:
+
+```
+$ agda --html --html-highlight=auto --html-dir html src/index.lagda.md
+$ jekyll -s html -d site
 ```
 
 ## Features: