From 99aa26401f6e102489d423bd149da38c251db0cc Mon Sep 17 00:00:00 2001
From: Michael Reed <michael@michaelreed.io>
Date: Fri, 19 Jun 2020 11:21:00 -0400
Subject: [PATCH 01/38] EPUB: Populate acknowledgements.md with contributors

Use liquid-lua to generate acknowledgements_epub.md, which is used by
pandoc to build the EPUB book.  Also stop using the '{%-' / '-%}'
syntax, which liquid-lua does not support, in templates.

Also add a vertical space between the first bullet in each bulleted
list so pandoc recognizes bulleted lists as such. This has no effect on
the the website.
---
 .gitignore                   |  4 ++++
 .travis.yml                  |  1 +
 Makefile                     | 24 ++++++++++++++++----
 epub/index.md                |  2 +-
 epub/rewrite-html-ul.lua     |  5 ++++
 epub/run-liquid.lua          | 19 ++++++++++++++++
 src/plfa/acknowledgements.md | 44 ++++++++++++++++++++----------------
 7 files changed, 73 insertions(+), 26 deletions(-)
 create mode 100644 epub/rewrite-html-ul.lua
 create mode 100644 epub/run-liquid.lua

diff --git a/.gitignore b/.gitignore
index 2d7777f3..0967dd49 100644
--- a/.gitignore
+++ b/.gitignore
@@ -26,3 +26,7 @@ Gemfile.lock
 
 ## Emacs files
 auto/
+
+## Misc build files
+out/
+src/plfa/acknowledgements_epub.md
diff --git a/.travis.yml b/.travis.yml
index 7269268f..97b07520 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -22,6 +22,7 @@ addons:
     packages:
       - libgmp-dev
       - libicu-dev
+      - luarocks
 
 # Ensure we run BASH and not SH
 env:
diff --git a/Makefile b/Makefile
index 88c544fd..9eb27434 100644
--- a/Makefile
+++ b/Makefile
@@ -49,12 +49,10 @@ out/:
 #       sections are displayed to users. Some readers may be slow if the chapter
 #       files are too large, so for large documents with few level-1 headings, one
 #       might want to use a chapter level of 2 or 3."
-#
-#TODO: embedded fonts not working (path problem?)
 
 epub: out/plfa.epub
 
-out/plfa.epub: out/ $(AGDA) $(LUA) epub/main.css
+out/plfa.epub: out/ $(AGDA) $(LUA) epub/main.css src/plfa/acknowledgements_epub.md
 	pandoc --strip-comments \
 		--css=epub/main.css \
 		--epub-embed-font='assets/fonts/mononoki.woff' \
@@ -62,6 +60,7 @@ out/plfa.epub: out/ $(AGDA) $(LUA) epub/main.css
 		--epub-embed-font='assets/fonts/DejaVuSansMono.woff' \
 		--lua-filter epub/include-files.lua \
 		--lua-filter epub/rewrite-links.lua \
+		--lua-filter epub/rewrite-html-ul.lua \
 		--lua-filter epub/default-code-class.lua -M default-code-class=agda \
 		--standalone \
 		--fail-if-warnings \
@@ -70,7 +69,8 @@ out/plfa.epub: out/ $(AGDA) $(LUA) epub/main.css
 		-o "$@" \
 		epub/index.md
 
-
+src/plfa/acknowledgements_epub.md: src/plfa/acknowledgements.md _config.yml 
+	lua epub/run-liquid.lua _config.yml $< > $@
 
 
 # Convert literal Agda to Markdown
@@ -119,7 +119,7 @@ build-incremental: $(MARKDOWN)
 
 # Remove all auxiliary files
 clean:
-	rm -f .agda-stdlib.sed .links-*.sed
+	rm -f .agda-stdlib.sed .links-*.sed src/plfa/acknowledgements_epub.md
 ifneq ($(strip $(AGDAI)),)
 	rm $(AGDAI)
 endif
@@ -158,6 +158,9 @@ travis-setup:\
 	$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src\
 	$(HOME)/.agda/defaults\
 	$(HOME)/.agda/libraries\
+	$(HOME)/.local/share/lua/5.1/tinyyaml.lua\
+	$(HOME)/.local/share/lua/5.1/liquid.lua\
+	$(HOME)/.local/share/lua/5.1/cjson\
 	/usr/bin/pandoc
 
 .phony: travis-setup
@@ -204,6 +207,17 @@ $(HOME)/.local/bin/agda:
 	cd $(HOME)/agda-$(AGDA_VERSION);\
 		stack install --stack-yaml=stack-8.0.2.yaml
 
+$(HOME)/.local/share/lua/5.1/tinyyaml.lua:
+	luarocks install lua-tinyyaml
+
+$(HOME)/.local/share/lua/5.1/liquid.lua:
+	luarocks install liquid
+
+$(HOME)/.local/share/lua/5.1/cjson:
+	# Only this particular version works:
+	# https://github.com/mpx/lua-cjson/issues/56:
+	luarocks install lua-cjson 2.1.0-1
+
 travis-uninstall-agda:
 	rm -rf $(HOME)/agda-$(AGDA_VERSION)/
 	rm -f $(HOME)/.local/bin/agda
diff --git a/epub/index.md b/epub/index.md
index 1124e8d0..c6f8bf89 100644
--- a/epub/index.md
+++ b/epub/index.md
@@ -65,7 +65,7 @@ src/plfa/part2/Substitution.lagda.md
 # Backmatter
 
 ``` {.include shift-heading-level-by=1}
-src/plfa/acknowledgements.md
+src/plfa/acknowledgements_epub.md
 src/plfa/Fonts.lagda.md
 src/plfa/statistics.md
 ```
diff --git a/epub/rewrite-html-ul.lua b/epub/rewrite-html-ul.lua
new file mode 100644
index 00000000..5a83375a
--- /dev/null
+++ b/epub/rewrite-html-ul.lua
@@ -0,0 +1,5 @@
+-- Transforms '<ul class={something}>' into '<ul>'.
+function RawBlock (el)
+    el.text = el.text:gsub('%s*<%s*ul%s*class=%s*"?[%w-]+"?%s*>%s*', '<ul>')
+    return el
+end
\ No newline at end of file
diff --git a/epub/run-liquid.lua b/epub/run-liquid.lua
new file mode 100644
index 00000000..c70040bc
--- /dev/null
+++ b/epub/run-liquid.lua
@@ -0,0 +1,19 @@
+local yaml = require 'tinyyaml'
+local liquid = require 'liquid'
+
+if #arg ~= 2 then
+    print('usage: ' .. arg[0] .. ' [yaml_file] [markdown_file]')
+    os.exit(1)
+end
+
+-- 1. Read YAML metadata from file, which we nest under the key 'site'.
+local metadata = { ['site'] = yaml.parse(io.open(arg[1]):read('a')) }
+
+-- 2. Read markdown document from file.
+local document = io.open(arg[2]):read('a')
+
+-- 3. Render the markdown document with the YAML metadata as context.
+local template = liquid.Template:parse(document)
+local result = template:render(liquid.InterpreterContext:new(metadata))
+
+print(result)
\ No newline at end of file
diff --git a/src/plfa/acknowledgements.md b/src/plfa/acknowledgements.md
index f3fc8bf6..6df83e23 100644
--- a/src/plfa/acknowledgements.md
+++ b/src/plfa/acknowledgements.md
@@ -7,12 +7,14 @@ next      : /Fonts/
 ---
 
 Thank you to:
-  * The inventors of Agda, for a new playground.
-  * The authors of Software Foundations, for inspiration.
+
+* The inventors of Agda, for a new playground.
+* The authors of Software Foundations, for inspiration.
 
 
 A special thank you, for inventing ideas on which
 this book is based, and for hand-holding:
+
 <ul class="list-of-contributors">
 <li>Andreas Abel</li>
 <li>Catarina Coquand</li>
@@ -25,32 +27,34 @@ this book is based, and for hand-holding:
 <li>Ulf Norell</li>
 </ul>
 
-{%- if site.contributors or site.extra_contributors -%}
+{% if site.contributors or site.extra_contributors %}
 For pull requests big and small, and for answering questions on the Agda mailing list:
+
 <ul class="list-of-contributors">
-{%- for contributor in site.contributors -%}
+{% for contributor in site.contributors %}
   <li><a href="https://github.com/{{ contributor.github_username }}">{{ contributor.name }}</a></li>
-{%- endfor -%}
-{%- for contributor in site.extra_contributors -%}
-  {%- if contributor.name and contributor.github_username -%}
+{% endfor %}
+{% for contributor in site.extra_contributors %}
+  {% if contributor.name and contributor.github_username %}
   <li><a href="https://github.com/{{ contributor.github_username }}">{{ contributor.name }}</a></li>
-  {%- else -%}
-  {%- if contributor.name -%}
+  {% else %}
+  {% if contributor.name %}
   <li>{{ contributor.name }}</li>
-  {%- endif -%}
-  {%- if contributor.github_username -%}
+  {% endif %}
+  {% if contributor.github_username %}
   <li><a href="https://github.com/{{ contributor.github_username }}">{{ contributor.github_username }}</a></li>
-  {%- endif -%}
-  {%- endif -%}
-{%- endfor -%}
+  {% endif %}
+  {% endif %}
+{% endfor %}
 <li>[Your name goes here]</li>
 </ul>
-{%- else -%}
-{%- endif -%}
+{% else %}
+{% endif %}
 
 
 For support:
-  * EPSRC Programme Grant EP/K034413/1
-  * NSF Grant No. 1814460
-  * Foundation Sciences Mathematiques de Paris (FSMP)
-    Distinguised Professor Fellowship
+
+* EPSRC Programme Grant EP/K034413/1
+* NSF Grant No. 1814460
+* Foundation Sciences Mathematiques de Paris (FSMP)
+  Distinguised Professor Fellowship
\ No newline at end of file

From 024a62d29f6166ad303f67e568be99b8bbbac910 Mon Sep 17 00:00:00 2001
From: Michael Reed <michael@michaelreed.io>
Date: Sun, 28 Jun 2020 20:20:39 -0400
Subject: [PATCH 02/38] Fix remaining epubcheck warnings

HTML does not permit nested <p> elements, which epubcheck complains
about. This change fixes those remaining warnings.

This change also causes the Dedication on the website to be centered
when viewed in Safari, which it was not before. The EPUB output looks
the same in either version with Thorium reader 1.3 on macOS.
---
 src/plfa/dedication.md | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/plfa/dedication.md b/src/plfa/dedication.md
index 585dc757..ccbe0ff4 100644
--- a/src/plfa/dedication.md
+++ b/src/plfa/dedication.md
@@ -6,8 +6,17 @@ next      : /Preface/
 ---
 
 <p style="text-align:center;">
-  <p style="font-size:1.5em">de Philip, para Wanda</p>
-  <p style="font-size:1.17em">amor da minha vida</p>
-  <p style="font-size:1em">knock knock knock</p>
-  <p style="font-size:1em">...</p>
+  <span style="font-size:1.5em">de Philip, para Wanda</span>
+</p>
+
+<p style="text-align:center;">
+  <span style="font-size:1.17em">amor da minha vida</span>
+</p>
+
+<p style="text-align:center;">
+  <span style="font-size:1em">knock knock knock</span>
+</p>
+
+<p style="text-align:center;">
+  <span style="font-size:1em">...</span>
 </p>

