Working on getting rid of deadlinks

Makefile

@@ -5,12 +5,16 @@ 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
+	ruby -S bundle exec htmlproofer _site --disable-external
 
-out/%.md: src/%.lagda
-	mkdir -p out
-	agda2html --verbose --link-to-agda-stdlib --use-jekyll=out/ -i $< -o $@
+out/:
+	mkdir -p out/
+
+out/%.md: src/%.lagda | out/
+	agda2html --verbose --link-to-agda-stdlib --use-jekyll=out/ -i $< -o $@ 2>&1 \
+		| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
 
 # start server
 server-start:

_config.yml

@@ -22,9 +22,8 @@ description: >
 disqus:
   shortname: wenkokke
 
-# technical details below --- do not modify (ง'-')ง 
 baseurl: "/sf"
-url: "https://wenkokke.github.io/sf"  
+url: "https://wenkokke.github.io"
 markdown: kramdown
 theme: minima
 exclude:

_includes/header.html

@@ -15,7 +15,7 @@
 
             <div class="trigger">
                 <a class="page-link" href="{{ "/" | relative_url }}">Table of Contents</a>
-                <a class="page-link" href="{{ "/about" | relative_url }}">About</a>
+                <a class="page-link" href="{{ "/Acknowledgements" | relative_url }}">About</a>
             </div>
         </nav>
 

src/Acknowledgements.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Acknowledgements"
 layout    : page
-permalink : /Acknowledgements
+permalink : /Acknowledgements/
 ---
 
 Thank you to the following.
@@ -14,7 +14,7 @@ To Conor McBride and James McKinna, for cool ideas and handholding.
 
 To Andreas Abel and Ulf Norell, ditto.
 
-To David Darais, for showing me how much more compact it is to avoid raw terms.
+To David Darais, for showing us how much more compact it is to avoid raw terms.
 
 For pull requests.
 * Vikraman Choudhury

src/Connectives.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Connectives: Conjunction, disjunction, and implication"
 layout    : page
-permalink : /Connectives
+permalink : /Connectives/
 ---
 
 This chapter introduces the basic logical connectives, by observing

src/DeBruijn.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "DeBruijn: Inherently typed De Bruijn representation"
 layout    : page
-permalink : /DeBruijn
+permalink : /DeBruijn/
 ---
 
 ## Imports

src/Decidable.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Decidable: Booleans and decision procedures"
 layout    : page
-permalink : /Decidable
+permalink : /Decidable/
 ---
 
 We have a choice as to how to represent relations:

src/Equality.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Equality: Equality and equational reasoning"
 layout    : page
-permalink : /Equality
+permalink : /Equality/
 ---
 
 Much of our reasoning has involved equality.  Given two terms `M`

src/Extensions.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Extensions: Extensions to simply-typed lambda calculus"
 layout    : page
-permalink : /Extensions
+permalink : /Extensions/
 ---
 
 ## Imports

src/Fonts.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Fonts"
 layout    : page
-permalink : /Fonts
+permalink : /Fonts/
 ---
 
 Test page for fonts.

src/Inference.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Inference: Bidirectional type inference"
 layout    : page
-permalink : /Inference
+permalink : /Inference/
 ---
 
 ## Imports

src/Isomorphism.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Isomorphism: Isomorphism and Embedding"
 layout    : page
-permalink : /Isomorphism
+permalink : /Isomorphism/
 ---
 
 This section introduces isomorphism as a way of asserting that two

src/Lambda.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Lambda: Introduction to Lambda Calculus"
 layout    : page
-permalink : /Lambda
+permalink : /Lambda/
 ---
 
 The _lambda-calculus_, first published by the logician Alonzo Church in

src/LambdaProp.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "LambdaProp: Properties of Simply-Typed Lambda Calculus"
 layout    : page
-permalink : /LambdaProp
+permalink : /LambdaProp/
 ---
 
 This chapter develops the fundamental theory of the Simply

src/Lists.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Lists: Lists and higher-order functions"
 layout    : page
-permalink : /Lists
+permalink : /Lists/
 ---
 
 This chapter discusses the list data type.  It gives further examples

src/Modules.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Modules: Modules and List Examples"
 layout    : page
-permalink : /Modules
+permalink : /Modules/
 ---
 
 ** Turn this into a Setoid example. Copy equivalence relation and setoid

src/Naturals.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Naturals: Natural numbers"
 layout    : page
-permalink : /Naturals
+permalink : /Naturals/
 ---
 
 The night sky holds more stars than I can count, though fewer than five

src/Negation.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Negation: Negation, with intuitionistic and classical logic"
 layout    : page
-permalink : /Negation
+permalink : /Negation/
 ---
 
 This chapter introduces negation, and discusses intuitionistic

src/Preface.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Preface"
 layout    : page
-permalink : /Preface
+permalink : /Preface/
 ---
 
 This book is an introduction to programming language theory, written

src/Properties.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Properties: Proof by Induction"
 layout    : page
-permalink : /Properties
+permalink : /Properties/
 ---
 
 Now that we've defined the naturals and operations upon them, our next

src/Pure.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Pure: Pure Type Systems"
 layout    : page
-permalink : /Pure
+permalink : /Pure/
 ---
 
 Barendregt, H. (1991). Introduction to generalized type

src/Quantifiers.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Quantifiers: Universals and existentials"
 layout    : page
-permalink : /Quantifiers
+permalink : /Quantifiers/
 ---
 
 This chapter introduces universal and existential quantification.

src/Relations.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Relations: Inductive definition of relations"
 layout    : page
-permalink : /Relations
+permalink : /Relations/
 ---
 
 After having defined operations such as addition and multiplication,

src/Untyped.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Untyped: Untyped lambda calculus with full normalisation"
 layout    : page
-permalink : /Untyped
+permalink : /Untyped/
 ---
 
 This chapter considers a system that varies, in interesting ways,