From 2987995c7ab475d6e7c817895eab82c30ceb16ba Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Tue, 24 Aug 2021 01:01:23 +0100 Subject: [PATCH] WIP rewrite of book rendering. --- Makefile | 146 +++--------------- .../DejaVu-mononoki-Symbola-Droid.ttf | Bin book/epub.css | 90 +++++++++++ book/epub.md | 71 +++++++++ book/epub.mk | 38 +++++ {src/plfa => book}/epub.xml | 0 .../lua/epub-clean-html.lua | 0 {epub => book/lua}/include-files.lua | 16 +- .../lua/latex-render-codeblocks.lua | 50 +++--- book/lua/remove-badges.lua | 22 +++ .../lua/set-default-code-class.lua | 12 +- book/lua/single-file-headers.lua | 57 +++++++ .../lua/single-file-links.lua | 0 book/pdf.mk | 122 +++++++++++++++ pdf/plfa.tex => book/pdf.tex | 1 - css/epub.css | 42 ----- epub/render-liquid-template.rb | 19 --- epub/rewrite-links.lua | 19 --- hs/Hakyll/Web/Routes/Permalink.hs | 12 +- hs/Main.hs | 97 +++--------- pdf/lua/remove-badges.lua | 12 -- pdf/lua/single-file-headers-ids.lua | 50 ------ pdf/templates/acknowledgements.latex | 4 - pdf/templates/chapter.latex | 3 - src/plfa/epub.md | 7 - templates/epub.html | 26 ---- 26 files changed, 486 insertions(+), 430 deletions(-) rename {pdf => book}/DejaVu-mononoki-Symbola-Droid.ttf (100%) create mode 100644 book/epub.css create mode 100644 book/epub.md create mode 100644 book/epub.mk rename {src/plfa => book}/epub.xml (100%) rename epub/rewrite-html-ul.lua => book/lua/epub-clean-html.lua (100%) rename {epub => book/lua}/include-files.lua (86%) rename pdf/lua/typeset-codeblocks.lua => book/lua/latex-render-codeblocks.lua (59%) create mode 100644 book/lua/remove-badges.lua rename epub/default-code-class.lua => book/lua/set-default-code-class.lua (73%) create mode 100644 book/lua/single-file-headers.lua rename pdf/lua/rewrite-links.lua => book/lua/single-file-links.lua (100%) create mode 100644 book/pdf.mk rename pdf/plfa.tex => book/pdf.tex (99%) delete mode 100644 css/epub.css delete mode 100644 epub/render-liquid-template.rb delete mode 100644 epub/rewrite-links.lua delete mode 100644 pdf/lua/remove-badges.lua delete mode 100644 pdf/lua/single-file-headers-ids.lua delete mode 100644 pdf/templates/acknowledgements.latex delete mode 100644 pdf/templates/chapter.latex delete mode 100644 src/plfa/epub.md delete mode 100644 templates/epub.html diff --git a/Makefile b/Makefile index 7a40b317..aa873dfe 100644 --- a/Makefile +++ b/Makefile @@ -1,17 +1,14 @@ + ################################################################################# # Configuration ################################################################################# -SITE_DIR := _site +SITE_DIR := _site CACHE_DIR := _cache -TMP_DIR := $(CACHE_DIR)/tmp +TMP_DIR := $(CACHE_DIR)/tmp -AGDA := stack exec agda -- \ - --no-libraries \ - --include-path=standard-library/src -PANDOC := stack exec pandoc -- \ - --indented-code-classes=default - --top-level-division=chapter +AGDA := stack exec agda -- --no-libraries --include-path=standard-library/src +PANDOC := stack exec pandoc -- ################################################################################# @@ -57,15 +54,6 @@ test: setup-install-htmlproofer build . -################################################################################# -# Test generated EPUB with EPUBCheck -################################################################################# - -.PHONY: test-epub -test-epub: setup-check-epubcheck build - epubcheck $(SITE_DIR)/plfa.epub - - ################################################################################# # Automatically rebuild the site on changes, and start a preview server ################################################################################# @@ -161,118 +149,18 @@ endif endif +################################################################################# +# Build EPUB +################################################################################# + +include book/epub.mk + + ################################################################################# # Build PDF ################################################################################# -PDF_DIR := pdf -PDF_TEMPLATE_DIR := $(PDF_DIR)/templates -PDF_LUA_DIR := $(PDF_DIR)/lua -MD_DIR := src -LAGDA_TEX_DIR := $(TMP_DIR)/lagda_tex -TEX_DIR := $(TMP_DIR)/tex - -# Convert MD_DIR/%.lagda.md to LAGDA_TEX_DIR/%.lagda.tex -define LAGDA_TEX_PATH -$(patsubst $(MD_DIR)/%.lagda.md,$(LAGDA_TEX_DIR)/%.lagda.tex,$(1)) -endef - -# Convert MD_DIR/%.md to LAGDA_TEX_DIR/%.lagda.tex or TEX_DIR/%.tex -define TEX_PATH -$(patsubst $(PDF_DIR)/%,$(TEX_DIR)/%,\ - $(patsubst README.md,$(TEX_DIR)/plfa/frontmatter/README.tex,\ - $(patsubst $(MD_DIR)/%.md,$(TEX_DIR)/%.tex,\ - $(patsubst $(MD_DIR)/%.lagda.md,$(TEX_DIR)/%.tex,$(1))))) -endef - -# List source and intermediate files -PDF_LUA_SCRIPTS := $(wildcard $(PDF_LUA_DIR)/*.lua) -PDF_STATIC_FILES := $(wildcard pdf/*.*) -MD_FILES := README.md $(wildcard $(MD_DIR)/plfa/**/*.md) -LAGDA_MD_FILES := $(filter %.lagda.md,$(MD_FILES)) -LAGDA_TEX_FILES := $(call LAGDA_TEX_PATH,$(LAGDA_MD_FILES)) -TEX_FILES := $(call TEX_PATH,$(MD_FILES) $(PDF_STATIC_FILES)) - -# Compile PLFA to a PDF -.PHONY: pdf -pdf: $(SITE_DIR)/plfa.pdf - -$(SITE_DIR)/plfa.pdf: $(TEX_FILES) - @cd $(TEX_DIR) && latexmk -pdf -lualatex -use-make -halt-on-error plfa.tex - @cp $(TEX_DIR)/plfa.pdf $(SITE_DIR)/plfa.pdf - - -# Copy static files needed by PDF compilation -define MK_COPYSTATIC_RULE -src := $(1) -dst := $(2) -$$(dst): $$(src) - @echo "Copy $$< to $$@" - @cp $$< $$@ -endef - -# Compile Markdown files to LaTeX -define MK_MD2TEX_RULE -src := $(1) -dst := $(2) -tpl := $(3) -$$(dst): export UNCHECKED_FILES = README.md -$$(dst): $$(src) $$(tpl) $(PDF_LUA_SCRIPTS) | setup-install-pandoc - @echo "Compile $$< to $$@" - @mkdir -p '$$(@D)' - @$(PANDOC) \ - --lua-filter=$(PDF_LUA_DIR)/remove-badges.lua \ - --lua-filter=$(PDF_LUA_DIR)/typeset-codeblocks.lua \ - --lua-filter=$(PDF_LUA_DIR)/rewrite-links.lua \ - --lua-filter=$(PDF_LUA_DIR)/single-file-headers-ids.lua \ - --template=$$(tpl) \ - $$< -o $$@ -endef - -# Compile Literate Agda files to LaTeX -define MK_LAGDA_MD2TEX_RULE -src := $(1) -dst := $(2) -$$(dst): $$(src) $(LAGDA_TEX_FILES) | setup-install-agda - @$(AGDA) --include-path=$(LAGDA_TEX_DIR) --latex --latex-dir=$(TEX_DIR) $$< -endef - - -# Copy static files (from PDF_DIR/% to TEX_DIR/%) -$(foreach static_file,\ - $(PDF_STATIC_FILES),\ - $(eval $(call MK_COPYSTATIC_RULE,\ - $(static_file),\ - $(call TEX_PATH,$(static_file))))) - -# Compile .md files (from MD_DIR/%.md to TEX_DIR/%.tex) -$(foreach md_file,\ - $(filter-out %acknowledgements.md %.lagda.md,$(MD_FILES)),\ - $(eval $(call MK_MD2TEX_RULE,\ - $(md_file),\ - $(call TEX_PATH,$(md_file)),\ - $(PDF_TEMPLATE_DIR)/chapter.latex))) - -# Compile .lagda.md files (from MD_DIR/%.md to LAGDA_TEX_DIR/%.lagda.tex) -$(foreach lagda_md_file,\ - $(LAGDA_MD_FILES),\ - $(eval $(call MK_MD2TEX_RULE,\ - $(lagda_md_file),\ - $(call LAGDA_TEX_PATH,$(lagda_md_file)),\ - $(PDF_TEMPLATE_DIR)/chapter.latex))) - -# Compile acknowledgements (from SITE_DIR/acknowledgements.md to TEX_DIR/acknowledgements.tex) -$(eval $(call MK_MD2TEX_RULE,\ - $(SITE_DIR)/acknowledgements.md,\ - $(TEX_DIR)/plfa/backmatter/acknowledgements.tex,\ - $(PDF_TEMPLATE_DIR)/acknowledgements.latex)) - -# Compile .lagda.tex files (from LAGDA_TEX_DIR/%.lagda.tex to TEX_DIR/%.tex) -$(foreach lagda_md_file,\ - $(LAGDA_MD_FILES),\ - $(eval $(call MK_LAGDA_MD2TEX_RULE,\ - $(call LAGDA_TEX_PATH,$(lagda_md_file)),\ - $(call TEX_PATH,$(lagda_md_file))))) +include book/pdf.mk ################################################################################# @@ -312,6 +200,14 @@ ifeq (,$(wildcard $(shell which fix-whitespace))) @echo " stack install --stack-yaml stack-8.8.3.yaml" endif +.PHONY: setup-check-latexmk +setup-check-latexmk: +ifeq (,$(wildcard $(shell which latexmk))) + @echo "The command you called requires Latexmk" + @echo "Latemk is included in MacTeX and MikTeX" + @echo "See: https://mg.readthedocs.io/latexmk.html" +endif + .PHONY: setup-check-epubcheck setup-check-epubcheck: ifeq (,$(wildcard $(shell which epubcheck))) diff --git a/pdf/DejaVu-mononoki-Symbola-Droid.ttf b/book/DejaVu-mononoki-Symbola-Droid.ttf similarity index 100% rename from pdf/DejaVu-mononoki-Symbola-Droid.ttf rename to book/DejaVu-mononoki-Symbola-Droid.ttf diff --git a/book/epub.css b/book/epub.css new file mode 100644 index 00000000..b6a50a63 --- /dev/null +++ b/book/epub.css @@ -0,0 +1,90 @@ +/* This is Pandoc's default ebook CSS, modified slightly. */ +/* https://github.com/jgm/pandoc/blob/master/data/epub.css */ +@font-face { + font-family: 'DejaVu-mononoki-Symbola-Droid'; + font-weight: normal; + font-style: normal; + src: url('../public/webfonts/DejaVu-mononoki-Symbola-Droid.woff'); +} + +body { + margin: 5%; + text-align: justify; + font-size: medium; +} + +code { + font-family: 'DejaVu-mononoki-Symbola-Droid', monospace; +} + +h1, +h2, +h3, +h4, +h5, +h6 { + text-align: left; +} + +nav#toc ol, +nav#landmarks ol { + padding: 0; + margin-left: 1em; +} + +nav#toc ol li, +nav#landmarks ol li { + list-style-type: none; + margin: 0; + padding: 0; +} + +a.footnote-ref { + vertical-align: super; +} + +em, +em em em, +em em em em em { + font-style: italic; +} + +em em, +em em em em { + font-style: normal; +} + +code { + white-space: pre-wrap; +} + +span.smallcaps { + font-variant: small-caps; +} + +span.underline { + text-decoration: underline; +} + +q { + quotes: "“""”""‘""’"; +} + +div.column { + display: inline-block; + vertical-align: top; + width: 50%; +} + +div.hanging-indent { + margin-left: 1.5em; + text-indent: -1.5em; +} + +/* Workaround for iBooks issue; see #6242 */ +@media screen { + .sourceCode { + overflow: visible !important; + white-space: pre-wrap !important; + } +} diff --git a/book/epub.md b/book/epub.md new file mode 100644 index 00000000..d6ef5e0f --- /dev/null +++ b/book/epub.md @@ -0,0 +1,71 @@ +--- +title: Programming Language Foundations in Agda +author: +- Philip Wadler +- Wen Kokke +- Jeremy G. Siek +description: This book is an introduction to programming language theory using the proof assistant Agda. +rights: Creative Commons Attribution 4.0 International License +language: en-US +--- + +# Front matter + +``` {.include shift-heading-level-by=1} +src/plfa/frontmatter/dedication.md +src/plfa/frontmatter/preface.md +``` + +# Part 1: Logical Foundations + +``` {.include shift-heading-level-by=1} +src/plfa/part1/Naturals.lagda.md +src/plfa/part1/Induction.lagda.md +src/plfa/part1/Relations.lagda.md +src/plfa/part1/Equality.lagda.md +src/plfa/part1/Isomorphism.lagda.md +src/plfa/part1/Connectives.lagda.md +src/plfa/part1/Negation.lagda.md +src/plfa/part1/Quantifiers.lagda.md +src/plfa/part1/Decidable.lagda.md +src/plfa/part1/Lists.lagda.md +``` + +# Part 2: Operational Semantics + +``` {.include shift-heading-level-by=1} +src/plfa/part2/Lambda.lagda.md +src/plfa/part2/Properties.lagda.md +src/plfa/part2/DeBruijn.lagda.md +src/plfa/part2/More.lagda.md +src/plfa/part2/Bisimulation.lagda.md +src/plfa/part2/Inference.lagda.md +src/plfa/part2/Untyped.lagda.md +src/plfa/part2/Confluence.lagda.md +src/plfa/part2/BigStep.lagda.md +``` + +# Part 3: Denotational Semantics + +``` {.include shift-heading-level-by=1} +src/plfa/part3/Denotational.lagda.md +src/plfa/part3/Compositional.lagda.md +src/plfa/part3/Soundness.lagda.md +src/plfa/part3/Adequacy.lagda.md +src/plfa/part3/ContextualEquivalence.lagda.md +``` + +# Appendix + +``` {.include shift-heading-level-by=1} +src/plfa/part2/Substitution.lagda.md +``` + + +# Backmatter + +## Acknowledgements +``` {.include shift-heading-level-by=1} +_site/acknowledgements.md +src/plfa/backmatter/Fonts.lagda.md +``` diff --git a/book/epub.mk b/book/epub.mk new file mode 100644 index 00000000..93839871 --- /dev/null +++ b/book/epub.mk @@ -0,0 +1,38 @@ +EPUB_DIR := book +EPUB_TEMPLATE_DIR := $(EPUB_DIR)/templates +EPUB_LUA_DIR := $(EPUB_DIR)/lua +EPUB_LUA_SCRIPTS := $(wildcard $(EPUB_LUA_DIR)/*.lua) +MD_DIR := src +MD_FILES := README.md $(wildcard $(MD_DIR)/plfa/**/*.md) + + +# Compile PLFA to an EPUB +.PHONY: epub +epub: $(SITE_DIR)/plfa.epub + +$(SITE_DIR)/plfa.epub: book/epub.md book/epub.css $(MD_FILES) $(EPUB_LUA_SCRIPTS) | setup-install-pandoc + @$(PANDOC) \ + --strip-comments \ + --css=epub/epub.css \ + --epub-embed-font='public/webfonts/DejaVu-mononoki-Symbola-Droid.woff' \ + --lua-filter=$(EPUB_LUA_DIR)/include-files.lua \ + --lua-filter=$(EPUB_LUA_DIR)/single-file-links.lua \ + --lua-filter=$(EPUB_LUA_DIR)/epub-clean-html.lua \ + --lua-filter=$(EPUB_LUA_DIR)/set-default-code-class.lua -M default-code-class=agda \ + --standalone \ + --fail-if-warnings \ + --toc --toc-depth=2 \ + --epub-chapter-level=2 \ + $< -o $@ + + +# Test EPUB with EPUBCheck +.PHONY: epub-test +epub-test: $(SITE_DIR)/plfa.epub | setup-check-epubcheck + epubcheck $(SITE_DIR)/plfa.epub + + +# Clean generated files +.PHONY: epub-clean +epub-clean: + rm $(SITE_DIR)/plfa.epub diff --git a/src/plfa/epub.xml b/book/epub.xml similarity index 100% rename from src/plfa/epub.xml rename to book/epub.xml diff --git a/epub/rewrite-html-ul.lua b/book/lua/epub-clean-html.lua similarity index 100% rename from epub/rewrite-html-ul.lua rename to book/lua/epub-clean-html.lua diff --git a/epub/include-files.lua b/book/lua/include-files.lua similarity index 86% rename from epub/include-files.lua rename to book/lua/include-files.lua index 5d70c890..7d0c88a1 100644 --- a/epub/include-files.lua +++ b/book/lua/include-files.lua @@ -13,7 +13,7 @@ local List = require 'pandoc.List' --- Shift headings in block list by given number -function shift_headings(blocks, shift_by) +local function shift_headings(blocks, shift_by) if not shift_by then return blocks end @@ -30,7 +30,8 @@ end --- Filter function for code blocks function CodeBlock(cb) - -- ignore code blocks which are not of class "include". + + -- Ignore code blocks which are not of class "include". if not cb.classes:includes 'include' then return end @@ -40,21 +41,24 @@ function CodeBlock(cb) local shift_heading_level_by = tonumber(cb.attributes['shift-heading-level-by']) - local blocks = List:new() for line in cb.text:gmatch('[^\n]+') do if line:sub(1,2) ~= '//' then -- Read in the document at the file path specified by `line`. local fh = io.open(line) local document = pandoc.read(fh:read '*a', format) + fh:close() + -- Before shifting headings, add a title heading at the beginning of the chapter. - local heading = pandoc.Header(1, pandoc.Str(pandoc.utils.stringify(document.meta.title))) - document.blocks:insert(1, heading) + if document.meta.title then + local heading = pandoc.Header(1, pandoc.Str(pandoc.utils.stringify(document.meta.title))) + document.blocks:insert(1, heading) + end -- Shift all headings by the user-specified amount, which is 0 by default. local chapter = shift_headings(document.blocks, shift_heading_level_by) + -- Concatenate the chapter blocks (discarding the metadata) to the current document. blocks:extend(chapter) - fh:close() end end return blocks diff --git a/pdf/lua/typeset-codeblocks.lua b/book/lua/latex-render-codeblocks.lua similarity index 59% rename from pdf/lua/typeset-codeblocks.lua rename to book/lua/latex-render-codeblocks.lua index e67f8244..a10162dd 100644 --- a/pdf/lua/typeset-codeblocks.lua +++ b/book/lua/latex-render-codeblocks.lua @@ -1,4 +1,20 @@ -local function typeset_codeblock(cb) +local unchecked_files = {} + +local function is_checked() + -- Check if any of our input files is an unchecked file. + for _, input_file in pairs(PANDOC_STATE.input_files) do + if unchecked_files[input_file] then + if #PANDOC_STATE.input_files > 1 then + error("Cannot handle multiple unchecked input files.") + else + return false + end + end + end + return true +end + +local function render_codeblock(cb) -- If a code block has class Agda or its class is omitted, format it as... -- -- \begin{agda}\begin{code} .. \end{agda}\end{code} @@ -10,40 +26,22 @@ local function typeset_codeblock(cb) -- Any file which is not checked by Agda must have its code blocks typeset in the latter style. -- Specify these files via the UNCHECKED_FILES environment variable. if is_checked() then - if #(cb.classes) == 0 or cb.classes[1] == 'agda' then + if #cb.classes == 0 or cb.classes[1] == 'agda' then return pandoc.RawBlock('tex', '\\begin{agda}\n\\begin{code}\n' .. cb.text .. '\n\\end{code}\n\\end{agda}') end end return pandoc.RawBlock('tex', '\\begin{pre}\n' .. cb.text .. '\n\\end{pre}') end --- Set of unchecked files, where the names of unchecked files are stored in the table keys. -local UNCHECKED_FILES = nil - --- Return whether the current file is checked by Agda, given by the UNCHECKED_FILES environment variable. -function is_checked() - - -- Initialise the table. - if UNCHECKED_FILES == nil then - UNCHECKED_FILES = {} - for unchecked_file in string.gmatch(pandoc.system.environment().UNCHECKED_FILES, "([^ ]+)") do - UNCHECKED_FILES[unchecked_file] = true +local function get_unchecked_files(meta) + if meta['unchecked-files'] then + for unchecked_file in string.gmatch(pandoc.utils.stringify(meta['unchecked-files']), "([^ ]+)") do + unchecked_files[unchecked_file] = true end end - - -- Check if any of our input files is an unchecked file. - for _, input_file in pairs(PANDOC_STATE.input_files) do - if UNCHECKED_FILES[input_file] then - if #PANDOC_STATE.input_files > 1 then - error("Cannot handle multiple unchecked input files.") - else - return false - end - end - end - return true end return { - { CodeBlock = typeset_codeblock } + { Meta = get_unchecked_files }, + { CodeBlock = render_codeblock } } diff --git a/book/lua/remove-badges.lua b/book/lua/remove-badges.lua new file mode 100644 index 00000000..9d345261 --- /dev/null +++ b/book/lua/remove-badges.lua @@ -0,0 +1,22 @@ +local badge_url = nil + +local function remove_badges(ln) + -- Remove link elements if their first child is a badge. + if #ln.content > 0 and ln.content[1].t == "Image" then + if string.find(ln.content[1].src, badge_url, 1, true) then + return pandoc.Null() + end + end +end + +local function get_badge_url(meta) + if meta['badge-url'] then + badge_url = pandoc.utils.stringify(meta['badge-url']) + end +end + + +return { + { Meta = get_badge_url }, + { Link = remove_badges } +} diff --git a/epub/default-code-class.lua b/book/lua/set-default-code-class.lua similarity index 73% rename from epub/default-code-class.lua rename to book/lua/set-default-code-class.lua index adb4706e..5c1af173 100644 --- a/epub/default-code-class.lua +++ b/book/lua/set-default-code-class.lua @@ -8,19 +8,21 @@ local default_code_classes = {} -function add_default_code_class(el) +local function add_default_code_class(el) if #(el.classes) == 0 then el.classes = default_code_classes return el end end -function get_default_code_class(meta) +local function get_default_code_class(meta) if meta['default-code-class'] then default_code_classes = {pandoc.utils.stringify(meta['default-code-class'])} end end -return {{Meta = get_default_code_class}, - {Code = add_default_code_class}, - {CodeBlock = add_default_code_class}} +return { + {Meta = get_default_code_class}, + {Code = add_default_code_class}, + {CodeBlock = add_default_code_class} +} diff --git a/book/lua/single-file-headers.lua b/book/lua/single-file-headers.lua new file mode 100644 index 00000000..8a653686 --- /dev/null +++ b/book/lua/single-file-headers.lua @@ -0,0 +1,57 @@ +-- Performs the following transformations on Header identifiers: +-- +-- Case 1: +-- /title/: "Some Title" +-- /permalink/: /Title/ -> # Some Title {#Title} +-- +-- Case 2: +-- ## Subsection Title {name=more-stuff} -> ## Subsection Title {#Title-more-stuff} +-- + +local identifier = nil +local title = nil + +local function get_meta_info(meta) + + -- Get the title. + if meta['title'] then + title = meta['title'] + elseif meta['default-title'] then + title = meta['default-title'] + end + title = pandoc.utils.stringify(title) + + -- Get the identifier. + if meta['permalink'] then + identifier = meta['permalink'][1].c:match("^/(%w+)/$") + elseif meta['title'] then + identifier = meta['title'] + elseif meta['default-title'] then + identifier = meta['default-title'] + end + identifier = string.lower(pandoc.utils.stringify(identifier)) +end + +local function insert_title(doc) + -- Insert title in front of the blocks + if title then + header = pandoc.Header(1,title) + header.identifier = identifier + table.insert(doc.blocks,1,header) + end + return doc +end + +local function change_identifier(elem) + -- Change header identifier based on metadata + if elem.t == "Header" and elem.attributes.name then + elem.identifier = identifier .. "-" .. elem.attributes.name + end + return elem +end + +return { + {Meta = get_meta_info}, + {Header = change_identifier}, + {Pandoc = insert_title} +} diff --git a/pdf/lua/rewrite-links.lua b/book/lua/single-file-links.lua similarity index 100% rename from pdf/lua/rewrite-links.lua rename to book/lua/single-file-links.lua diff --git a/book/pdf.mk b/book/pdf.mk new file mode 100644 index 00000000..b984e52c --- /dev/null +++ b/book/pdf.mk @@ -0,0 +1,122 @@ +PDF_DIR := book +PDF_TEMPLATE_DIR := $(PDF_DIR)/templates +PDF_LUA_DIR := $(PDF_DIR)/lua +MD_DIR := src +LAGDA_TEX_DIR := $(TMP_DIR)/lagda_tex +TEX_DIR := $(TMP_DIR)/tex + +# Convert MD_DIR/%.lagda.md to LAGDA_TEX_DIR/%.lagda.tex +define LAGDA_TEX_PATH +$(patsubst $(MD_DIR)/%.lagda.md,$(LAGDA_TEX_DIR)/%.lagda.tex,$(1)) +endef + +# Convert MD_DIR/%.md to LAGDA_TEX_DIR/%.lagda.tex or TEX_DIR/%.tex +define TEX_PATH +$(patsubst $(PDF_DIR)/%,$(TEX_DIR)/%,\ + $(patsubst README.md,$(TEX_DIR)/plfa/frontmatter/README.tex,\ + $(patsubst $(MD_DIR)/%.md,$(TEX_DIR)/%.tex,\ + $(patsubst $(MD_DIR)/%.lagda.md,$(TEX_DIR)/%.tex,$(1))))) +endef + +# List source and intermediate files +PDF_LUA_SCRIPTS := $(wildcard $(PDF_LUA_DIR)/*.lua) +PDF_STATIC_FILES := book/pdf.tex book/DejaVu-mononoki-Symbola-Droid.ttf +MD_FILES := README.md $(wildcard $(MD_DIR)/plfa/**/*.md) +MD_FILES := $(filter-out %Fonts.lagda.md,$(MD_FILES)) +LAGDA_MD_FILES := $(filter %.lagda.md,$(MD_FILES)) +LAGDA_TEX_FILES := $(call LAGDA_TEX_PATH,$(LAGDA_MD_FILES)) +TEX_FILES := $(call TEX_PATH,$(MD_FILES) $(PDF_STATIC_FILES)) + + +# Compile PLFA to a PDF +.PHONY: pdf +pdf: $(SITE_DIR)/plfa.pdf + +$(SITE_DIR)/plfa.pdf: $(TEX_FILES) + @cd $(TEX_DIR) && latexmk -pdf -lualatex -use-make -halt-on-error pdf.tex + @cp $(TEX_DIR)/pdf.pdf $(SITE_DIR)/plfa.pdf + + +# Copy static files needed by PDF compilation +define MK_COPYSTATIC_RULE +src := $(1) +dst := $(2) +$$(dst): $$(src) + @echo "Copy $$< to $$@" + @mkdir -p '$$(@D)' + @cp $$< $$@ +endef + +# Compile Markdown files to LaTeX +# +# NOTE: Passing --indented-code-classes=default sets the class for /indented/ code blocks +# to 'default', which lets us distinguish them from /fenced/ code blocks without a +# class. That's important, since fenced code blocks are checked by Agda, but indented +# code blocks are /not/, so latex-render-codeblocks.lua needs to be able to tell the +# difference. +# +define MK_MD2TEX_RULE +src := $(1) +dst := $(2) +ttl := $(3) +$$(dst): $$(src) $(PDF_LUA_SCRIPTS) | setup-install-pandoc + @echo "Compile $$< to $$@" + @mkdir -p '$$(@D)' + @$(PANDOC) \ + --top-level-division=chapter \ + --indented-code-classes=default \ + --lua-filter=$(PDF_LUA_DIR)/remove-badges.lua -M badge-url=https://img.shields.io/badge/ \ + --lua-filter=$(PDF_LUA_DIR)/latex-render-codeblocks.lua -M unchecked-files=README.md \ + --lua-filter=$(PDF_LUA_DIR)/single-file-links.lua \ + --lua-filter=$(PDF_LUA_DIR)/single-file-headers.lua -M default-title=$$(ttl) \ + $$< -o $$@ +endef + +# Compile Literate Agda files to LaTeX +define MK_LAGDA_MD2TEX_RULE +src := $(1) +dst := $(2) +$$(dst): $$(src) $(LAGDA_TEX_FILES) | setup-install-agda setup-check-latexmk + @$(AGDA) --include-path=$(LAGDA_TEX_DIR) --latex --latex-dir=$(TEX_DIR) $$< +endef + + +# Copy static files (from PDF_DIR/% to TEX_DIR/%) +$(foreach static_file,\ + $(PDF_STATIC_FILES),\ + $(eval $(call MK_COPYSTATIC_RULE,\ + $(static_file),\ + $(call TEX_PATH,$(static_file))))) + +# Compile .md files (from MD_DIR/%.md to TEX_DIR/%.tex) +$(foreach md_file,\ + $(filter-out %acknowledgements.md %.lagda.md,$(MD_FILES)),\ + $(eval $(call MK_MD2TEX_RULE,\ + $(md_file),\ + $(call TEX_PATH,$(md_file))))) + +# Compile .lagda.md files (from MD_DIR/%.md to LAGDA_TEX_DIR/%.lagda.tex) +$(foreach lagda_md_file,\ + $(LAGDA_MD_FILES),\ + $(eval $(call MK_MD2TEX_RULE,\ + $(lagda_md_file),\ + $(call LAGDA_TEX_PATH,$(lagda_md_file))))) + +# Compile acknowledgements (from SITE_DIR/acknowledgements.md to TEX_DIR/acknowledgements.tex) +$(eval $(call MK_MD2TEX_RULE,\ + $(SITE_DIR)/acknowledgements.md,\ + $(TEX_DIR)/plfa/backmatter/acknowledgements.tex,\ + Acknowledgements)) + +# Compile .lagda.tex files (from LAGDA_TEX_DIR/%.lagda.tex to TEX_DIR/%.tex) +$(foreach lagda_md_file,\ + $(LAGDA_MD_FILES),\ + $(eval $(call MK_LAGDA_MD2TEX_RULE,\ + $(call LAGDA_TEX_PATH,$(lagda_md_file)),\ + $(call TEX_PATH,$(lagda_md_file))))) + + +# Clean generated files +.PHONY: pdf-clean +pdf-clean: + @rm -rf $(SITE_DIR)/plfa.pdf $(LAGDA_TEX_DIR) $(TEX_DIR) diff --git a/pdf/plfa.tex b/book/pdf.tex similarity index 99% rename from pdf/plfa.tex rename to book/pdf.tex index e21b9e39..b8508663 100644 --- a/pdf/plfa.tex +++ b/book/pdf.tex @@ -173,5 +173,4 @@ \input{plfa/part2/Substitution} \input{plfa/backmatter/acknowledgements} -\input{plfa/backmatter/Fonts} \end{document} diff --git a/css/epub.css b/css/epub.css deleted file mode 100644 index 1a8c1d0e..00000000 --- a/css/epub.css +++ /dev/null @@ -1,42 +0,0 @@ -/* This is Pandoc's default ebook CSS, modified slightly. */ -/* https://github.com/jgm/pandoc/blob/master/data/epub.css */ -@font-face { - font-family: 'mononoki'; - font-weight: normal; - font-style: normal; - src: url('../webfonts/mononoki.woff'); -} -@font-face { - font-family: 'FreeMono'; - font-weight: normal; - font-style: normal; - src: url('../webfonts/FreeMono.woff'); -} -@font-face { - font-family: 'DejaVuSansMono'; - font-weight: normal; - font-style: normal; - src: url('../webfonts/DejaVuSansMono.woff'); -} -body { margin: 5%; text-align: justify; font-size: medium; } -code { font-family: 'mononoki', 'FreeMono', 'DejaVuSansMono', monospace; } -h1, h2, h3, h4, h5, h6 { text-align: left; } -nav#toc ol, nav#landmarks ol { padding: 0; margin-left: 1em; } -nav#toc ol li, nav#landmarks ol li { list-style-type: none; margin: 0; padding: 0; } -a.footnote-ref { vertical-align: super; } -em, em em em, em em em em em { font-style: italic;} -em em, em em em em { font-style: normal; } -code{ white-space: pre-wrap; } -span.smallcaps{ font-variant: small-caps; } -span.underline{ text-decoration: underline; } -q { quotes: "“" "”" "‘" "’"; } -div.column{ display: inline-block; vertical-align: top; width: 50%; } -div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;} - -/* Workaround for iBooks issue; see #6242 */ -@media screen { - .sourceCode { - overflow: visible !important; - white-space: pre-wrap !important; - } -} diff --git a/epub/render-liquid-template.rb b/epub/render-liquid-template.rb deleted file mode 100644 index 927b25b5..00000000 --- a/epub/render-liquid-template.rb +++ /dev/null @@ -1,19 +0,0 @@ -#!/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) diff --git a/epub/rewrite-links.lua b/epub/rewrite-links.lua deleted file mode 100644 index 90e5008b..00000000 --- a/epub/rewrite-links.lua +++ /dev/null @@ -1,19 +0,0 @@ --- Performs the following transformations on Link targets: --- --- Case 1: --- [text](/chapter/#more-stuff) -> [text](#chapter-more-stuff) --- --- Case 2: --- [text](/chapter/) -> [text](#chapter) --- --- All other Links are ignored. -function Link (el) - local n - -- Case 1: - el.target, n = el.target:gsub("^/(%w+)/#([%w-]+)$", "#%1-%2") - -- Case 2: - if n == 0 then - el.target = el.target:gsub("^/(%w+)/$", "#%1") - end - return el -end diff --git a/hs/Hakyll/Web/Routes/Permalink.hs b/hs/Hakyll/Web/Routes/Permalink.hs index 6f36603f..0e060f6e 100644 --- a/hs/Hakyll/Web/Routes/Permalink.hs +++ b/hs/Hakyll/Web/Routes/Permalink.hs @@ -3,7 +3,6 @@ module Hakyll.Web.Routes.Permalink ( convertPermalink , permalinkRoute - , permalinkRouteWithDefault , stripIndexFile ) where @@ -19,11 +18,12 @@ convertPermalink :: FilePath -> FilePath convertPermalink link = fromMaybe link (stripPrefix "/" link) "index.html" permalinkRoute :: Routes -permalinkRoute = permalinkRouteWithDefault (error "Missing field 'permalink'.") - -permalinkRouteWithDefault :: Routes -> Routes -permalinkRouteWithDefault def = metadataRoute $ \metadata -> - maybe def (constRoute . convertPermalink) (lookupString "permalink" metadata) +permalinkRoute = metadataRoute $ \metadata -> + case lookupString "permalink" metadata of + Nothing -> + customRoute (\identifier -> error $ "missing field 'permalink' in metadata " <> toFilePath identifier) + Just permalink -> + constRoute (convertPermalink permalink) -- Removes "index.html" from URLs. stripIndexFile :: String -> String diff --git a/hs/Main.hs b/hs/Main.hs index 3274df47..4219e23c 100644 --- a/hs/Main.hs +++ b/hs/Main.hs @@ -1,7 +1,7 @@ +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE OverloadedStrings #-} import Control.Monad ((<=<), forM_) -import qualified Data.ByteString.Lazy as BL import Data.Functor ((<&>)) import qualified Data.Text as T import Hakyll @@ -16,7 +16,6 @@ import qualified Text.CSL as CSL import qualified Text.CSL.Pandoc as CSL (processCites) import Text.Pandoc (Pandoc(..), ReaderOptions(..), WriterOptions(..), Extension(..)) import qualified Text.Pandoc as Pandoc -import qualified Text.Pandoc.Filter as Pandoc (Filter(..), applyFilters) -------------------------------------------------------------------------------- -- Configuration @@ -124,29 +123,6 @@ sassOptions = defaultSassOptions { sassIncludePaths = Just ["css"] } -epubSectionContext :: Context String -epubSectionContext = mconcat - [ contentField "content" "content" - , titlerunningField - , subtitleField - ] - -epubReaderOptions :: ReaderOptions -epubReaderOptions = siteReaderOptions - { readerStandalone = True - , readerStripComments = True - } - -epubWriterOptions :: WriterOptions -epubWriterOptions = siteWriterOptions - { writerTableOfContents = True - , writerTOCDepth = 2 - , writerEpubFonts = [ "public/webfonts/DejaVuSansMono.woff" - , "public/webfonts/FreeMono.woff" - , "public/webfonts/mononoki.woff" - ] - , writerEpubChapterLevel = 2 - } -------------------------------------------------------------------------------- -- Build site @@ -198,40 +174,14 @@ main = do -- -- NOTE: The order of the various match expressions is important: -- Special-case compilation instructions for files such as - -- "src/plfa/epub.md" and "src/plfa/index.md" would be overwritten - -- by the general purpose compilers for "src/**.md", which would + -- "src/plfa/index.md" would be overwritten by the general + -- purpose compilers for "src/**.md", which would -- cause them to render incorrectly. It is possible to explicitly -- exclude such files using `complement` patterns, but this vastly -- complicates the match patterns. -- hakyll $ do - -- Compile EPUB - match "src/plfa/epub.md" $ do - route $ constRoute "plfa.epub" - compile $ do - epubTemplate <- load "templates/epub.html" - >>= compilePandocTemplate - epubMetadata <- load "src/plfa/epub.xml" - let ropt = epubReaderOptions - let wopt = epubWriterOptions - { writerTemplate = Just . itemBody $ epubTemplate - , writerEpubMetadata = Just . T.pack . itemBody $ epubMetadata - } - getResourceBody - >>= applyAsTemplate (tableOfContentsContext epubSectionContext) - >>= readPandocWith ropt - >>= applyPandocFilters ropt [] "epub3" - >>= writeEPUB3With wopt - - match "templates/epub.html" $ - compile $ getResourceBody - >>= applyAsTemplate siteContext - - match "src/plfa/epub.xml" $ - compile $ getResourceBody - >>= applyAsTemplate siteContext - -- Compile Table of Contents match "src/plfa/index.md" $ do route permalinkRoute @@ -253,15 +203,16 @@ main = do >>= applyAsTemplate acknowledgementsContext >>= readMarkdownWith siteReaderOptions <&> writeHTML5With siteWriterOptions - >>= saveSnapshot "content" >>= loadAndApplyTemplate "templates/page.html" siteContext >>= loadAndApplyTemplate "templates/default.html" siteContext >>= prettifyUrls - match "src/plfa/backmatter/acknowledgements.md" $ version "raw" $ do - route $ constRoute "acknowledgements.md" + match "src/plfa/backmatter/acknowledgements.md" $ version "native" $ do + route $ constRoute "versions/native/acknowledgements.native" compile $ getResourceBody >>= applyAsTemplate acknowledgementsContext + >>= readMarkdownWith siteReaderOptions + <&> writeNativeWith siteWriterOptions match "authors/*.metadata" $ compile getResourceBody @@ -298,7 +249,7 @@ main = do compile $ pageWithAgdaCompiler agdaOptions -- Compile other sections and pages - match ("README.md" .||. "src/**.md" .&&. complement "src/plfa/epub.md") $ do + match ("README.md" .||. "src/**.md") $ do route permalinkRoute compile pageCompiler @@ -349,7 +300,7 @@ main = do create ["public/css/style.css"] $ do route idRoute compile $ do - csses <- loadAll ("css/*.css" .||. "css/*.scss" .&&. complement "css/epub.css") + csses <- loadAll ("css/*.css" .||. "css/*.scss") makeItem $ unlines $ map itemBody csses -- Copy versions @@ -395,7 +346,7 @@ processCites csl bib item = do withItemBody (return . CSL.processCites style refs) item -- | Write a document as HTML using Pandoc, with the supplied options. -writeHTML5With :: WriterOptions -- ^ Writer options for pandoc +writeHTML5With :: WriterOptions -- ^ Writer options for Pandoc -> Item Pandoc -- ^ Document to write -> Item String -- ^ Resulting HTML writeHTML5With wopt (Item itemi doc) = @@ -403,26 +354,14 @@ writeHTML5With wopt (Item itemi doc) = Left err -> error $ "Hakyll.Web.Pandoc.writePandocWith: " ++ show err Right item' -> Item itemi $ T.unpack item' --- | Write a document as EPUB3 using Pandoc, with the supplied options. -writeEPUB3With :: WriterOptions -> Item Pandoc -> Compiler (Item BL.ByteString) -writeEPUB3With wopt (Item itemi doc) = - return $ case Pandoc.runPure $ Pandoc.writeEPUB3 wopt doc of - Left err -> error $ "Hakyll.Web.Pandoc.writeEPUB3With: " ++ show err - Right doc' -> Item itemi doc' - --- | Apply a filter to a Pandoc document. -applyPandocFilters :: ReaderOptions -> [Pandoc.Filter] -> String -> Item Pandoc -> Compiler (Item Pandoc) -applyPandocFilters ropt filters fmt = withItemBody $ - unsafeCompiler . Pandoc.runIOorExplode . Pandoc.applyFilters ropt filters [fmt] - --- | Compile a Pandoc template (as opposed to a Hakyll template). -compilePandocTemplate :: Item String -> Compiler (Item (Pandoc.Template T.Text)) -compilePandocTemplate i = do - let templatePath = toFilePath $ itemIdentifier i - let templateBody = T.pack $ itemBody i - templateOrError <- unsafeCompiler $ Pandoc.compileTemplate templatePath templateBody - template <- either fail return templateOrError - makeItem template +-- | Write a document as HTML using Pandoc, with the supplied options. +writeNativeWith :: WriterOptions -- ^ Writer options for Pandoc + -> Item Pandoc -- ^ Document to write + -> Item String -- ^ Resulting Markdown +writeNativeWith wopt (Item itemi doc) = + case Pandoc.runPure $ Pandoc.writeNative wopt doc of + Left err -> error $ "Hakyll.Web.Pandoc.writeNativeWith: " ++ show err + Right item' -> Item itemi $ T.unpack item' -------------------------------------------------------------------------------- diff --git a/pdf/lua/remove-badges.lua b/pdf/lua/remove-badges.lua deleted file mode 100644 index 69230ff0..00000000 --- a/pdf/lua/remove-badges.lua +++ /dev/null @@ -1,12 +0,0 @@ -function remove_badges(ln) - -- Remove link elements if their first child is a badge. - if #ln.content > 0 and ln.content[1].t == "Image" then - if string.match(ln.content[1].src, 'https://img%.shields%.io/badge/') then - return pandoc.Null() - end - end -end - -return { - { Link = remove_badges } -} diff --git a/pdf/lua/single-file-headers-ids.lua b/pdf/lua/single-file-headers-ids.lua deleted file mode 100644 index c5d09443..00000000 --- a/pdf/lua/single-file-headers-ids.lua +++ /dev/null @@ -1,50 +0,0 @@ --- Performs the following transformations on Header identifiers: --- --- Case 1: --- /title/: "Some Title" --- /permalink/: /Title/ -> # Some Title {#Title} --- --- Case 2: --- ## Subsection Title {name=more-stuff} -> ## Subsection Title {#Title-more-stuff} --- - -local identifier = nil -local title = nil - -function get_identifier(meta) - -- get title identifier from permalinks - for k,v in pairs(meta) do - if k == "title" then - title = {table.unpack(v)} - end - if k == "permalink" then - -- set lower case permalink as identifier - identifier = v[1].c:match("^/(%w+)/$") - end - end -end - -function insert_title(doc) - -- insert title in front of the blocks - if title then - header = pandoc.Header(1,title) - header.identifier = identifier - table.insert(doc.blocks,1,header) - end - return doc -end - -function change_identifier(elem) - -- change header identifier based on metadata - local name = elem.attributes["name"] - if elem.t == "Header" and name then - elem.identifier = identifier .. "-" .. name - end - return elem -end - -return { - {Meta = get_identifier}, - {Header = change_identifier}, - {Pandoc = insert_title} -} diff --git a/pdf/templates/acknowledgements.latex b/pdf/templates/acknowledgements.latex deleted file mode 100644 index eea01198..00000000 --- a/pdf/templates/acknowledgements.latex +++ /dev/null @@ -1,4 +0,0 @@ -\chapter{Acknowledgements} -$body$ - - diff --git a/pdf/templates/chapter.latex b/pdf/templates/chapter.latex deleted file mode 100644 index dc7dfa72..00000000 --- a/pdf/templates/chapter.latex +++ /dev/null @@ -1,3 +0,0 @@ -$body$ - - diff --git a/src/plfa/epub.md b/src/plfa/epub.md deleted file mode 100644 index fef0519c..00000000 --- a/src/plfa/epub.md +++ /dev/null @@ -1,7 +0,0 @@ -$for(parts)$ -# $title$ -$for(sections)$ -$content$ -$endfor$ -$endfor$ - diff --git a/templates/epub.html b/templates/epub.html deleted file mode 100644 index 4ee72389..00000000 --- a/templates/epub.html +++ /dev/null @@ -1,26 +0,0 @@ - - - - - - $pagetitle$ - - - - -
-

$pagetitle$

-$for(authors)$ -

$name$

-$endfor$ -$if(rights)$ -
$rights$
- $endif$ -
- - - -$$body$$ - - -