IntersectMBO · zeme-wana · May 11, 2024 · May 6, 2024 · May 9, 2024 · May 10, 2024
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
 ```