From 54f7d9a90a8ef3caf4398ca661526b773c5fb623 Mon Sep 17 00:00:00 2001
From: Michael Reed <michael@michaelreed.io>
Date: Wed, 1 Jul 2020 10:57:15 -0400
Subject: [PATCH 03/38] Review: Don't build EPUB by default for now

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 9eb27434..cf11be16 100644
--- a/Makefile
+++ b/Makefile
@@ -13,7 +13,7 @@ endif
 
 
 # Build PLFA and test hyperlinks
-test: build epub
+test: build
 	ruby -S bundle exec htmlproofer '_site'
 
 

From 2e6e53d60a00d88d087fe0a1a95c99c97b8cad70 Mon Sep 17 00:00:00 2001
From: Michael Reed <michael@michaelreed.io>
Date: Wed, 1 Jul 2020 11:58:46 -0400
Subject: [PATCH 04/38] Review: Add instructions for building the EPUB

---
 README.md | 47 +++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 45 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index abec3ef5..d13c10f7 100644
--- a/README.md
+++ b/README.md
@@ -32,6 +32,12 @@ permalink: /GettingStarted/
 [ruby-html-proofer]: https://github.com/gjtorikian/html-proofer
 
 [kramdown]: https://kramdown.gettalong.org/syntax.html
+[pandoc]: https://pandoc.org/installing.html
+
+[lua]: https://www.lua.org/download.html
+[luarocks]: https://luarocks.org/
+[liquid-lua]: https://luarocks.org/modules/3scale/liquid
+[lua-cjson-broken]: https://github.com/mpx/lua-cjson/issues/56
 
 
 <!-- Status & Version Badges -->
@@ -172,9 +178,13 @@ You'll see the key sequence of the character in mini buffer.
 
 ## Dependencies for developers
 
-Building PLFA is currently supported on Linux and macOS.
+PLFA is available as both a website and an EPUB e-book,
+both of which can be built on Linux and macOS.
 PLFA is written in literate Agda with [Kramdown Markdown][kramdown].
-The book is built in three stages:
+
+### Building the website
+
+The website version of the book is built in three stages:
 
  1. The `.lagda.md` files are compiled to Markdown using Agda’s highlighter.
     (This requires several POSIX tools, such as `bash`, `sed`, and `grep`.)
@@ -216,3 +226,36 @@ If you simply wish to have a local copy of the book, e.g. for offline reading, b
 bundle install
 bundle exec jekyll serve
 ```
+
+### Building the EPUB
+
+The EPUB version of the book is built using Pandoc,
+with Lua filters,
+and the script `run-liquid.lua`,
+which wraps the library [`liquid.lua`][liquid-lua].
+Here's how to build the EPUB:
+
+1. Install a recent version of Pandoc, [available here][pandoc].
+   We recommend their official installer (on the linked page),
+   which is much faster than compiling Pandoc from source with Haskell Stack.
+
+1. Install Lua version 5.3, [available here][lua].
+   Other versions have not been tested.
+
+1. Install luarocks, [available here][luarocks],
+   which we will use to install the dependencies of `run-liquid.lua`.
+
+1. Install the dependencies of `run-liquid.lua` by running:
+   ```bash
+   luarocks install lua-cjson 2.1.0-1
+   luarocks install lua-tinyyaml
+   luarocks install liquid
+   ```
+   Be sure to install `lua-cjson` version `2.1.0-1` as specified above:
+   [newer version are broken][lua-cjson-broken].
+
+1. Finally build the EPUB by running:
+   ```bash
+   make epub
+   ```
+   Pandoc will write the EPUB to `out/plfa.epub`.

From 4e837c0975dad79de95d8b0482ba14877c29cacb Mon Sep 17 00:00:00 2001
From: Michael Reed <michael@michaelreed.io>
Date: Wed, 1 Jul 2020 17:08:19 -0400
Subject: [PATCH 05/38] run-liquid.lua: Add error checking and file output
 parameter

When running `make epub`, Make would try to satisfy the target
'src/plfa/acknowledgements_epub.md' by calling run-liquid.lua.  But due
to the use of shell redirection, Make would always create the file
acknowledgements_epub.md, even if run-liquid.lua failed, in which case
acknowledgements_epub.md would be empty.  This empty file would still
satisfy the 'src/plfa/acknowledgements_epub.md' target, allowing the
pandoc command line in the 'out/plfa.epub' target to proceed---and later
fail.

To avoid this, we now (a) add a bunch of error checking to run-liquid.lua,
and (b) write directly to acknowledgements_epub.md instead of relying on
shell redirection, so that acknowledgements_epub.md will only be created
(or modified) if run-liquid.lua succeeds.
---
 Makefile            |  2 +-
 epub/run-liquid.lua | 43 ++++++++++++++++++++++++++++++++++++++-----
 2 files changed, 39 insertions(+), 6 deletions(-)

diff --git a/Makefile b/Makefile
index cf11be16..592890f0 100644
--- a/Makefile
+++ b/Makefile
@@ -70,7 +70,7 @@ out/plfa.epub: out/ $(AGDA) $(LUA) epub/main.css src/plfa/acknowledgements_epub.
 		epub/index.md
 
 src/plfa/acknowledgements_epub.md: src/plfa/acknowledgements.md _config.yml 
-	lua epub/run-liquid.lua _config.yml $< > $@
+	lua epub/run-liquid.lua _config.yml $< $@
 
 
 # Convert literal Agda to Markdown
diff --git a/epub/run-liquid.lua b/epub/run-liquid.lua
index c70040bc..7305bea3 100644
--- a/epub/run-liquid.lua
+++ b/epub/run-liquid.lua
@@ -1,19 +1,52 @@
 local yaml = require 'tinyyaml'
 local liquid = require 'liquid'
 
-if #arg ~= 2 then
-    print('usage: ' .. arg[0] .. ' [yaml_file] [markdown_file]')
+-- Given a file name, return its file descriptor.
+-- Throws an error on failure.
+local function errOpen (fname, mode)
+    local fd = io.open(fname, mode)
+    if fd == nil then
+        error('could not open file: ' .. fname)
+    end
+    return fd
+end
+
+-- Given a file name and some data, overwrite the file with the data.
+-- Throws an error on failure.
+local function errWrite (fname, data)
+    local fd = errOpen(fname, 'w')
+    local status, errstr = fd:write(data)
+    if status == nil then
+        error(fname .. ': ' .. errstr)
+    end
+end
+
+-- Given a file name, return that file's entire contents.
+-- Throws an error on failure.
+local function errReadAll (fname)
+    local data = errOpen(fname, 'r'):read('a')
+    if data == nil then
+        error('could not read from open file: ' .. fname)
+    end
+    return data
+end
+
+
+-- We must have exactly three arguments.
+if #arg ~= 3 then
+    print('usage: ' .. arg[0] .. ' [yaml_file] [markdown_in_file] [markdown_out_file]')
     os.exit(1)
 end
 
 -- 1. Read YAML metadata from file, which we nest under the key 'site'.
-local metadata = { ['site'] = yaml.parse(io.open(arg[1]):read('a')) }
+local metadata = { ['site'] = yaml.parse(errReadAll(arg[1])) }
 
 -- 2. Read markdown document from file.
-local document = io.open(arg[2]):read('a')
+local document = errReadAll(arg[2])
 
 -- 3. Render the markdown document with the YAML metadata as context.
 local template = liquid.Template:parse(document)
 local result = template:render(liquid.InterpreterContext:new(metadata))
 
-print(result)
\ No newline at end of file
+-- 4. Write rendered document to output file.
+errWrite(arg[3], result)
\ No newline at end of file

From c76940cbb50deb83fdf4ce12db8c4ee08279db45 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 13:02:27 +0100
Subject: [PATCH 06/38] Moved generated acknowledgements to out/epub.

---
 Makefile                                            | 11 +++++++----
 epub/index.md                                       |  4 ++--
 epub/{run-liquid.lua => render-liquid-template.lua} |  0
 3 files changed, 9 insertions(+), 6 deletions(-)
 rename epub/{run-liquid.lua => render-liquid-template.lua} (100%)

diff --git a/Makefile b/Makefile
index 592890f0..55ba1160 100644
--- a/Makefile
+++ b/Makefile
@@ -50,9 +50,12 @@ out/:
 #       files are too large, so for large documents with few level-1 headings, one
 #       might want to use a chapter level of 2 or 3."
 
-epub: out/plfa.epub
+epub: out/epub/plfa.epub
 
-out/plfa.epub: out/ $(AGDA) $(LUA) epub/main.css src/plfa/acknowledgements_epub.md
+out/epub/:
+	mkdir -p out/epub/
+
+out/epub/plfa.epub: out/epub/ | $(AGDA) $(LUA) epub/main.css out/epub/acknowledgements.md
 	pandoc --strip-comments \
 		--css=epub/main.css \
 		--epub-embed-font='assets/fonts/mononoki.woff' \
@@ -69,8 +72,8 @@ out/plfa.epub: out/ $(AGDA) $(LUA) epub/main.css src/plfa/acknowledgements_epub.
 		-o "$@" \
 		epub/index.md
 
-src/plfa/acknowledgements_epub.md: src/plfa/acknowledgements.md _config.yml 
-	lua epub/run-liquid.lua _config.yml $< $@
+out/epub/acknowledgements.md: src/plfa/acknowledgements.md _config.yml
+	lua epub/render-liquid-template.lua _config.yml $< $@
 
 
 # Convert literal Agda to Markdown
diff --git a/epub/index.md b/epub/index.md
index c6f8bf89..6976f2fe 100644
--- a/epub/index.md
+++ b/epub/index.md
@@ -65,9 +65,9 @@ src/plfa/part2/Substitution.lagda.md
 # Backmatter
 
 ``` {.include shift-heading-level-by=1}
-src/plfa/acknowledgements_epub.md
+out/epub/acknowledgements.md
 src/plfa/Fonts.lagda.md
 src/plfa/statistics.md
 ```
 
-<!-- TODO: include the rest of the stuff on https://plfa.github.io/ -->
\ No newline at end of file
+<!-- TODO: include the rest of the stuff on https://plfa.github.io/ -->
diff --git a/epub/run-liquid.lua b/epub/render-liquid-template.lua
similarity index 100%
rename from epub/run-liquid.lua
rename to epub/render-liquid-template.lua

From ce40f1d96f4772017d9233ffb3f91d28154ee151 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 13:04:58 +0100
Subject: [PATCH 07/38] Updated EPUB instructions in README.

---
 README.md | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

diff --git a/README.md b/README.md
index d13c10f7..f852d53f 100644
--- a/README.md
+++ b/README.md
@@ -229,11 +229,7 @@ bundle exec jekyll serve
 
 ### Building the EPUB
 
-The EPUB version of the book is built using Pandoc,
-with Lua filters,
-and the script `run-liquid.lua`,
-which wraps the library [`liquid.lua`][liquid-lua].
-Here's how to build the EPUB:
+The EPUB version of the book is built using Pandoc, with Lua filters, and the script `epub/render-liquid-template.lua`, which wraps the library [`liquid.lua`][liquid-lua]. Here's how to build the EPUB:
 
 1. Install a recent version of Pandoc, [available here][pandoc].
    We recommend their official installer (on the linked page),
@@ -243,7 +239,7 @@ Here's how to build the EPUB:
    Other versions have not been tested.
 
 1. Install luarocks, [available here][luarocks],
-   which we will use to install the dependencies of `run-liquid.lua`.
+   which we will use to install the dependencies of `render-liquid-template.lua`.
 
 1. Install the dependencies of `run-liquid.lua` by running:
    ```bash
