Generate correct links in index.md; added 'make test' option which runs htmlproofer; excluded a number of files from the _site directory; these should've all been seperate commits, shouldn't they have?

.travis.yml

@@ -6,7 +6,7 @@ language: ruby
 # Caching so the next build will be fast too.
 cache:
   bundler: true
-  timeout: 1200
+  timeout: 1500
   directories:
   - $HOME/.stack
   - $HOME/.agda

Gemfile

@@ -2,3 +2,4 @@ source "https://rubygems.org"
 
 gem "minima", "~> 2.4.0"
 gem "github-pages", group: :jekyll_plugins
+gem "html-proofer"

Gemfile.lock

@@ -13,6 +13,7 @@ GEM
       execjs
     coffee-script-source (1.11.1)
     colorator (1.1.0)
+    colorize (0.8.1)
     commonmarker (0.17.9)
       ruby-enum (~> 0.5)
     concurrent-ruby (1.0.5)
@@ -83,6 +84,15 @@ GEM
     html-pipeline (2.8.0)
       activesupport (>= 2)
       nokogiri (>= 1.4)
+    html-proofer (3.9.1)
+      activesupport (>= 4.2, < 6.0)
+      addressable (~> 2.3)
+      colorize (~> 0.8)
+      mercenary (~> 0.3.2)
+      nokogiri (~> 1.8.1)
+      parallel (~> 1.3)
+      typhoeus (~> 1.3)
+      yell (~> 2.0)
     http_parser.rb (0.6.0)
     i18n (0.9.5)
       concurrent-ruby (~> 1.0)
@@ -210,6 +220,7 @@ GEM
       mini_portile2 (~> 2.3.0)
     octokit (4.9.0)
       sawyer (~> 0.8.0, >= 0.5.3)
+    parallel (1.12.1)
     pathutil (0.16.1)
       forwardable-extended (~> 2.6)
     public_suffix (2.0.5)
@@ -238,12 +249,14 @@ GEM
     tzinfo (1.2.5)
       thread_safe (~> 0.1)
     unicode-display_width (1.3.2)
+    yell (2.0.7)
 
 PLATFORMS
   ruby
 
 DEPENDENCIES
   github-pages
+  html-proofer
   minima (~> 2.4.0)
 
 BUNDLED WITH

Makefile

@@ -2,7 +2,11 @@ agda := $(wildcard src/*.lagda) $(wildcard src/**/*.lagda)
 agdai := $(wildcard src/*.agdai) $(wildcard src/**/*.agdai)
 markdown := $(subst src/,out/,$(subst .lagda,.md,$(agda)))
 
-all: bugfix $(markdown)
+all: $(markdown)
+
+test: $(markdown)
+	ruby -S bundle exec jekyll build -d _site/sf/
+	ruby -S bundle exec htmlproofer _site
 
 out/%.md: src/%.lagda
 	mkdir -p out
@@ -68,7 +72,7 @@ $(HOME)/agda2html-master/:
 	cd $(HOME)/agda2html-master;\
 		stack install
 
-.phony: serve build clean clobber macos-setup travis-setup
+.phony: serve build test clean clobber macos-setup travis-setup
 
 # workaround for a bug in agda2html
 bugfix:

_config.yml

@@ -28,6 +28,10 @@ url: "https://wenkokke.github.io/sf"
 markdown: kramdown
 theme: minima
 exclude:
-  - src/
+  - "src/"
-  - Gemfile
+  - "extra/"
-  - Gemfile.lock
+  - "README.md"
+  - "Notes.md"
+  - "*.lagda"
+  - "Gemfile"
+  - "Gemfile.lock"

index.md

@@ -18,38 +18,38 @@ fixes are encouraged.
 
 ## Front matter
 
-  - [Preface](Preface)
+  - [Preface]({{ site.baseurl }}{% link out/Preface.md %})
 
 ## Part 1: Logical Foundations
 
 (This part is ready for review. Please comment!)
 
-  - [Naturals: Natural numbers](Naturals)
+  - [Naturals: Natural numbers]({{ site.baseurl }}{% link out/Naturals.md %})
   - [Properties: Proof by induction](Properties)
-  - [Relations: Inductive definition of relations](Relations)
+  - [Relations: Inductive definition of relations]({{ site.baseurl }}{% link out/Relations.md %})
-  - [Equality: Equality and equational reasoning](Equality)
+  - [Equality: Equality and equational reasoning]({{ site.baseurl }}{% link out/Equality.md %})
-  - [Isomorphism: Isomorphism and embedding](Isomorphism)
+  - [Isomorphism: Isomorphism and embedding]({{ site.baseurl }}{% link out/Isomorphism.md %})
-  - [Connectives: Conjunction, disjunction, and implication](Connectives)
+  - [Connectives: Conjunction, disjunction, and implication]({{ site.baseurl }}{% link out/Connectives.md %})
-  - [Negation: Negation, with intuitionistic and classical Logic](Negation)
+  - [Negation: Negation, with intuitionistic and classical Logic]({{ site.baseurl }}{% link out/Negation.md %})
-  - [Quantifiers: Universals and existentials](Quantifiers)
+  - [Quantifiers: Universals and existentials]({{ site.baseurl }}{% link out/Quantifiers.md %})
-  - [Lists: Lists and higher-order functions](Lists)
+  - [Lists: Lists and higher-order functions]({{ site.baseurl }}{% link out/Lists.md %})
-  - [Decidable: Booleans and decision procedures](Decidable)
+  - [Decidable: Booleans and decision procedures]({{ site.baseurl }}{% link out/Decidable.md %})
 
 ## Part 2: Programming Language Foundations
 
 (This part is not yet ready for review.)
 
-  - [Lambda: Lambda: Introduction to Lambda Calculus](Lambda)
+  - [Lambda: Lambda: Introduction to Lambda Calculus]({{ site.baseurl }}{% link out/Lambda.md %})
-  - [LambdaProp: Properties of Simply-Typed Lambda Calculus](LambdaProp)
+  - [LambdaProp: Properties of Simply-Typed Lambda Calculus]({{ site.baseurl }}{% link out/LambdaProp.md %})
-  - [DeBruijn: Inherently typed De Bruijn representation](DeBruijn)
+  - [DeBruijn: Inherently typed De Bruijn representation]({{ site.baseurl }}{% link out/DeBruijn.md %})
-  - [Extensions: Extensions to simply-typed lambda calculus](Extensions)
+  - [Extensions: Extensions to simply-typed lambda calculus]({{ site.baseurl }}{% link out/Extensions.md %})
-  - [Inference: Bidirectional type inference](Inference)
+  - [Inference: Bidirectional type inference]({{ site.baseurl }}{% link out/Inference.md %})
-  - [Untyped: Untyped lambda calculus with full normalisation](Untyped)
+  - [Untyped: Untyped lambda calculus with full normalisation]({{ site.baseurl }}{% link out/Untyped.md %})
 
 ## Backmatter
 
-  - [Acknowledgements](Acknowledgements)
+  - [Acknowledgements]({{ site.baseurl }}{% link out/Acknowledgements.md %})
-  - [Fonts: Test page for fonts](Fonts)
+  - [Fonts: Test page for fonts]({{ site.baseurl }}{% link out/Fonts.md %})
 
 [sf]: https://softwarefoundations.cis.upenn.edu/
 [wen]: https://github.com/wenkokke