Improvements to plutus-metatheory site

IntersectMBO · May 6, 2024 · f545b46 · f545b46
1 parent 067e74f
commit f545b46
Show file tree

Hide file tree

Showing 5 changed files with 29 additions and 4 deletions.
diff --git a/nix/plutus-metatheory-site.nix b/nix/plutus-metatheory-site.nix
@@ -8,8 +8,12 @@ let
     name = "plutus-metatheory-doc";
     src = inputs.self + /plutus-metatheory;
     buildInputs = [ repoRoot.nix.agda-with-stdlib ];
+
+    # Because of a quirk with jekyll, the _layouts folder must be in the same
+    # directory as the source folder.
     buildPhase = ''
-      mkdir "$out"
+      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;
@@ -21,7 +25,7 @@ let
     }
     ''
       mkdir "$out"
-      # disable the disk cache otherwise it tries to write to the source
+      # Disable the disk cache otherwise it tries to write to the source
       jekyll build \
         --disable-disk-cache \
         -s ${plutus-metatheory-agda-html} \

diff --git a/nix/shell.nix b/nix/shell.nix
@@ -46,6 +46,7 @@ in
     pkgs.bzip2
     pkgs.gawk
     pkgs.scriv
+    pkgs.fswatch
 
     # Needed to make building things work, not for commands
     pkgs.zlib
@@ -79,6 +80,7 @@ in
     group = "changelog";
   };
 
+
   shellHook = ''
     ${builtins.readFile certEnv}
   '';

diff --git a/plutus-metatheory/.gitignore b/plutus-metatheory/.gitignore
@@ -2,3 +2,8 @@
 *.lagda~
 *.agda~
 src/MAlonzo
+html/_site
+html/.jekyll-cache
+html/*.html
+html/*.md
+html/*.css
diff --git a/plutus-metatheory/README.md b/plutus-metatheory/README.md
@@ -80,8 +80,8 @@ $ 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
+$ agda --html --html-highlight=auto --html-dir=html src/index.lagda.md
+$ jekyll build -s html -d html/_site
 ```
 
 ## Features:

diff --git a/plutus-metatheory/html/_layouts/page.html b/plutus-metatheory/html/_layouts/page.html
@@ -0,0 +1,14 @@
+<!doctype html>
+<html lang="en">
+  <head>
+    <meta charset="utf-8">
+    <title>{{ page.title }}</title>
+    <link rel="stylesheet" href="./Agda.css">
+  </head>
+  <body>
+    <h1>{{ page.title }}</h1>
+    <section>
+      {{ content }}
+    </section>
+  </body>
+</html>