@@ -251,11 +247,10 @@ Here's how to build the EPUB:
    luarocks install lua-tinyyaml
    luarocks install liquid
    ```
-   Be sure to install `lua-cjson` version `2.1.0-1` as specified above:
-   [newer version are broken][lua-cjson-broken].
+   Be sure to install `lua-cjson` version `2.1.0-1` as specified above, as [newer version are broken][lua-cjson-broken].
 
 1. Finally build the EPUB by running:
    ```bash
    make epub
    ```
-   Pandoc will write the EPUB to `out/plfa.epub`.
+   Pandoc will write the EPUB to `out/epub/plfa.epub`.

From 6edc6e5b8547d2491d0b15fccb47b34507567eea Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 13:06:24 +0100
Subject: [PATCH 08/38] Fix #487

---
 src/plfa/part1/Relations.lagda.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/plfa/part1/Relations.lagda.md b/src/plfa/part1/Relations.lagda.md
index 0e621d44..fbdca82f 100644
--- a/src/plfa/part1/Relations.lagda.md
+++ b/src/plfa/part1/Relations.lagda.md
@@ -280,8 +280,8 @@ hold, then `m ≤ p` holds.  Again, `m`, `n`, and `p` are implicit:
 ≤-trans (s≤s m≤n) (s≤s n≤p)  =  s≤s (≤-trans m≤n n≤p)
 ```
 Here the proof is by induction on the _evidence_ that `m ≤ n`.  In the
-base case, the first inequality holds by `z≤n` and must show `zero ≤
-p`, which follows immediately by `z≤n`.  In this case, the fact that
+base case, the first inequality holds by `z≤n` and must show `zero ≤ p`,
+which follows immediately by `z≤n`.  In this case, the fact that
 `n ≤ p` is irrelevant, and we write `_` as the pattern to indicate
 that the corresponding evidence is unused.
 

From 2f8418a8c202b18c3e34468a7d7f1bde90dcc9d9 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 13:14:07 +0100
Subject: [PATCH 09/38] Luarocks install local

---
 .travis.yml |  1 +
 Makefile    | 10 +++-------
 2 files changed, 4 insertions(+), 7 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 97b07520..842ec274 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -12,6 +12,7 @@ cache:
   - $HOME/.stack
   - $HOME/.agda
   - $HOME/.local
+  - $HOME/.luarocks
   - $HOME/agda-$AGDA_VERSION
   - $HOME/agda-stdlib-$AGDA_STDLIB_VERSION
   - $HOME/acknowledgements-master
diff --git a/Makefile b/Makefile
index 55ba1160..18ed74a5 100644
--- a/Makefile
+++ b/Makefile
@@ -29,10 +29,6 @@ test-stable-offline: $(MARKDOWN)
 	ruby -S bundle exec htmlproofer '_site' --disable-external
 
 
-statistics:
-	hs/agda-count
-
-
 out/:
 	mkdir -p out/
 
@@ -211,15 +207,15 @@ $(HOME)/.local/bin/agda:
 		stack install --stack-yaml=stack-8.0.2.yaml
 
 $(HOME)/.local/share/lua/5.1/tinyyaml.lua:
-	luarocks install lua-tinyyaml
+	luarocks install --local lua-tinyyaml
 
 $(HOME)/.local/share/lua/5.1/liquid.lua:
-	luarocks install liquid
+	luarocks install --local liquid
 
 $(HOME)/.local/share/lua/5.1/cjson:
 	# Only this particular version works:
 	# https://github.com/mpx/lua-cjson/issues/56:
-	luarocks install lua-cjson 2.1.0-1
+	luarocks install --local lua-cjson 2.1.0-1
 
 travis-uninstall-agda:
 	rm -rf $(HOME)/agda-$(AGDA_VERSION)/

From 95b976ed1b2d577b0e70169e1d1ebf8026ed79fe Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 13:33:54 +0100
Subject: [PATCH 10/38] Minor fix.

---
 Makefile    | 2 +-
 _config.yml | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 18ed74a5..cdde572d 100644
--- a/Makefile
+++ b/Makefile
@@ -118,7 +118,7 @@ build-incremental: $(MARKDOWN)
 
 # Remove all auxiliary files
 clean:
-	rm -f .agda-stdlib.sed .links-*.sed src/plfa/acknowledgements_epub.md
+	rm -f .agda-stdlib.sed .links-*.sed out/epub/acknowledgements.md
 ifneq ($(strip $(AGDAI)),)
 	rm $(AGDAI)
 endif
diff --git a/_config.yml b/_config.yml
index 9cd89930..f0a4ac89 100644
--- a/_config.yml
+++ b/_config.yml
@@ -67,3 +67,4 @@ exclude:
   - "Gemfile"
   - "Gemfile.lock"
   - "highlight.sh"
+  - "out/epub/acknowledgements.md"

From 0b4df68fba9a7f32603208bfb22dcc210a6a15cc Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 13:40:12 +0100
Subject: [PATCH 11/38] Added EPUB build to Travis

---
 .travis.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.travis.yml b/.travis.yml
index 842ec274..70d53641 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -42,7 +42,9 @@ script:
 - agda --version
 - acknowledgements --version
 - pandoc --version
+- make build
 - make test-offline # disable to only build cache
+- make epub
 
 before_deploy:
 - acknowledgements -i _config.yml >> _config.yml

From 5728f680762145d3cd1e9a5428412e0a13df1598 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 15:46:48 +0100
Subject: [PATCH 12/38] Install packages to lua_modules/, add to path if found.

---
 .gitignore         | 5 ++---
 .travis.yml        | 1 +
 Makefile           | 7 ++++++-
 epub/set_paths.lua | 4 ++++
 4 files changed, 13 insertions(+), 4 deletions(-)
 create mode 100644 epub/set_paths.lua

diff --git a/.gitignore b/.gitignore
index 0967dd49..3a8c59f5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -21,12 +21,11 @@ Gemfile.lock
 *.spl
 *.synctex.gz
 
-## EPUB files
-*.epub
+## Lua files
+lua_modules/
 
 ## Emacs files
 auto/
 
 ## Misc build files
 out/
-src/plfa/acknowledgements_epub.md
diff --git a/.travis.yml b/.travis.yml
index 70d53641..edce3071 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -21,6 +21,7 @@ cache:
 addons:
   apt:
     packages:
+      - epubcheck
       - libgmp-dev
       - libicu-dev
       - luarocks
diff --git a/Makefile b/Makefile
index cdde572d..9edb2ab5 100644
--- a/Makefile
+++ b/Makefile
@@ -4,6 +4,11 @@ AGDAI := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*'
 LUA := $(shell find . -type f -and -path '*/epub/*' -and -name '*.lua')
 MARKDOWN := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA))))
 PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
+LUA_MODULES := lua_modules/
+
+ifneq ($(wildcard $(LUA_MODULES)),)
+	LUA_FLAGS += -l epub/set_paths
+endif
 
 ifeq ($(AGDA_STDLIB_VERSION),)
 AGDA_STDLIB_URL := https://agda.github.io/agda-stdlib/
@@ -69,7 +74,7 @@ out/epub/plfa.epub: out/epub/ | $(AGDA) $(LUA) epub/main.css out/epub/acknowledg
 		epub/index.md
 
 out/epub/acknowledgements.md: src/plfa/acknowledgements.md _config.yml
-	lua epub/render-liquid-template.lua _config.yml $< $@
+	lua $(LUA_FLAGS) epub/render-liquid-template.lua _config.yml $< $@
 
 
 # Convert literal Agda to Markdown
diff --git a/epub/set_paths.lua b/epub/set_paths.lua
new file mode 100644
index 00000000..3242dbdd
--- /dev/null
+++ b/epub/set_paths.lua
@@ -0,0 +1,4 @@
+-- set_paths.lua
+local version = _VERSION:match("%d+%.%d+")
+package.path = 'lua_modules/share/lua/' .. version .. '/?.lua;lua_modules/share/lua/' .. version .. '/?/init.lua;' .. package.path
+package.cpath = 'lua_modules/lib/lua/' .. version .. '/?.so;' .. package.cpath
\ No newline at end of file

From cfec58a2baf021b87218619fe14e38b7481e3c24 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 16:09:36 +0100
Subject: [PATCH 13/38] Install lua packages locally

---
 Makefile | 27 +++++++++++++++------------
 1 file changed, 15 insertions(+), 12 deletions(-)

diff --git a/Makefile b/Makefile
index 9edb2ab5..1290dfd8 100644
--- a/Makefile
+++ b/Makefile
@@ -4,6 +4,7 @@ AGDAI := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*'
 LUA := $(shell find . -type f -and -path '*/epub/*' -and -name '*.lua')
 MARKDOWN := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA))))
 PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
+LUA_VERSION := $(lua -e "print(string.sub(_VERSION,5))")
 LUA_MODULES := lua_modules/
 
 ifneq ($(wildcard $(LUA_MODULES)),)
@@ -162,9 +163,9 @@ travis-setup:\
 	$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src\
 	$(HOME)/.agda/defaults\
 	$(HOME)/.agda/libraries\
-	$(HOME)/.local/share/lua/5.1/tinyyaml.lua\
-	$(HOME)/.local/share/lua/5.1/liquid.lua\
-	$(HOME)/.local/share/lua/5.1/cjson\
+	lua_modules/share/lua/$(LUA_VERSION)/cjson\
+	lua_modules/share/lua/$(LUA_VERSION)/tinyyaml.lua\
+	lua_modules/share/lua/$(LUA_VERSION)/liquid.lua\
 	/usr/bin/pandoc
 
 .phony: travis-setup
@@ -180,7 +181,8 @@ $(HOME)/.local/bin/acknowledgements:
 
 # The version of pandoc on Xenial is too old.
 /usr/bin/pandoc:
-	curl -L https://github.com/jgm/pandoc/releases/download/2.9.2.1/pandoc-2.9.2.1-1-amd64.deb -o $(HOME)/pandoc.deb
+	curl -L https://github.com/jgm/pandoc/releases/download/2.9.2.1/pandoc-2.9.2.1-1-amd64.deb\
+	     -o $(HOME)/pandoc.deb
 	sudo dpkg -i $(HOME)/pandoc.deb
 
 travis-uninstall-acknowledgements:
