Fixed broken local links; added jekyll-feed back into the plugins.

Makefile

@@ -5,9 +5,9 @@ markdown := $(subst src/,out/,$(subst .lagda,.md,$(agda)))
 all: $(markdown)
 
 test: $(markdown)
-	ruby -S bundle exec jekyll clean
-	ruby -S bundle exec jekyll build -d _site/sf/
-	ruby -S bundle exec htmlproofer _site --disable-external
+	ruby -S bundle exec jekyll clean -d _test
+	ruby -S bundle exec jekyll build -d _test/sf/
+	ruby -S bundle exec htmlproofer _test
 
 out/:
 	mkdir -p out/

_config.yml

@@ -24,6 +24,8 @@ disqus:
 
 baseurl: "/sf"
 url: "https://wenkokke.github.io"
+plugins:
+  - jekyll-feed
 markdown: kramdown
 theme: minima
 exclude:

src/plta/DeBruijn.lagda

@@ -212,8 +212,7 @@ data Value : ∀ {Γ A} → Γ ⊢ A → Set where
     → Value (ƛ N)
 \end{code}
 
-Here `` `zero `` requires an implicit parameter to aid inference
-(much in the same way that `[]` did in [Lists](Lists)).
+Here `zero` requires an implicit parameter to aid inference (much in the same way that `[]` did in [Lists]({{ site.baseurl }}{% link out/plta/Lists.md %})).
 
 ## Reduction step
 

src/plta/Decidable.lagda

@@ -33,9 +33,7 @@ open import Function using (_∘_)
 
 ## Evidence vs Computation
 
-Recall that Chapter [Relations](Relations) defined comparison
-an inductive datatype, which provides *evidence* that one number
-is less than or equal to another.
+Recall that Chapter [Relations]({{ site.baseurl }}{% link out/plta/Relations.md %}) defined comparison an inductive datatype, which provides *evidence* that one number is less than or equal to another.
 \begin{code}
 infix 4 _≤_
 
@@ -499,8 +497,7 @@ on which matches; but either is equally valid.
 
 ## Decidability of All
 
-Recall that in Chapter [Lists](Lists#All) we defined a predicate `All P`
-that holds if a given predicate is satisfied by every element of a list.
+Recall that in Chapter [Lists]({{ site.baseurl }}{% link out/plta/Lists.md %}#All) we defined a predicate `All P` that holds if a given predicate is satisfied by every element of a list.
 \begin{code}
 data All {A : Set} (P : A → Set) : List A → Set where
   [] : All P []
@@ -516,7 +513,7 @@ all p  =  foldr _∧_ true ∘ map p
 \end{code}
 The function can be written in a particularly compact style by
 using the higher-order functions `map` and `foldr` as defined in
-the sections on [Map](Lists#Map) and [Fold](Lists#Fold).
+the sections on [Map]({{ site.baseurl }}{% link out/plta/Lists.md %}#Map) and [Fold]({{ site.baseurl }}{% link out/plta/Lists.md %}#Fold).
 
 As one would hope, if we replace booleans by decidables there is again
 an analogue of `All`.  First, return to the notion of a predicate `P` as

src/plta/Lambda.lagda

@@ -28,13 +28,13 @@ recursive function definitions.
 
 This chapter formalises the simply-typed lambda calculus, giving its
 syntax, small-step semantics, and typing rules.  The next chapter
-[LambdaProp](LambdaProp) reviews its main properties, including
+[LambdaProp]({{ site.baseurl }}{% link out/plta/LambdaProp.md %}) reviews its main properties, including
 progress and preservation.  Following chapters will look at a number
 of variants of lambda calculus.
 
 Be aware that the approach we take here is _not_ our recommended
 approach to formalisation.  Using De Bruijn indices and
-inherently-typed terms, as we will do in Chapter [DeBruijn](DeBruijn),
+inherently-typed terms, as we will do in Chapter [DeBruijn]({{ site.baseurl }}{% link out/plta/DeBruijn.md %}),
 leads to a more compact formulation.  Nonetheless, we begin with named
 variables, partly because such terms are easier to read and partly
 because the development is more traditional.
@@ -144,7 +144,7 @@ four : Term
 four = plus · two · two
 \end{code}
 The recursive definition of addition is similar to our original
-definition of `_+_` for naturals, as given in Chapter [Natural](Naturals).
+definition of `_+_` for naturals, as given in Chapter [Naturals]({{ site.baseurl }}{% link out/plta/Naturals.md %}).
 Later we will confirm that two plus two is four, in other words that
 the term
 
@@ -278,7 +278,7 @@ names, `x` and `x′`.
 We only consider reduction of _closed_ terms,
 those that contain no free variables.  We consider
 a precise definition of free variables in Chapter
-[LambdaProp](LambdaProp).
+[LambdaProp]({{ site.baseurl }}{% link out/plta/LambdaProp.md %}).
 
 *rewrite (((*
 A term is a value if it is fully reduced.
@@ -326,7 +326,7 @@ An alternative is not to focus on closed terms,
 to treat variables as values, and to treat
 `ƛ x ⇒ N` as a value only if `N` is a value.
 Indeed, this is how Agda normalises terms.
-We consider this approach in a [later chapter](Untyped).
+We consider this approach in a [later chapter]({{ site.baseurl }}{% link out/plta/Untyped.md %}).
 
 ## Substitution
 
@@ -600,7 +600,7 @@ are written as follows.
     L ⟹* N
 
 Here it is formalised in Agda, along similar lines to what
-we used for reasoning about [Equality](Equality).
+we used for reasoning about [Equality]({{ site.baseurl }}{% link out/plta/Equality.md %}).
 
 \begin{code}
 infix  2 _⟹*_

src/plta/Lists.lagda

@@ -34,7 +34,7 @@ postulate
   extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
 \end{code}
 
-[extensionality]: Equality#extensionality
+[extensionality]: {{ site.baseurl }}{% link out/plta/Equality.md %}#extensionality
 
 
 ## Lists
@@ -862,7 +862,7 @@ _∘′_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂}
 (g ∘′ f) x  =  g (f x)
 \end{code}
 
-[unipoly]: Equality/index.html#unipoly
+[unipoly]: {{ site.baseurl }}{% link out/plta/Equality.md %}#unipoly
 
 Show that `Any` and `All` satisfy a version of De Morgan's Law.
 \begin{code}

src/plta/Modules.lagda

@@ -38,7 +38,8 @@ postulate
   extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
 \end{code}
 
-[extensionality]: Equality#extensionality
+[extensionality]: {{ site.baseurl }}{% link out/plta/Equality.md %}#extensionality
+
 
 
 ## Modules

src/plta/Naturals.lagda

@@ -269,7 +269,7 @@ specifies operators to support reasoning about equivalence, and adds
 all the names specified in the `using` clause into the current scope.
 In this case, the names added are `begin_`, `_≡⟨⟩_`, and `_∎`.  We
 will see how these are used below.  We take all these as givens for now,
-but will see how they are defined in Chapter [Equality](Equality).
+but will see how they are defined in Chapter [Equality]({{ site.baseurl }}{% link out/plta/Equality.md %}).
 
 Agda uses underbars to indicate where terms appear in infix or mixfix
 operators. Thus, `_≡_` and `_≡⟨⟩_` are infix (each operator is written

src/plta/Negation.lagda

@@ -142,13 +142,13 @@ when `A` is anything other than `⊥` itself.
 
 ### Exercise (`≢`, `<-irrerflexive`)
 
-Using negation, show that [strict inequality](Relations/#strict-inequality)
+Using negation, show that [strict inequality]({{ site.baseurl }}{% link out/plta/Relations.md %}/#strict-inequality)
 is irreflexive, that is, `n < n` holds for no `n`.
 
 
 ### Exercise (`trichotomy`)
 
-Show that strict inequality satisfies [trichotomy](Relations/#trichotomy),
+Show that strict inequality satisfies [trichotomy]({{ site.baseurl }}{% link out/plta/Relations.md %}/#trichotomy),
 that is, for any naturals `m` and `n` exactly one of the following holds:
 
 * `m < n`

src/plta/Properties.lagda

@@ -534,7 +534,7 @@ which is left as an exercise for the reader.
 
 Write out what is known about associativity on each of the first four
 days using a finite story of creation, as
-[earlier](Naturals/index.html#finite-creation).
+[earlier]({{ site.baseurl }}{% link out/plta/Naturals.md %}#finite-creation).
 
 
 ## Associativity with rewrite

src/plta/Quantifiers.lagda

@@ -32,7 +32,7 @@ postulate
   extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
 \end{code}
 
-[extensionality]: Equality/index.html#extensionality
+[extensionality]: {{ site.baseurl }}{% link out/plta/Equality.md %}#extensionality
 
 
 ## Universals
@@ -92,7 +92,7 @@ Show that universals distribute over conjunction.
 ∀-Distrib-× = ∀ {A : Set} {B C : A → Set} →
   (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
 \end{code}
-Compare this with the result (`→-distrib-×`) in Chapter [Connectives](Connectives).
+Compare this with the result (`→-distrib-×`) in Chapter [Connectives]({{ site.baseurl }}{% link out/plta/Connectives.md %}).
 
 ### Exercise (`⊎∀-implies-∀⊎`)
 
@@ -218,7 +218,7 @@ The result can be viewed as a generalisation of currying.  Indeed, the code to
 establish the isomorphism is identical to what we wrote when discussing
 [implication][implication].
 
-[implication]: Connectives/index.html#implication
+[implication]: {{ site.baseurl }}{% link out/plta/Connectives.md %}/index.html#implication
 
 ### Exercise (`∃-distrib-⊎`)
 
@@ -240,7 +240,7 @@ Does the converse hold? If so, prove; if not, explain why.
 
 ## An existential example
 
-Recall the definitions of `even` and `odd` from Chapter [Relations](Relations).
+Recall the definitions of `even` and `odd` from Chapter [Relations]({{ site.baseurl }}{% link out/plta/Relations.md %}).
 \begin{code}
 data even : ℕ → Set
 data odd  : ℕ → Set

src/plta/Relations.lagda

@@ -128,7 +128,7 @@ either `(1 ≤ 2) ≤ 3` or `1 ≤ (2 ≤ 3)`.
 
 Given two numbers, it is straightforward to compute whether or not the first is
 less than or equal to the second.  We don't give the code for doing so here, but
-will return to this point in Chapter [Decidability](Decidability).
+will return to this point in Chapter [Decidable]({{ site.baseurl }}{% link out/plta/Decidable.md %}).
 
 
 ## Properties of ordering relations
@@ -418,7 +418,7 @@ transitivity proves `m + p ≤ n + q`, as was to be shown.
 
 The proof of monotonicity (and the associated lemmas) can be written
 in a more readable form by using an anologue of our notation for
-`≡-reasoning`.  Read ahead to chapter [Equivalence](Equivalence) to
+`≡-reasoning`.  Read ahead to chapter [Equality]({{ site.baseurl }}{% link out/plta/Equality.md %}) to
 see how `≡-reasoning` is defined, define `≤-reasoning` analogously,
 and use it to write out an alternative proof that addition is
 monotonic with regard to inequality.
@@ -448,7 +448,7 @@ It is also monotonic with regards to addition and multiplication.
 Most of the above are considered in exercises below.  Irreflexivity
 requires negation, as does the fact that the three cases in
 trichotomy are mutually exclusive, so those points are deferred
-to the chapter that introduces [negation](Negation).
+to the chapter that introduces [negation]({{ site.baseurl }}{% link out/plta/Negation.md %}).
 
 It is straightforward to show that `suc m ≤ n` implies `m < n`,
 and conversely.  One can then give an alternative derivation of the
@@ -469,7 +469,7 @@ the sense that for any `m` and `n` that one of the following holds:
 This only involves two relations, as we define `m > n` to
 be the same as `n < m`. You will need a suitable data declaration,
 similar to that used for totality.  (We will show that the three cases
-are exclusive after [negation](Negation) is introduced.)
+are exclusive after [negation]({{ site.baseurl }}{% link out/plta/Negation.md %}) is introduced.)
 
 ### Exercise (`+-mono-<`)
 
@@ -591,7 +591,7 @@ import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total;
                                   +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
 \end{code}
 In the standard library, `≤-total` is formalised in terms of
-disjunction (which we define in Chapter [Connectives](Connectives)),
+disjunction (which we define in Chapter [Connectives]({{ site.baseurl }}{% link out/plta/Connectives.md %})),
 and `+-monoʳ-≤`, `+-monoˡ-≤`, `+-mono-≤` are proved differently than here
 as well as taking as implicit arguments that here are explicit.