Improvements to plutus-metatheory site (#5959)

* Improvements to plutus-metatheory site * Added markdown titles to markdown files so they get built properly. Not all of the titles are very interesting. --------- Co-authored-by: Ramsay Taylor <ramsay.taylor@iohk.io>
IntersectMBO · May 11, 2024 · 1df52aa · 1df52aa
1 parent 253004f
commit 1df52aa
Show file tree

Hide file tree

Showing 57 changed files with 262 additions and 43 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>
diff --git a/plutus-metatheory/src/Algorithmic.lagda.md b/plutus-metatheory/src/Algorithmic.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic
+layout: page
+---
 ```
 module Algorithmic where
 ```
@@ -335,4 +339,4 @@ constr-cong' :  ∀{Γ : Ctx Φ}{n}{i : Fin n}{A : Vec (List (Φ ⊢Nf⋆ *)) n}
             → (q : subst (IList (Γ ⊢_)) p' cs' ≡ subst (IList (Γ ⊢_)) p cs)
             → constr i A p' cs' ≡ constr i A p cs
 constr-cong' refl refl refl = refl
-```
+```
diff --git a/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CCvsCK.lagda.md b/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CCvsCK.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.BehaviouralEquivalence.CCvsCK
+layout: page
+---
 # CK machine
 
 ```

diff --git a/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CKvsCEK.lagda.md b/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CKvsCEK.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.BehaviouralEquivalence.CCvsCEK
+layout: page
+---
 # CEK behavioural equivalence with CK machine
 
 ```

diff --git a/plutus-metatheory/src/Algorithmic/CEK.lagda.md b/plutus-metatheory/src/Algorithmic/CEK.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.CEK
+layout: page
+---
 # CEK machine that discharges builtin args
 
 ```

diff --git a/plutus-metatheory/src/Algorithmic/CK.lagda.md b/plutus-metatheory/src/Algorithmic/CK.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.CK
+layout: page
+---
 # CK machine
 
 ```

diff --git a/plutus-metatheory/src/Algorithmic/Completeness.lagda.md b/plutus-metatheory/src/Algorithmic/Completeness.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Completeness
+layout: page
+---
 ```
 module Algorithmic.Completeness where
 

diff --git a/plutus-metatheory/src/Algorithmic/Erasure.lagda.md b/plutus-metatheory/src/Algorithmic/Erasure.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Erasure
+layout: page
+---
 ```
 {-# OPTIONS --injective-type-constructors #-}
 

diff --git a/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda.md b/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Erasure.RenamingSubstitution
+layout: page
+---
 ```
 module Algorithmic.Erasure.RenamingSubstitution where
 ```

diff --git a/plutus-metatheory/src/Algorithmic/Evaluation.lagda.md b/plutus-metatheory/src/Algorithmic/Evaluation.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Evaluation
+layout: page
+---
 ```
 module Algorithmic.Evaluation where
 ```
@@ -85,4 +89,4 @@ stepper {A} t n with eval (gas n) t
 ... | steps x (error _)   = return (error A)
 
 ```
-
+
diff --git a/plutus-metatheory/src/Algorithmic/Examples.lagda.md b/plutus-metatheory/src/Algorithmic/Examples.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Examples
+layout: page
+---
 ```
 module Algorithmic.Examples where
 ```

diff --git a/plutus-metatheory/src/Algorithmic/Properties.lagda.md b/plutus-metatheory/src/Algorithmic/Properties.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Properties
+layout: page
+---
 ```
 module Algorithmic.Properties where
 ```

diff --git a/plutus-metatheory/src/Algorithmic/Reduction.lagda.md b/plutus-metatheory/src/Algorithmic/Reduction.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Reduction
+layout: page
+---
 ```
 module Algorithmic.Reduction where
 ```

diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.ReductionEC
+layout: page
+---
 ```
 module Algorithmic.ReductionEC where
 ```
@@ -371,4 +375,4 @@ ival : ∀ b → Value (builtin b / refl)
 ival b = V-I b base
 -- -}
 ```
-
+
diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.ReductionEC.Determinism
+layout: page
+---
 ```
 module Algorithmic.ReductionEC.Determinism where
 ```
@@ -684,4 +688,4 @@ determinism {L = L} (ruleErr E' p) (ruleErr E'' q) | step ¬VL E err r' U with U
 ... | refl ,, refl ,, refl | refl ,, refl ,, refl = refl
 -- -}
 ```  
-
+
diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.ReductionEC.Progress
+layout: page
+---
 ```
 module Algorithmic.ReductionEC.Progress where
 ```
@@ -139,4 +143,4 @@ progress (case M cases)  with progress M
 ... | step (ruleErr E refl) = step (ruleErr (case cases E) refl)
 ... | done (V-constr e Tss refl refl vs refl) = step (ruleEC [] (β-case e Tss refl vs refl cases) refl refl)
 
- 
+ 
diff --git a/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda.md b/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.RenamingSubstitution
+layout: page
+---
 ```
 module Algorithmic.RenamingSubstitution where
 ```
@@ -591,4 +595,4 @@ exts⋆ˢ : ∀{Φ}{Γ Δ : Ctx Φ}
 -}
 ```
 
-
+
diff --git a/plutus-metatheory/src/Algorithmic/Signature.lagda.md b/plutus-metatheory/src/Algorithmic/Signature.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Algorithmic.Signature
+layout: page
+---
 ```
 module Algorithmic.Signature where
 ```
@@ -94,4 +97,4 @@ uniqueSigTy (bresult _) (bresult _) = refl
 uniqueSigTy (A B⇒ s) (.A B⇒ s') = cong (A B⇒_) (uniqueSigTy s s')
 uniqueSigTy (sucΠ s) (sucΠ s') = cong sucΠ (uniqueSigTy s s') 
 ```
-
+
diff --git a/plutus-metatheory/src/Algorithmic/Soundness.lagda.md b/plutus-metatheory/src/Algorithmic/Soundness.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Soundness
+layout: page
+---
 ```
 module Algorithmic.Soundness where
 

diff --git a/plutus-metatheory/src/Builtin.lagda.md b/plutus-metatheory/src/Builtin.lagda.md
@@ -184,22 +184,22 @@ hence need to be embedded into `n⋆ / n♯ ⊢⋆` using the postfix constructo
     
     list :  ∀{n⋆ n♯} → n♯ ⊢♯ → n⋆ / n♯ ⊢⋆
     list a = (blist a) ↑
-    ```
+```
 
-    ###Operators for constructing signatures
-
-    The following operators are used to express signatures in a familiar way,
-    but ultimately, they construct a Sig 
+### Operators for constructing signatures
 
-    An expression 
-      n⋆×n♯ [ t₁ , t₂ , t₃ ]⟶ tᵣ
-
-    is actually parsed as
-      (((n⋆×n♯ [ t₁) , t₂) , t₃) ]⟶ tᵣ
-
-    and constructs a signature
+The following operators are used to express signatures in a familiar way,
+but ultimately, they construct a Sig 
+
+An expression 
+  n⋆×n♯ [ t₁ , t₂ , t₃ ]⟶ tᵣ
+
+is actually parsed as
+  (((n⋆×n♯ [ t₁) , t₂) , t₃) ]⟶ tᵣ
+
+and constructs a signature
 
-    sig n⋆ n♯ (t₃ ∷ t₂ ∷ t₁) tᵣ
+sig n⋆ n♯ (t₃ ∷ t₂ ∷ t₁) tᵣ
 
     ```
     ArgSet : Set

diff --git a/plutus-metatheory/src/Builtin/Constant/AtomicType.lagda.md b/plutus-metatheory/src/Builtin/Constant/AtomicType.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Builtin.Constant.AtomicType
+layout: page
+---
 
 ```
 module Builtin.Constant.AtomicType where

diff --git a/plutus-metatheory/src/Check.lagda.md b/plutus-metatheory/src/Check.lagda.md
@@ -1,4 +1,5 @@
 ---
+title: Type Checker
 layout: page
 ---
 ## Type checker

diff --git a/plutus-metatheory/src/Cost.lagda.md b/plutus-metatheory/src/Cost.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Cost
+layout: page
+---
 # Costs
 
 

diff --git a/plutus-metatheory/src/Cost/Base.lagda.md b/plutus-metatheory/src/Cost/Base.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Cost.Base
+layout: page
+---
 ```
 module Cost.Base where 
 
@@ -92,4 +95,4 @@ record MachineParameters (Cost : Set) : Set where
 
     startupCost : Cost 
     startupCost = cekMachineCost BStartup
-``` 
+``` 
diff --git a/plutus-metatheory/src/Cost/Model.lagda.md b/plutus-metatheory/src/Cost/Model.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Cost.Model
+layout: page
+---
 # Builtin Cost Models
 
 ```

diff --git a/plutus-metatheory/src/Cost/Raw.lagda.md b/plutus-metatheory/src/Cost/Raw.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Cost.Raw
+layout: page
+---
 # Raw Cost structures to inferface with Haskell
 
 ```

diff --git a/plutus-metatheory/src/Cost/Size.lagda.md b/plutus-metatheory/src/Cost/Size.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Cost.Size
+layout: page
+---
 # Size of Constants
 
 ```
@@ -83,4 +87,4 @@ defaultConstantMeasure (tmCon (pair t u) (x , y)) =
 defaultValueMeasure : Value → CostingNat 
 defaultValueMeasure (V-con ty x) = defaultConstantMeasure (tmCon ty x)
 defaultValueMeasure _ = 0
-```
+```
diff --git a/plutus-metatheory/src/Declarative/Examples/StdLib/ChurchNat.lagda.md b/plutus-metatheory/src/Declarative/Examples/StdLib/ChurchNat.lagda.md
@@ -1,3 +1,7 @@
+---
+title: ChurchNat
+layout: page
+---
 ```
 module Declarative.Examples.StdLib.ChurchNat where
 ```

diff --git a/plutus-metatheory/src/Declarative/Examples/StdLib/Function.lagda.md b/plutus-metatheory/src/Declarative/Examples/StdLib/Function.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Function
+layout: page
+---
 ```
 module Declarative.Examples.StdLib.Function where
 ```

diff --git a/plutus-metatheory/src/Declarative/Examples/StdLib/Nat.lagda.md b/plutus-metatheory/src/Declarative/Examples/StdLib/Nat.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Nat
+layout: page
+---
 ```
 module Declarative.Examples.StdLib.Nat where
 ```