@@ -211,16 +213,17 @@ $(HOME)/.local/bin/agda:
 	cd $(HOME)/agda-$(AGDA_VERSION);\
 		stack install --stack-yaml=stack-8.0.2.yaml
 
-$(HOME)/.local/share/lua/5.1/tinyyaml.lua:
-	luarocks install --local lua-tinyyaml
+lua_modules/share/lua/$(LUA_VERSION)/cjson:
+# Only this particular version works:
+# https://github.com/mpx/lua-cjson/issues/56:
+	luarocks install --tree lua_modules lua-cjson 2.1.0-1
+	luarocks install --tree lua_modules liquid
 
-$(HOME)/.local/share/lua/5.1/liquid.lua:
-	luarocks install --local liquid
+lua_modules/share/lua/$(LUA_VERSION)/tinyyaml.lua:
+	luarocks install --tree lua_modules lua-tinyyaml
 
-$(HOME)/.local/share/lua/5.1/cjson:
-	# Only this particular version works:
-	# https://github.com/mpx/lua-cjson/issues/56:
-	luarocks install --local lua-cjson 2.1.0-1
+lua_modules/share/lua/$(LUA_VERSION)/liquid.lua:
+	luarocks install --tree lua_modules liquid
 
 travis-uninstall-agda:
 	rm -rf $(HOME)/agda-$(AGDA_VERSION)/

From 8f0b55b4ae61df1537bf625fd8e164ea08e552e3 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 16:15:54 +0100
Subject: [PATCH 14/38] Minor fix.

---
 Makefile | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/Makefile b/Makefile
index 1290dfd8..d99e452d 100644
--- a/Makefile
+++ b/Makefile
@@ -216,14 +216,13 @@ $(HOME)/.local/bin/agda:
 lua_modules/share/lua/$(LUA_VERSION)/cjson:
 # Only this particular version works:
 # https://github.com/mpx/lua-cjson/issues/56:
-	luarocks install --tree lua_modules lua-cjson 2.1.0-1
-	luarocks install --tree lua_modules liquid
+	luarocks install --tree=lua_modules/ lua-cjson 2.1.0-1
 
 lua_modules/share/lua/$(LUA_VERSION)/tinyyaml.lua:
-	luarocks install --tree lua_modules lua-tinyyaml
+	luarocks install --tree=lua_modules/ lua-tinyyaml
 
 lua_modules/share/lua/$(LUA_VERSION)/liquid.lua:
-	luarocks install --tree lua_modules liquid
+	luarocks install --tree lua_modules/ liquid
 
 travis-uninstall-agda:
 	rm -rf $(HOME)/agda-$(AGDA_VERSION)/

From f510d870ff4e54605b6628482d21790ef4e7866c Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 16:19:57 +0100
Subject: [PATCH 15/38] Debugging travis build.

---
 .travis.yml | 1 +
 Makefile    | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/.travis.yml b/.travis.yml
index edce3071..ca514ff9 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -9,6 +9,7 @@ cache:
   timeout: 1500
   directories:
   - out/
+  - lua_modules/
   - $HOME/.stack
   - $HOME/.agda
   - $HOME/.local
diff --git a/Makefile b/Makefile
index d99e452d..8d316528 100644
--- a/Makefile
+++ b/Makefile
@@ -222,7 +222,7 @@ lua_modules/share/lua/$(LUA_VERSION)/tinyyaml.lua:
 	luarocks install --tree=lua_modules/ lua-tinyyaml
 
 lua_modules/share/lua/$(LUA_VERSION)/liquid.lua:
-	luarocks install --tree lua_modules/ liquid
+	luarocks install --tree=lua_modules/ liquid
 
 travis-uninstall-agda:
 	rm -rf $(HOME)/agda-$(AGDA_VERSION)/

From 840d93deef9328554adb7db0ec1e57bd1f8c0efa Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 19:12:58 +0100
Subject: [PATCH 16/38] Install Lua 5.3

---
 Makefile | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 8d316528..cba0300f 100644
--- a/Makefile
+++ b/Makefile
@@ -4,7 +4,6 @@ AGDAI := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*'
 LUA := $(shell find . -type f -and -path '*/epub/*' -and -name '*.lua')
 MARKDOWN := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA))))
 PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
-LUA_VERSION := $(lua -e "print(string.sub(_VERSION,5))")
 LUA_MODULES := lua_modules/
 
 ifneq ($(wildcard $(LUA_MODULES)),)
@@ -163,6 +162,7 @@ travis-setup:\
 	$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src\
 	$(HOME)/.agda/defaults\
 	$(HOME)/.agda/libraries\
+	$(HOME)/.local/bin/lua\
 	lua_modules/share/lua/$(LUA_VERSION)/cjson\
 	lua_modules/share/lua/$(LUA_VERSION)/tinyyaml.lua\
 	lua_modules/share/lua/$(LUA_VERSION)/liquid.lua\
@@ -213,6 +213,11 @@ $(HOME)/.local/bin/agda:
 	cd $(HOME)/agda-$(AGDA_VERSION);\
 		stack install --stack-yaml=stack-8.0.2.yaml
 
+$(HOME)/.local/bin/lua:
+  curl http://www.lua.org/ftp/lua-5.3.5.tar.gz | tar xz
+	make linux
+	make INSTALL_TOP=$(HOME)/.local install
+
 lua_modules/share/lua/$(LUA_VERSION)/cjson:
 # Only this particular version works:
 # https://github.com/mpx/lua-cjson/issues/56:

From 06205deaa74d3b5db7b803de5987908873ad38d4 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 19:18:06 +0100
Subject: [PATCH 17/38] Update Lua config

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index cba0300f..8badf31f 100644
--- a/Makefile
+++ b/Makefile
@@ -214,7 +214,7 @@ $(HOME)/.local/bin/agda:
 		stack install --stack-yaml=stack-8.0.2.yaml
 
 $(HOME)/.local/bin/lua:
-  curl http://www.lua.org/ftp/lua-5.3.5.tar.gz | tar xz
+  curl http://www.lua.org/ftp/lua-$(LUA_VERSION).$(LUA_PATCH_VERSION).tar.gz | tar xz
 	make linux
 	make INSTALL_TOP=$(HOME)/.local install
 

From b76a105cce8cc66e29cd15db22d27f3ec0756c54 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 19:29:52 +0100
Subject: [PATCH 18/38] Check luarocks version. Specify lua version on rocks
 install.

---
 .travis.yml | 2 ++
 Makefile    | 6 +++---
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index ca514ff9..3ae9430f 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -44,6 +44,8 @@ script:
 - agda --version
 - acknowledgements --version
 - pandoc --version
+- lua -v
+- luarocks --version
 - make build
 - make test-offline # disable to only build cache
 - make epub
diff --git a/Makefile b/Makefile
index 8badf31f..31733847 100644
--- a/Makefile
+++ b/Makefile
@@ -221,13 +221,13 @@ $(HOME)/.local/bin/lua:
 lua_modules/share/lua/$(LUA_VERSION)/cjson:
 # Only this particular version works:
 # https://github.com/mpx/lua-cjson/issues/56:
-	luarocks install --tree=lua_modules/ lua-cjson 2.1.0-1
+	luarocks install --lua-version=$(LUA_VERSION) --tree=lua_modules/ lua-cjson 2.1.0-1
 
 lua_modules/share/lua/$(LUA_VERSION)/tinyyaml.lua:
-	luarocks install --tree=lua_modules/ lua-tinyyaml
+	luarocks install --lua-version=$(LUA_VERSION) --tree=lua_modules/ lua-tinyyaml
 
 lua_modules/share/lua/$(LUA_VERSION)/liquid.lua:
-	luarocks install --tree=lua_modules/ liquid
+	luarocks install --lua-version=$(LUA_VERSION) --tree=lua_modules/ liquid
 
 travis-uninstall-agda:
 	rm -rf $(HOME)/agda-$(AGDA_VERSION)/

From 968676147ae541b25e2bb639daaebcbd5711ca8f Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 19:31:55 +0100
Subject: [PATCH 19/38] Specify lua-dir.

---
 Makefile | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Makefile b/Makefile
index 31733847..e0d75d64 100644
--- a/Makefile
+++ b/Makefile
@@ -221,13 +221,13 @@ $(HOME)/.local/bin/lua:
 lua_modules/share/lua/$(LUA_VERSION)/cjson:
 # Only this particular version works:
 # https://github.com/mpx/lua-cjson/issues/56:
-	luarocks install --lua-version=$(LUA_VERSION) --tree=lua_modules/ lua-cjson 2.1.0-1
+	luarocks install --lua-dir=$(HOME)/.local --lua-version=$(LUA_VERSION) --tree=lua_modules/ lua-cjson 2.1.0-1
 
 lua_modules/share/lua/$(LUA_VERSION)/tinyyaml.lua:
-	luarocks install --lua-version=$(LUA_VERSION) --tree=lua_modules/ lua-tinyyaml
+	luarocks install --lua-dir=$(HOME)/.local --lua-version=$(LUA_VERSION) --tree=lua_modules/ lua-tinyyaml
 
 lua_modules/share/lua/$(LUA_VERSION)/liquid.lua:
-	luarocks install --lua-version=$(LUA_VERSION) --tree=lua_modules/ liquid
+	luarocks install --lua-dir=$(HOME)/.local --lua-version=$(LUA_VERSION) --tree=lua_modules/ liquid
 
 travis-uninstall-agda:
 	rm -rf $(HOME)/agda-$(AGDA_VERSION)/

From 871052e49bef2e909742bca6a3900f5b911124fa Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 19:33:20 +0100
Subject: [PATCH 20/38] Full path to Lua

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index e0d75d64..4a198acd 100644
--- a/Makefile
+++ b/Makefile
@@ -74,7 +74,7 @@ out/epub/plfa.epub: out/epub/ | $(AGDA) $(LUA) epub/main.css out/epub/acknowledg
 		epub/index.md
 
 out/epub/acknowledgements.md: src/plfa/acknowledgements.md _config.yml
-	lua $(LUA_FLAGS) epub/render-liquid-template.lua _config.yml $< $@
+	 $(HOME)/.local/bin/lua $(LUA_FLAGS) epub/render-liquid-template.lua _config.yml $< $@
 
 
 # Convert literal Agda to Markdown

From 660e558299d924831b695c66c070d34eea928b1a Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 19:53:24 +0100
Subject: [PATCH 21/38] Major changes to Makefile

---
 Makefile | 172 ++++++++++++++++++++++++++++++++-----------------------
 1 file changed, 101 insertions(+), 71 deletions(-)

diff --git a/Makefile b/Makefile
index 4a198acd..4ace20bf 100644
--- a/Makefile
+++ b/Makefile
@@ -1,10 +1,21 @@
 SHELL := /usr/bin/env bash
-AGDA := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.lagda.md')
-AGDAI := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.agdai')
-LUA := $(shell find . -type f -and -path '*/epub/*' -and -name '*.lua')
-MARKDOWN := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA))))
+AGDA_FILES := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.lagda.md')
+AGDAI_FILES := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.agdai')
+MARKDOWN_FILES := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA_FILES))))
 PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
-LUA_MODULES := lua_modules/
+
+RUBY := ruby
+GEM := $(RUBY) -S gem
+BUNDLE := $(RUBY) -S bundle
+JEKYLL := $(JEKYLL)
+HTML_PROOFER := $(BUNDLE) exec htmlproofer
+
+LUA_FILES := $(shell find . -type f -and -path '*/epub/*' -and -name '*.lua')
+LUA_HOME := $(HOME)/.local
+LUA := $(LUA_HOME)/bin/lua
+LUAROCKS := luarocks --lua-dir=$(LUA_HOME) --lua-version=$(LUA_VERSION)
+LUA_MODULES := lua_modules
+PANDOC := /usr/bin/pandoc
 
 ifneq ($(wildcard $(LUA_MODULES)),)
 	LUA_FLAGS += -l epub/set_paths
@@ -19,19 +30,19 @@ endif
 
 # Build PLFA and test hyperlinks
 test: build
-	ruby -S bundle exec htmlproofer '_site'
+	$(HTMLPROOFER) '_site'
 
 
 # Build PLFA and test hyperlinks offline
 test-offline: build
-	ruby -S bundle exec htmlproofer '_site' --disable-external
+	$(HTMLPROOFER) '_site' --disable-external
 
 
 # Build PLFA and test hyperlinks for stable
-test-stable-offline: $(MARKDOWN)
-	ruby -S bundle exec jekyll clean
-	ruby -S bundle exec jekyll build --destination '_site/stable' --baseurl '/stable'
-	ruby -S bundle exec htmlproofer '_site' --disable-external
+test-stable-offline: $(MARKDOWN_FILES)
+	$(JEKYLL) clean
+	$(JEKYLL) build --destination '_site/stable' --baseurl '/stable'
+	$(HTMLPROOFER) '_site' --disable-external
 
 
 out/:
@@ -56,8 +67,8 @@ epub: out/epub/plfa.epub
 out/epub/:
 	mkdir -p out/epub/
 
-out/epub/plfa.epub: out/epub/ | $(AGDA) $(LUA) epub/main.css out/epub/acknowledgements.md
-	pandoc --strip-comments \
+out/epub/plfa.epub: out/epub/ | $(AGDA_FILES) $(LUA_FILES) epub/main.css out/epub/acknowledgements.md
+	$(PANDOC) --strip-comments \
 		--css=epub/main.css \
 		--epub-embed-font='assets/fonts/mononoki.woff' \
 		--epub-embed-font='assets/fonts/FreeMono.woff' \
@@ -74,7 +85,7 @@ out/epub/plfa.epub: out/epub/ | $(AGDA) $(LUA) epub/main.css out/epub/acknowledg
 		epub/index.md
 
 out/epub/acknowledgements.md: src/plfa/acknowledgements.md _config.yml
-	 $(HOME)/.local/bin/lua $(LUA_FLAGS) epub/render-liquid-template.lua _config.yml $< $@
+	 $(LUA) $(LUA_FLAGS) epub/render-liquid-template.lua _config.yml $< $@
 
 
 # Convert literal Agda to Markdown
@@ -93,17 +104,17 @@ else
 endif
 endef
 
-$(foreach agda,$(AGDA),$(eval $(call AGDA_template,$(agda))))
+$(foreach agda,$(AGDA_FILES),$(eval $(call AGDA_template,$(agda))))
 
 
 # Start server
 serve:
-	ruby -S bundle exec jekyll serve --incremental
+	$(JEKYLL) serve --incremental
 
 
 # Start background server
 server-start:
-	ruby -S bundle exec jekyll serve --no-watch --detach
+	$(JEKYLL) serve --no-watch --detach
 
 
 # Stop background server
@@ -112,26 +123,26 @@ server-stop:
 
 
 # Build website using jekyll
-build: $(MARKDOWN)
-	ruby -S bundle exec jekyll build
+build: $(MARKDOWN_FILES)
+	$(JEKYLL) build
 
 
 # Build website using jekyll incrementally
-build-incremental: $(MARKDOWN)
-	ruby -S bundle exec jekyll build --incremental
+build-incremental: $(MARKDOWN_FILES)
+	$(JEKYLL) build --incremental
 
 
 # Remove all auxiliary files
 clean:
 	rm -f .agda-stdlib.sed .links-*.sed out/epub/acknowledgements.md
-ifneq ($(strip $(AGDAI)),)
-	rm $(AGDAI)
+ifneq ($(strip $(AGDAI_FILES)),)
+	rm $(AGDAI_FILES)
 endif
 
 
 # Remove all generated files
 clobber: clean
-	ruby -S bundle exec jekyll clean
+	$(JEKYLL) clean
 	rm -rf out/
 
 .phony: clobber
@@ -139,7 +150,7 @@ clobber: clean
 
 # List all .lagda files
 ls:
-	@echo $(AGDA)
+	@echo $(AGDA_FILES)
 
 .phony: ls
 
@@ -147,10 +158,10 @@ ls:
 # MacOS Setup (install Bundler)
 macos-setup:
 	brew install libxml2
-	ruby -S gem install bundler --no-ri --no-rdoc
-	ruby -S gem install pkg-config --no-ri --no-rdoc -v "~> 1.1"
-	ruby -S bundle config build.nokogiri --use-system-libraries
-	ruby -S bundle install
+	$(GEM) install bundler --no-ri --no-rdoc
+	$(GEM) install pkg-config --no-ri --no-rdoc -v "~> 1.1"
+	$(BUNDLE) config build.nokogiri --use-system-libraries
+	$(BUNDLE) install
 
 .phony: macos-setup
 
@@ -162,37 +173,16 @@ travis-setup:\
 	$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src\
 	$(HOME)/.agda/defaults\
 	$(HOME)/.agda/libraries\
-	$(HOME)/.local/bin/lua\
-	lua_modules/share/lua/$(LUA_VERSION)/cjson\
-	lua_modules/share/lua/$(LUA_VERSION)/tinyyaml.lua\
-	lua_modules/share/lua/$(LUA_VERSION)/liquid.lua\
+	$(LUA)\
+	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/cjson\
+	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/tinyyaml.lua\
+	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/liquid.lua\
 	/usr/bin/pandoc
 
 .phony: travis-setup
 
 
-travis-install-acknowledgements: $(HOME)/.local/bin/acknowledgements
-
-$(HOME)/.local/bin/acknowledgements:
-	curl -L https://github.com/plfa/acknowledgements/archive/master.zip -o $(HOME)/acknowledgements-master.zip
-	unzip -qq $(HOME)/acknowledgements-master.zip -d $(HOME)
-	cd $(HOME)/acknowledgements-master;\
-		stack install
-
-# The version of pandoc on Xenial is too old.
-/usr/bin/pandoc:
-	curl -L https://github.com/jgm/pandoc/releases/download/2.9.2.1/pandoc-2.9.2.1-1-amd64.deb\
-	     -o $(HOME)/pandoc.deb
-	sudo dpkg -i $(HOME)/pandoc.deb
-
-travis-uninstall-acknowledgements:
-	rm -rf $(HOME)/acknowledgements-master/
-	rm $(HOME)/.local/bin/acknowledgements
-
-travis-reinstall-acknowledgements: travis-uninstall-acknowledgements travis-reinstall-acknowledgements
-
-.phony: travis-install-acknowledgements travis-uninstall-acknowledgements travis-reinstall-acknowledgements
-
+# Agda
 
 travis-install-agda:\
 	$(HOME)/.local/bin/agda\
@@ -213,22 +203,6 @@ $(HOME)/.local/bin/agda:
 	cd $(HOME)/agda-$(AGDA_VERSION);\
 		stack install --stack-yaml=stack-8.0.2.yaml
 
-$(HOME)/.local/bin/lua:
-  curl http://www.lua.org/ftp/lua-$(LUA_VERSION).$(LUA_PATCH_VERSION).tar.gz | tar xz
-	make linux
-	make INSTALL_TOP=$(HOME)/.local install
-
-lua_modules/share/lua/$(LUA_VERSION)/cjson:
-# Only this particular version works:
-# https://github.com/mpx/lua-cjson/issues/56:
-	luarocks install --lua-dir=$(HOME)/.local --lua-version=$(LUA_VERSION) --tree=lua_modules/ lua-cjson 2.1.0-1
-
-lua_modules/share/lua/$(LUA_VERSION)/tinyyaml.lua:
-	luarocks install --lua-dir=$(HOME)/.local --lua-version=$(LUA_VERSION) --tree=lua_modules/ lua-tinyyaml
-
-lua_modules/share/lua/$(LUA_VERSION)/liquid.lua:
-	luarocks install --lua-dir=$(HOME)/.local --lua-version=$(LUA_VERSION) --tree=lua_modules/ liquid
-
 travis-uninstall-agda:
 	rm -rf $(HOME)/agda-$(AGDA_VERSION)/
 	rm -f $(HOME)/.local/bin/agda
@@ -239,6 +213,8 @@ travis-reinstall-agda: travis-uninstall-agda travis-install-agda
 .phony: travis-install-agda travis-uninstall-agda travis-reinstall-agda
 
 
+# Agda Standard Library
+
 travis-install-agda-stdlib: $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src
 
 $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src:
@@ -254,3 +230,57 @@ travis-uninstall-agda-stdlib:
 travis-reinstall-agda-stdlib: travis-uninstall-agda-stdlib travis-install-agda-stdlib
 
 .phony: travis-install-agda-stdlib travis-uninstall-agda-stdlib travis-reinstall-agda-stdlib epub
+
+
+# Acknowledgements
+
+travis-install-acknowledgements: $(HOME)/.local/bin/acknowledgements
+
+$(HOME)/.local/bin/acknowledgements:
+	curl -L https://github.com/plfa/acknowledgements/archive/master.zip -o $(HOME)/acknowledgements-master.zip
+	unzip -qq $(HOME)/acknowledgements-master.zip -d $(HOME)
+	cd $(HOME)/acknowledgements-master;\
+		stack install
+
+travis-uninstall-acknowledgements:
+	rm -rf $(HOME)/acknowledgements-master/
+	rm $(HOME)/.local/bin/acknowledgements
+
+travis-reinstall-acknowledgements: travis-uninstall-acknowledgements travis-reinstall-acknowledgements
+
+.phony: travis-install-acknowledgements travis-uninstall-acknowledgements travis-reinstall-acknowledgements
+
+
+# Pandoc
+# The version of Pandoc on Xenial is too old.
+
+$(PANDOC):
+	curl -L https://github.com/jgm/pandoc/releases/download/2.9.2.1/pandoc-2.9.2.1-1-amd64.deb\
+	     -o $(HOME)/pandoc.deb
+	sudo dpkg -i $(HOME)/pandoc.deb
+
+
+# Lua
+# The version of Lua on Xenial is too old.
+
+travis-install-lua:\
+	$(LUA)\
+	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/cjson\
+	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/tinyyaml.lua\
+	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/liquid.lua\
+
+$(LUA):
+  curl http://www.lua.org/ftp/lua-$(LUA_VERSION).$(LUA_FILES_PATCH_VERSION).tar.gz | tar xz
+	make linux
+	make INSTALL_TOP=$(LUA_HOME) install
+
+$(LUA_MODULES)/share/lua/$(LUA_VERSION)/cjson:
+# Only this particular version works:
+# https://github.com/mpx/lua-cjson/issues/56:
+	$(LUAROCKS) install --tree=$(LUA_MODULES) lua-cjson 2.1.0-1
+
+$(LUA_MODULES)/share/lua/$(LUA_VERSION)/tinyyaml.lua:
+	$(LUAROCKS) install --tree=$(LUA_MODULES) lua-tinyyaml
+
+$(LUA_MODULES)/share/lua/$(LUA_VERSION)/liquid.lua:
+	$(LUAROCKS) install --tree=$(LUA_MODULES) liquid

From 69b89e8d1f3b5572f054fdd2aab45fbd89463175 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 20:10:16 +0100
Subject: [PATCH 22/38] Moving things to .travis.yaml

---
 .travis.yml |  7 +++++--
 Makefile    | 36 ++++++++++--------------------------
 2 files changed, 15 insertions(+), 28 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 3ae9430f..715f129c 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -25,19 +25,22 @@ addons:
       - epubcheck
       - libgmp-dev
       - libicu-dev
-      - luarocks
 
 # Ensure we run BASH and not SH
 env:
   - SH=bash
 
 before_install:
-# Download and unpack the stack executable
+# Install Stack
 - mkdir -p ~/.local/bin
 - export PATH=$HOME/.local/bin:$PATH
 - travis_retry curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'
 # Download and install agda, agda-stdlib, and agda2html
 - make travis-setup
+# Install Pandoc
+- travis_retry curl -L https://github.com/jgm/pandoc/releases/download/2.9.2.1/pandoc-2.9.2.1-1-amd64.deb -o $HOME/pandoc.deb && sudo dpkg -i $HOME/pandoc.deb
+# Install Lua
+- travis_retry curl -R -O http://www.lua.org/ftp/lua-5.4.0.tar.gz | tar zxf && cd lua-5.4.0 && sudo make all test
 
 script:
 - travis_retry curl -L https://raw.githubusercontent.com/plfa/git-tools/master/git-restore-mtime | python
diff --git a/Makefile b/Makefile
index 4ace20bf..d63d8c93 100644
--- a/Makefile
+++ b/Makefile
@@ -11,9 +11,8 @@ JEKYLL := $(JEKYLL)
 HTML_PROOFER := $(BUNDLE) exec htmlproofer
 
 LUA_FILES := $(shell find . -type f -and -path '*/epub/*' -and -name '*.lua')
-LUA_HOME := $(HOME)/.local
-LUA := $(LUA_HOME)/bin/lua
-LUAROCKS := luarocks --lua-dir=$(LUA_HOME) --lua-version=$(LUA_VERSION)
+LUA := lua
+LUAROCKS := luarocks --lua-version=$(LUA_VERSION)
 LUA_MODULES := lua_modules
 PANDOC := /usr/bin/pandoc
 
@@ -173,11 +172,9 @@ travis-setup:\
 	$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src\
 	$(HOME)/.agda/defaults\
 	$(HOME)/.agda/libraries\
-	$(LUA)\
 	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/cjson\
 	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/tinyyaml.lua\
-	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/liquid.lua\
-	/usr/bin/pandoc
+	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/liquid.lua
 
 .phony: travis-setup
 
@@ -198,7 +195,8 @@ $(HOME)/.agda/libraries:
 	echo "$(PLFA_DIR)/plfa.agda-lib" >> $(HOME)/.agda/libraries
 
 $(HOME)/.local/bin/agda:
-	curl -L https://github.com/agda/agda/archive/v$(AGDA_VERSION).zip -o $(HOME)/agda-$(AGDA_VERSION).zip
+	travis_retry curl -L https://github.com/agda/agda/archive/v$(AGDA_VERSION).zip\
+	                  -o $(HOME)/agda-$(AGDA_VERSION).zip
 	unzip -qq $(HOME)/agda-$(AGDA_VERSION).zip -d $(HOME)
 	cd $(HOME)/agda-$(AGDA_VERSION);\
 		stack install --stack-yaml=stack-8.0.2.yaml
@@ -218,7 +216,8 @@ travis-reinstall-agda: travis-uninstall-agda travis-install-agda
 travis-install-agda-stdlib: $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src
 
 $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src:
-	curl -L https://github.com/agda/agda-stdlib/archive/v$(AGDA_STDLIB_VERSION).zip -o $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION).zip
+	travis_retry curl -L https://github.com/agda/agda-stdlib/archive/v$(AGDA_STDLIB_VERSION).zip\
+	                  -o $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION).zip
 	unzip -qq $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION).zip -d $(HOME)
 	mkdir -p $(HOME)/.agda
 
@@ -237,7 +236,8 @@ travis-reinstall-agda-stdlib: travis-uninstall-agda-stdlib travis-install-agda-s
 travis-install-acknowledgements: $(HOME)/.local/bin/acknowledgements
 
 $(HOME)/.local/bin/acknowledgements:
-	curl -L https://github.com/plfa/acknowledgements/archive/master.zip -o $(HOME)/acknowledgements-master.zip
+	travis_retry curl -L https://github.com/plfa/acknowledgements/archive/master.zip\
+	                  -o $(HOME)/acknowledgements-master.zip
 	unzip -qq $(HOME)/acknowledgements-master.zip -d $(HOME)
 	cd $(HOME)/acknowledgements-master;\
 		stack install
@@ -251,28 +251,12 @@ travis-reinstall-acknowledgements: travis-uninstall-acknowledgements travis-rein
 .phony: travis-install-acknowledgements travis-uninstall-acknowledgements travis-reinstall-acknowledgements
 
 
-# Pandoc
-# The version of Pandoc on Xenial is too old.
-
-$(PANDOC):
-	curl -L https://github.com/jgm/pandoc/releases/download/2.9.2.1/pandoc-2.9.2.1-1-amd64.deb\
-	     -o $(HOME)/pandoc.deb
-	sudo dpkg -i $(HOME)/pandoc.deb
-
-
 # Lua
-# The version of Lua on Xenial is too old.
 
 travis-install-lua:\
-	$(LUA)\
 	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/cjson\
 	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/tinyyaml.lua\
-	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/liquid.lua\
-
-$(LUA):
-  curl http://www.lua.org/ftp/lua-$(LUA_VERSION).$(LUA_FILES_PATCH_VERSION).tar.gz | tar xz
-	make linux
-	make INSTALL_TOP=$(LUA_HOME) install
+	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/liquid.lua
 
 $(LUA_MODULES)/share/lua/$(LUA_VERSION)/cjson:
 # Only this particular version works:

From d9249935c032bb5cde2da6bd6e2b4326fcb029da Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 20:11:43 +0100
Subject: [PATCH 23/38] Fix problem in Makefile

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index d63d8c93..9225729e 100644
--- a/Makefile
+++ b/Makefile
@@ -7,7 +7,7 @@ PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
 RUBY := ruby
 GEM := $(RUBY) -S gem
 BUNDLE := $(RUBY) -S bundle
-JEKYLL := $(JEKYLL)
+JEKYLL := $(BUNDLE) exec jekyll
 HTML_PROOFER := $(BUNDLE) exec htmlproofer
 
 LUA_FILES := $(shell find . -type f -and -path '*/epub/*' -and -name '*.lua')

From 5821dc621c73dfdcb26e33b108f7b300eabe6dcb Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 20:52:33 +0100
Subject: [PATCH 24/38] Change .travis.yaml

---
 .travis.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 715f129c..6a6bb311 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -35,12 +35,12 @@ before_install:
 - mkdir -p ~/.local/bin
 - export PATH=$HOME/.local/bin:$PATH
 - travis_retry curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'
-# Download and install agda, agda-stdlib, and agda2html
-- make travis-setup
 # Install Pandoc
 - travis_retry curl -L https://github.com/jgm/pandoc/releases/download/2.9.2.1/pandoc-2.9.2.1-1-amd64.deb -o $HOME/pandoc.deb && sudo dpkg -i $HOME/pandoc.deb
 # Install Lua
 - travis_retry curl -R -O http://www.lua.org/ftp/lua-5.4.0.tar.gz | tar zxf && cd lua-5.4.0 && sudo make all test
+# Download and install agda, agda-stdlib, and agda2html
+- make travis-setup
 
 script:
 - travis_retry curl -L https://raw.githubusercontent.com/plfa/git-tools/master/git-restore-mtime | python

From 2748c8605ce4140fa76069e3cac7c97f346dc0b7 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 21:03:59 +0100
Subject: [PATCH 25/38] Install Lua and Luarocks

---
 .travis.yml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.travis.yml b/.travis.yml
index 6a6bb311..de91d53a 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -38,7 +38,8 @@ before_install:
 # Install Pandoc
 - travis_retry curl -L https://github.com/jgm/pandoc/releases/download/2.9.2.1/pandoc-2.9.2.1-1-amd64.deb -o $HOME/pandoc.deb && sudo dpkg -i $HOME/pandoc.deb
 # Install Lua
-- travis_retry curl -R -O http://www.lua.org/ftp/lua-5.4.0.tar.gz | tar zxf && cd lua-5.4.0 && sudo make all test
+- travis_retry curl -L http://www.lua.org/ftp/lua-5.4.0.tar.gz | tar zx && cd lua-5.4.0 && make linux test && sudo make install
+- travis_retry curl -L https://luarocks.org/releases/luarocks-3.3.1.tar.gz | tar zx && cd luarocks-3.3.1 && ./configure && make && sudo make install
 # Download and install agda, agda-stdlib, and agda2html
 - make travis-setup
 

From 3c0394b8a0d8da97b96bb8ff83216c609b93c347 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 21:35:20 +0100
Subject: [PATCH 26/38] Rewrote render-liquid-template in Ruby

---
 .travis.yml                     |  3 --
 Makefile                        | 38 ++----------------------
 epub/render-liquid-template.lua | 52 ---------------------------------
 epub/render-liquid-template.rb  | 19 ++++++++++++
 4 files changed, 22 insertions(+), 90 deletions(-)
 delete mode 100644 epub/render-liquid-template.lua
 create mode 100644 epub/render-liquid-template.rb

diff --git a/.travis.yml b/.travis.yml
index de91d53a..18c41fcc 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -37,9 +37,6 @@ before_install:
 - travis_retry curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'
 # Install Pandoc
 - travis_retry curl -L https://github.com/jgm/pandoc/releases/download/2.9.2.1/pandoc-2.9.2.1-1-amd64.deb -o $HOME/pandoc.deb && sudo dpkg -i $HOME/pandoc.deb
-# Install Lua
-- travis_retry curl -L http://www.lua.org/ftp/lua-5.4.0.tar.gz | tar zx && cd lua-5.4.0 && make linux test && sudo make install
-- travis_retry curl -L https://luarocks.org/releases/luarocks-3.3.1.tar.gz | tar zx && cd luarocks-3.3.1 && ./configure && make && sudo make install
 # Download and install agda, agda-stdlib, and agda2html
 - make travis-setup
 
diff --git a/Makefile b/Makefile
index 9225729e..cd3d2542 100644
--- a/Makefile
+++ b/Makefile
@@ -3,22 +3,12 @@ AGDA_FILES := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/course
 AGDAI_FILES := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.agdai')
 MARKDOWN_FILES := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA_FILES))))
 PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
-
 RUBY := ruby
 GEM := $(RUBY) -S gem
 BUNDLE := $(RUBY) -S bundle
 JEKYLL := $(BUNDLE) exec jekyll
 HTML_PROOFER := $(BUNDLE) exec htmlproofer
-
 LUA_FILES := $(shell find . -type f -and -path '*/epub/*' -and -name '*.lua')
-LUA := lua
-LUAROCKS := luarocks --lua-version=$(LUA_VERSION)
-LUA_MODULES := lua_modules
-PANDOC := /usr/bin/pandoc
-
-ifneq ($(wildcard $(LUA_MODULES)),)
-	LUA_FLAGS += -l epub/set_paths
-endif
 
 ifeq ($(AGDA_STDLIB_VERSION),)
 AGDA_STDLIB_URL := https://agda.github.io/agda-stdlib/
@@ -67,7 +57,7 @@ out/epub/:
 	mkdir -p out/epub/
 
 out/epub/plfa.epub: out/epub/ | $(AGDA_FILES) $(LUA_FILES) epub/main.css out/epub/acknowledgements.md
-	$(PANDOC) --strip-comments \
+	pandoc --strip-comments \
 		--css=epub/main.css \
 		--epub-embed-font='assets/fonts/mononoki.woff' \
 		--epub-embed-font='assets/fonts/FreeMono.woff' \
@@ -84,7 +74,7 @@ out/epub/plfa.epub: out/epub/ | $(AGDA_FILES) $(LUA_FILES) epub/main.css out/epu
 		epub/index.md
 
 out/epub/acknowledgements.md: src/plfa/acknowledgements.md _config.yml
-	 $(LUA) $(LUA_FLAGS) epub/render-liquid-template.lua _config.yml $< $@
+	 $(RUBY) epub/render-liquid-template.rb _config.yml $< $@
 
 
 # Convert literal Agda to Markdown
@@ -171,10 +161,7 @@ travis-setup:\
 	$(HOME)/.local/bin/acknowledgements\
 	$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src\
 	$(HOME)/.agda/defaults\
-	$(HOME)/.agda/libraries\
-	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/cjson\
-	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/tinyyaml.lua\
-	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/liquid.lua
+	$(HOME)/.agda/libraries
 
 .phony: travis-setup
 
@@ -249,22 +236,3 @@ travis-uninstall-acknowledgements:
 travis-reinstall-acknowledgements: travis-uninstall-acknowledgements travis-reinstall-acknowledgements
 
 .phony: travis-install-acknowledgements travis-uninstall-acknowledgements travis-reinstall-acknowledgements
-
-
-# Lua
-
-travis-install-lua:\
-	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/cjson\
-	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/tinyyaml.lua\
-	$(LUA_MODULES)/share/lua/$(LUA_VERSION)/liquid.lua
-
-$(LUA_MODULES)/share/lua/$(LUA_VERSION)/cjson:
-# Only this particular version works:
-# https://github.com/mpx/lua-cjson/issues/56:
-	$(LUAROCKS) install --tree=$(LUA_MODULES) lua-cjson 2.1.0-1
-
-$(LUA_MODULES)/share/lua/$(LUA_VERSION)/tinyyaml.lua:
-	$(LUAROCKS) install --tree=$(LUA_MODULES) lua-tinyyaml
-
-$(LUA_MODULES)/share/lua/$(LUA_VERSION)/liquid.lua:
-	$(LUAROCKS) install --tree=$(LUA_MODULES) liquid
diff --git a/epub/render-liquid-template.lua b/epub/render-liquid-template.lua
deleted file mode 100644
index 7305bea3..00000000
--- a/epub/render-liquid-template.lua
+++ /dev/null
@@ -1,52 +0,0 @@
-local yaml = require 'tinyyaml'
-local liquid = require 'liquid'
-
--- Given a file name, return its file descriptor.
--- Throws an error on failure.
-local function errOpen (fname, mode)
-    local fd = io.open(fname, mode)
-    if fd == nil then
-        error('could not open file: ' .. fname)
-    end
-    return fd
-end
-
--- Given a file name and some data, overwrite the file with the data.
--- Throws an error on failure.
-local function errWrite (fname, data)
-    local fd = errOpen(fname, 'w')
-    local status, errstr = fd:write(data)
-    if status == nil then
-        error(fname .. ': ' .. errstr)
-    end
-end
-
--- Given a file name, return that file's entire contents.
--- Throws an error on failure.
-local function errReadAll (fname)
-    local data = errOpen(fname, 'r'):read('a')
-    if data == nil then
-        error('could not read from open file: ' .. fname)
-    end
-    return data
-end
-
-
--- We must have exactly three arguments.
-if #arg ~= 3 then
-    print('usage: ' .. arg[0] .. ' [yaml_file] [markdown_in_file] [markdown_out_file]')
-    os.exit(1)
-end
-
--- 1. Read YAML metadata from file, which we nest under the key 'site'.
-local metadata = { ['site'] = yaml.parse(errReadAll(arg[1])) }
-
--- 2. Read markdown document from file.
-local document = errReadAll(arg[2])
-
--- 3. Render the markdown document with the YAML metadata as context.
-local template = liquid.Template:parse(document)
-local result = template:render(liquid.InterpreterContext:new(metadata))
-
--- 4. Write rendered document to output file.
-errWrite(arg[3], result)
\ No newline at end of file
diff --git a/epub/render-liquid-template.rb b/epub/render-liquid-template.rb
new file mode 100644
index 00000000..927b25b5
--- /dev/null
+++ b/epub/render-liquid-template.rb
@@ -0,0 +1,19 @@
+#!/usr/bin/env ruby
+require 'yaml'
+require 'liquid'
+
+unless ARGV.length == 3
+  abort "Usage: render-liquid-template.rb [yaml_file] [markdown_in_file] [markdown_out_file]"
+end
+
+yaml_file, markdown_file_in, markdown_file_out = ARGV
+
+[yaml_file, markdown_file_in].each do |file|
+  unless File.file? file
+    abort "File does not exist: '%s'" % [file]
+  end
+end
+
+metadata = { 'site' => (YAML.load (File.read yaml_file)) }
+template = Liquid::Template.parse (File.read markdown_file_in)
+File.write markdown_file_out, (template.render metadata)

From 45f40d0d8d43cdb7c314a1e881283fb86aa320ea Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 21:39:29 +0100
Subject: [PATCH 27/38] Fixed Makefile, added epubtest.

---
 .travis.yml | 5 +----
 Makefile    | 9 ++++++++-
 2 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 18c41fcc..c091104d 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -9,11 +9,9 @@ cache:
   timeout: 1500
   directories:
   - out/
-  - lua_modules/
   - $HOME/.stack
   - $HOME/.agda
   - $HOME/.local
-  - $HOME/.luarocks
   - $HOME/agda-$AGDA_VERSION
   - $HOME/agda-stdlib-$AGDA_STDLIB_VERSION
   - $HOME/acknowledgements-master
@@ -45,11 +43,10 @@ script:
 - agda --version
 - acknowledgements --version
 - pandoc --version
-- lua -v
-- luarocks --version
 - make build
 - make test-offline # disable to only build cache
 - make epub
+- make epubcheck
 
 before_deploy:
 - acknowledgements -i _config.yml >> _config.yml
diff --git a/Makefile b/Makefile
index cd3d2542..1b600216 100644
--- a/Makefile
+++ b/Makefile
@@ -3,6 +3,8 @@ AGDA_FILES := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/course
 AGDAI_FILES := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.agdai')
 MARKDOWN_FILES := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA_FILES))))
 PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
+PANDOC := pandoc
+EPUBCHECK := epubcheck
 RUBY := ruby
 GEM := $(RUBY) -S gem
 BUNDLE := $(RUBY) -S bundle
@@ -53,11 +55,14 @@ out/:
 
 epub: out/epub/plfa.epub
 
+epubcheck: out/epub/plfa.epub
+	$(EPUBCHECK) out/epub/plfa.epub
+
 out/epub/:
 	mkdir -p out/epub/
 
 out/epub/plfa.epub: out/epub/ | $(AGDA_FILES) $(LUA_FILES) epub/main.css out/epub/acknowledgements.md
-	pandoc --strip-comments \
+	$(PANDOC) --strip-comments \
 		--css=epub/main.css \
 		--epub-embed-font='assets/fonts/mononoki.woff' \
 		--epub-embed-font='assets/fonts/FreeMono.woff' \
@@ -76,6 +81,8 @@ out/epub/plfa.epub: out/epub/ | $(AGDA_FILES) $(LUA_FILES) epub/main.css out/epu
 out/epub/acknowledgements.md: src/plfa/acknowledgements.md _config.yml
 	 $(RUBY) epub/render-liquid-template.rb _config.yml $< $@
 
+.phony: epub epubcheck
+
 
 # Convert literal Agda to Markdown
 define AGDA_template

From 615cdfe2456ac5ee3598e064e2b5f5a8610154dd Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 21:54:08 +0100
Subject: [PATCH 28/38] Adding 'liquid' as a dependency.

---
 Gemfile  | 5 +++++
 Makefile | 2 +-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/Gemfile b/Gemfile
index 1eac9d04..4ae04980 100644
--- a/Gemfile
+++ b/Gemfile
@@ -9,3 +9,8 @@ group :development do
   gem 'guard-shell'
   gem 'html-proofer'
 end
+
+group :epub do
+  gem 'safe_yaml'
+  gem 'liquid'
+end
diff --git a/Makefile b/Makefile
index 1b600216..8c4566fb 100644
--- a/Makefile
+++ b/Makefile
@@ -9,7 +9,7 @@ RUBY := ruby
 GEM := $(RUBY) -S gem
 BUNDLE := $(RUBY) -S bundle
 JEKYLL := $(BUNDLE) exec jekyll
-HTML_PROOFER := $(BUNDLE) exec htmlproofer
+HTMLPROOFER := $(BUNDLE) exec htmlproofer
 LUA_FILES := $(shell find . -type f -and -path '*/epub/*' -and -name '*.lua')
 
 ifeq ($(AGDA_STDLIB_VERSION),)

From eab2370701c27b8fff41aa44bc70d83c1e79fad7 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 21:55:05 +0100
Subject: [PATCH 29/38] Simplify .travis.yml

---
 .travis.yml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index c091104d..3bb8cf43 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -43,10 +43,8 @@ script:
 - agda --version
 - acknowledgements --version
 - pandoc --version
-- make build
-- make test-offline # disable to only build cache
-- make epub
-- make epubcheck
+- make build test-offline # disable to only build cache
+- make epub epubcheck
 
 before_deploy:
 - acknowledgements -i _config.yml >> _config.yml

From 0b63dd967a77aaecc07b6cbce9f238749fb3129a Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 22:08:27 +0100
Subject: [PATCH 30/38] Most hilarious ruby command ever.

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 8c4566fb..7aa41250 100644
--- a/Makefile
+++ b/Makefile
@@ -79,7 +79,7 @@ out/epub/plfa.epub: out/epub/ | $(AGDA_FILES) $(LUA_FILES) epub/main.css out/epu
 		epub/index.md
 
 out/epub/acknowledgements.md: src/plfa/acknowledgements.md _config.yml
-	 $(RUBY) epub/render-liquid-template.rb _config.yml $< $@
+	 $(BUNDLE) $(RUBY) epub/render-liquid-template.rb _config.yml $< $@
 
 .phony: epub epubcheck
 

From c021bcc82c43596c27cfe1a4327c79d573463dc7 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 22:21:18 +0100
Subject: [PATCH 31/38] Rewrote README to remove all the Lua stuff...

---
 README.md | 26 ++++----------------------
 1 file changed, 4 insertions(+), 22 deletions(-)

diff --git a/README.md b/README.md
index f852d53f..f48d015b 100644
--- a/README.md
+++ b/README.md
@@ -33,11 +33,7 @@ permalink: /GettingStarted/
 
 [kramdown]: https://kramdown.gettalong.org/syntax.html
 [pandoc]: https://pandoc.org/installing.html
-
-[lua]: https://www.lua.org/download.html
-[luarocks]: https://luarocks.org/
-[liquid-lua]: https://luarocks.org/modules/3scale/liquid
-[lua-cjson-broken]: https://github.com/mpx/lua-cjson/issues/56
+[epubcheck]: https://github.com/w3c/epubcheck
 
 
 <!-- Status & Version Badges -->
@@ -229,28 +225,14 @@ bundle exec jekyll serve
 
 ### Building the EPUB
 
-The EPUB version of the book is built using Pandoc, with Lua filters, and the script `epub/render-liquid-template.lua`, which wraps the library [`liquid.lua`][liquid-lua]. Here's how to build the EPUB:
+The EPUB version of the book is built using Pandoc. Here's how to build the EPUB:
 
 1. Install a recent version of Pandoc, [available here][pandoc].
    We recommend their official installer (on the linked page),
    which is much faster than compiling Pandoc from source with Haskell Stack.
 
-1. Install Lua version 5.3, [available here][lua].
-   Other versions have not been tested.
-
-1. Install luarocks, [available here][luarocks],
-   which we will use to install the dependencies of `render-liquid-template.lua`.
-
-1. Install the dependencies of `run-liquid.lua` by running:
-   ```bash
-   luarocks install lua-cjson 2.1.0-1
-   luarocks install lua-tinyyaml
-   luarocks install liquid
-   ```
-   Be sure to install `lua-cjson` version `2.1.0-1` as specified above, as [newer version are broken][lua-cjson-broken].
-
-1. Finally build the EPUB by running:
+2. Build the EPUB by running:
    ```bash
    make epub
    ```
-   Pandoc will write the EPUB to `out/epub/plfa.epub`.
+   The EPUB is written to `out/epub/plfa.epub`.

From bce8bb3d8943a5f4dbe472f6754f325d2a225c3d Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 22:22:13 +0100
Subject: [PATCH 32/38] Forgotten exec.

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 7aa41250..c57666b0 100644
--- a/Makefile
+++ b/Makefile
@@ -79,7 +79,7 @@ out/epub/plfa.epub: out/epub/ | $(AGDA_FILES) $(LUA_FILES) epub/main.css out/epu
 		epub/index.md
 
 out/epub/acknowledgements.md: src/plfa/acknowledgements.md _config.yml
-	 $(BUNDLE) $(RUBY) epub/render-liquid-template.rb _config.yml $< $@
+	 $(BUNDLE) exec ruby epub/render-liquid-template.rb _config.yml $< $@
 
 .phony: epub epubcheck
 

From 45203c2705e6e6f9088b93ffba4c813cc772fd42 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 23:25:59 +0100
Subject: [PATCH 33/38] Moved up acknowledgements.

---
 .travis.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 3bb8cf43..7c986b8a 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -43,11 +43,11 @@ script:
 - agda --version
 - acknowledgements --version
 - pandoc --version
-- make build test-offline # disable to only build cache
-- make epub epubcheck
+- make test-offline # build and test website
+- acknowledgements -i _config.yml >> _config.yml
+- make epubcheck # build and test EPUB
 
 before_deploy:
-- acknowledgements -i _config.yml >> _config.yml
 - make clean
 - rm -rf hs/ extra/ depr/ papers/ slides/ .bundle/ vendor/ *.agdai *.agda-lib *.lagda.md Guardfile Gemfile Gemfile.lock Makefile highlight.sh .gitignore .travis.yml
 

From 23a11a68aab064b7a261d76f5aeee859638dd1be Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Thu, 2 Jul 2020 23:47:27 +0100
Subject: [PATCH 34/38] Fix #476

---
 highlight.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/highlight.sh b/highlight.sh
index e6caefb9..29aa5b1f 100755
--- a/highlight.sh
+++ b/highlight.sh
@@ -110,7 +110,7 @@ for INCLUDE_PATH in "$@"; do
             find "$INCLUDE_PATH" -name "*.lagda.md" -print0 | while read -d $'\0' AGDA_MODULE_SRC; do
                 AGDA_MODULE_OUT="$(out_path "$AGDA_MODULE_SRC")"
                 AGDA_MODULE_HTML="$(basename "$(html_path "$AGDA_MODULE_SRC" "$HTML_DIR")" .md).html"
-                echo "s|$AGDA_MODULE_HTML|{% endraw %}{{ site.baseurl }}{% link $AGDA_MODULE_OUT %}{% raw %}|;" >> "$LOCAL_LINKS_SED"
+                echo "s|$AGDA_MODULE_HTML|{% endraw %}{{ site.baseurl }}{% link $AGDA_MODULE_OUT %}{% raw %}|g;" >> "$LOCAL_LINKS_SED"
             done
         fi
 

From 972cdf14a444f595591b83b29ad57a11f4c6153d Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Fri, 3 Jul 2020 00:23:11 +0100
Subject: [PATCH 35/38] removed superfluous lua script, moved acknowledgements

---
 .travis.yml        | 2 +-
 epub/set_paths.lua | 4 ----
 2 files changed, 1 insertion(+), 5 deletions(-)
 delete mode 100644 epub/set_paths.lua

diff --git a/.travis.yml b/.travis.yml
index 7c986b8a..7747c77a 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -43,8 +43,8 @@ script:
 - agda --version
 - acknowledgements --version
 - pandoc --version
-- make test-offline # build and test website
 - acknowledgements -i _config.yml >> _config.yml
+- make test-offline # build and test website
 - make epubcheck # build and test EPUB
 
 before_deploy:
diff --git a/epub/set_paths.lua b/epub/set_paths.lua
deleted file mode 100644
index 3242dbdd..00000000
--- a/epub/set_paths.lua
+++ /dev/null
@@ -1,4 +0,0 @@
--- set_paths.lua
-local version = _VERSION:match("%d+%.%d+")
-package.path = 'lua_modules/share/lua/' .. version .. '/?.lua;lua_modules/share/lua/' .. version .. '/?/init.lua;' .. package.path
-package.cpath = 'lua_modules/lib/lua/' .. version .. '/?.so;' .. package.cpath
\ No newline at end of file

From ec10e247011ded6ba59c3d7a1c22d3a157e0132a Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Fri, 3 Jul 2020 15:23:02 +0100
Subject: [PATCH 36/38] Don't cache out/

---
 .travis.yml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 7747c77a..c6144bbb 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -8,7 +8,6 @@ cache:
   bundler: true
   timeout: 1500
   directories:
-  - out/
   - $HOME/.stack
   - $HOME/.agda
   - $HOME/.local
@@ -29,17 +28,16 @@ env:
   - SH=bash
 
 before_install:
-# Install Stack
+# Install Stack:
 - mkdir -p ~/.local/bin
 - export PATH=$HOME/.local/bin:$PATH
 - travis_retry curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'
-# Install Pandoc
+# Install Pandoc:
 - travis_retry curl -L https://github.com/jgm/pandoc/releases/download/2.9.2.1/pandoc-2.9.2.1-1-amd64.deb -o $HOME/pandoc.deb && sudo dpkg -i $HOME/pandoc.deb
-# Download and install agda, agda-stdlib, and agda2html
+# Install agda, agda-stdlib, and agda2html:
 - make travis-setup
 
 script:
-- travis_retry curl -L https://raw.githubusercontent.com/plfa/git-tools/master/git-restore-mtime | python
 - agda --version
 - acknowledgements --version
 - pandoc --version

From 15e7086daba0e05bf504db586e2e20fd55a232d9 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Fri, 3 Jul 2020 15:56:08 +0100
Subject: [PATCH 37/38] Announce EPUB

---
 _posts/2020-06-02-plfa-as-epub.md | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 _posts/2020-06-02-plfa-as-epub.md

diff --git a/_posts/2020-06-02-plfa-as-epub.md b/_posts/2020-06-02-plfa-as-epub.md
new file mode 100644
index 00000000..0d7578de
--- /dev/null
+++ b/_posts/2020-06-02-plfa-as-epub.md
@@ -0,0 +1,10 @@
+---
+layout : post
+title  : "PLFA as EPUB"
+---
+
+It has been just over a year and a half since this feature was first requested in (#112)[issue112]… Thanks to hard work by [Michael Reed](mreed20), and a little elbow grease on our part, it is finally here! [An EPUB version of PLFA!][epub]
+
+[epub]: https://plfa.github.io/out/epub/plfa.epub
+[issue112]: https://github.com/plfa/plfa.github.io/issues/112
+[mreed20]: https://github.com/mreed20

From dedf93666dfa9575445073e1bc6e208eb7318e12 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Fri, 3 Jul 2020 16:26:19 +0100
Subject: [PATCH 38/38] Fix Markdown in announcement

---
 _posts/2020-06-02-plfa-as-epub.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/_posts/2020-06-02-plfa-as-epub.md b/_posts/2020-06-02-plfa-as-epub.md
index 0d7578de..1fff7fed 100644
--- a/_posts/2020-06-02-plfa-as-epub.md
+++ b/_posts/2020-06-02-plfa-as-epub.md
@@ -3,7 +3,7 @@ layout : post
 title  : "PLFA as EPUB"
 ---
 
-It has been just over a year and a half since this feature was first requested in (#112)[issue112]… Thanks to hard work by [Michael Reed](mreed20), and a little elbow grease on our part, it is finally here! [An EPUB version of PLFA!][epub]
+It has been just over a year and a half since this feature was first requested in [#112][issue112]… Thanks to hard work by [Michael Reed][mreed20], and a little elbow grease on our part, it is finally here! [An EPUB version of PLFA!][epub]
 
 [epub]: https://plfa.github.io/out/epub/plfa.epub
 [issue112]: https://github.com/plfa/plfa.github.io/issues/112