Fixed PDF and EPUB generation to use toc.metadata.

This commit is contained in:
Wen Kokke 2021-08-24 19:22:53 +01:00
parent e8df980d4b
commit b4ae07e13c
No known key found for this signature in database
GPG key ID: 7EB7DBBCEB539DB8
9 changed files with 239 additions and 194 deletions

View file

@ -12,6 +12,25 @@ AGDA := stack exec agda -- --no-libraries --include-path=standard-library/s
PANDOC := stack exec pandoc --
#################################################################################
# Build PLFA site, EPUB, and PDF
#################################################################################
.PHONY: all
all:
@echo "Building site..."
make build
@echo "Testing site..."
make test
@echo "Building epub..."
make epub-build
@echo "Testing epub..."
make epub-test
@echo "Building pdf..."
make pdf-build
@echo "Testing pdf..."
#################################################################################
# Setup Git Hooks
#################################################################################
@ -165,7 +184,7 @@ include book/pdf.mk
#################################################################################
# Setup dependencies
# Setup or check dependencies
#################################################################################
.PHONY: setup-check-stack
@ -209,13 +228,6 @@ ifeq (,$(wildcard $(shell which latexmk)))
@echo "See: https://mg.readthedocs.io/latexmk.html"
endif
.PHONY: setup-check-epubcheck
setup-check-epubcheck:
ifeq (,$(wildcard $(shell which epubcheck)))
@echo "The command you called requires EPUBCheck"
@echo "See: https://github.com/w3c/epubcheck"
endif
.PHONY: setup-check-rsync
setup-check-rsync:
ifeq (,$(wildcard $(shell which rsync)))

View file

@ -1,71 +1,7 @@
---
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/raw/plfa/backmatter/acknowledgements.md
src/plfa/backmatter/Fonts.lagda.md
```
$for(parts)$
# $title$
$for(sections)$
## $title$ {#$anchor$}
$body$
$endfor$
$endfor$

View file

@ -1,24 +1,36 @@
#################################################################################
# Configuration
#################################################################################
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)
FRANKENFONT := public/webfonts/DejaVu-mononoki-Symbola-Droid.woff
# Compile PLFA to an EPUB
#################################################################################
# Compile PLFA to an EPUB using Pandoc
#################################################################################
.PHONY: epub-build
epub-build: $(SITE_DIR)/plfa.epub
$(SITE_DIR)/plfa.epub: book/epub.md book/epub.css $(MD_FILES) $(EPUB_LUA_SCRIPTS) | setup-install-pandoc
$(SITE_DIR)/plfa.epub: \
$(EPUB_DIR)/epub.md $(EPUB_DIR)/epub.css $(RAW_DIR)/epub.xml $(FRANKENFONT) \
$(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 \
--css=$(EPUB_DIR)/epub.css \
--epub-embed-font=$(FRANKENFONT) \
--epub-metadata=$(RAW_DIR)/epub.xml
--indented-code-class=default \
--lua-filter=$(EPUB_LUA_DIR)/set-default-code-class.lua -M default-code-class=agda \
--lua-filter=$(EPUB_LUA_DIR)/remove-badges.lua -M badge-url=https://img.shields.io/badge/ \
--lua-filter=$(EPUB_LUA_DIR)/epub-clean-html.lua \
--lua-filter=$(EPUB_LUA_DIR)/single-file-links.lua \
--standalone \
--fail-if-warnings \
--toc --toc-depth=2 \
@ -26,13 +38,39 @@ $(SITE_DIR)/plfa.epub: book/epub.md book/epub.css $(MD_FILES) $(EPUB_LUA_SCRIPTS
$< -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
#################################################################################
# Tasks for files that are generated by Hakyll
#################################################################################
$(RAW_DIR)/epub.xml: $(EPUB_DIR)/epub.xml
make build
#################################################################################
# Clean up and remove generated EPUB
#################################################################################
.PHONY: epub-clean
epub-clean:
rm $(SITE_DIR)/plfa.epub
rm -f $(SITE_DIR)/plfa.epub
#################################################################################
# Setup or check dependencies
#################################################################################
.PHONY: setup-check-epubcheck
setup-check-epubcheck:
ifeq (,$(wildcard $(shell which epubcheck)))
@echo "The command you called requires EPUBCheck"
@echo "See: https://github.com/w3c/epubcheck"
endif

View file

@ -12,22 +12,6 @@
-- pandoc's List type
local List = require 'pandoc.List'
--- Shift headings in block list by given number
local function shift_headings(blocks, shift_by)
if not shift_by then
return blocks
end
local shift_headings_filter = {
Header = function (header)
header.level = header.level + shift_by
return header
end
}
return pandoc.walk_block(pandoc.Div(blocks), shift_headings_filter).content
end
--- Filter function for code blocks
function CodeBlock(cb)
@ -46,20 +30,22 @@ function CodeBlock(cb)
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)
local doc = pandoc.read(fh:read '*a', format)
blocks:extend(document.blocks)
fh:close()
-- Before shifting headings, add a title heading at the beginning of the chapter.
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)
end
end
return blocks
end
-- Apply a filter to a document.
function apply_filter(doc, filters)
div = pandoc.Div(doc.blocks)
for _, filter in pairs(filters) do
if filter.Meta then
filter.Meta(doc.meta)
end
div = pandoc.walk_block(div, filter)
end
return pandoc.Pandoc(div.content, doc.meta)
end

View file

@ -1,3 +1,7 @@
#################################################################################
# Configuration
#################################################################################
PDF_DIR := book
PDF_TEMPLATE_DIR := $(PDF_DIR)/templates
PDF_LUA_DIR := $(PDF_DIR)/lua
@ -5,6 +9,11 @@ MD_DIR := src
LAGDA_TEX_DIR := $(TMP_DIR)/lagda_tex
TEX_DIR := $(TMP_DIR)/tex
#################################################################################
# Helper functions for translating paths
#################################################################################
# Convert MD_DIR/%.md to its modified source path
define MD_PATH
$(patsubst $(MD_DIR)/%/acknowledgements.md,$(RAW_DIR)/%/acknowledgements.md,\
@ -28,7 +37,11 @@ $(patsubst $(RAW_DIR)/%,$(TEX_DIR)/%,\
$(patsubst $(MD_DIR)/%.lagda.md,$(TEX_DIR)/%.tex,$(1))))))
endef
# List source and intermediate files
#################################################################################
# Lists of source and intermediate files
#################################################################################
PDF_LUA_SCRIPTS := $(wildcard $(PDF_LUA_DIR)/*.lua)
PDF_STATIC_FILES := $(PDF_DIR)/pdf.tex $(PDF_DIR)/DejaVu-mononoki-Symbola-Droid.ttf
MD_FILES := README.md $(wildcard $(MD_DIR)/plfa/**/*.md)
@ -37,16 +50,10 @@ LAGDA_TEX_FILES := $(call LAGDA_TEX_PATH,$(LAGDA_MD_FILES))
TEX_FILES := $(call TEX_PATH,$(MD_FILES) $(RAW_DIR)/pdf.tex $(PDF_STATIC_FILES))
# Generated by Hakyll
$(RAW_DIR)/pdf.tex: $(PDF_DIR)/pdf.tex $(MD_DIR)/plfa/toc.metadata
make build
#################################################################################
# Compile PLFA to a PDF via Pandoc and Latexmk
#################################################################################
# Generated by Hakyll
$(RAW_DIR)/plfa/backmatter/acknowledgements.md: $(MD_DIR)/plfa/backmatter/acknowledgements.md
make build
# Compile PLFA to a PDF
.PHONY: pdf-build
pdf-build: $(SITE_DIR)/plfa.pdf
@ -55,6 +62,10 @@ $(SITE_DIR)/plfa.pdf: $(TEX_FILES)
@cp $(TEX_DIR)/pdf.pdf $(SITE_DIR)/plfa.pdf
#################################################################################
# Definitions of various compilation tasks
#################################################################################
# Copy static files needed by PDF compilation
define MK_COPYSTATIC_RULE
src := $(1)
@ -65,6 +76,14 @@ $$(dst): $$(src)
@cp $$< $$@
endef
# Copy static files from PDF_DIR/% to TEX_DIR/%
$(foreach static_file,\
$(PDF_STATIC_FILES),\
$(eval $(call MK_COPYSTATIC_RULE,\
$(call MD_PATH,$(static_file)),\
$(call TEX_PATH,$(static_file)))))
# Compile Markdown files to LaTeX
#
# NOTE: Passing --indented-code-classes=default sets the class for /indented/ code blocks
@ -85,26 +104,9 @@ $$(dst): $$(src) $(PDF_LUA_SCRIPTS) | setup-install-pandoc
--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 \
$$< -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,\
$(call MD_PATH,$(static_file)),\
$(call TEX_PATH,$(static_file)))))
# Compile .md files (from MD_DIR/%.md to TEX_DIR/%.tex)
$(foreach md_file,\
$(filter-out %.lagda.md,$(MD_FILES)),\
@ -119,6 +121,15 @@ $(foreach lagda_md_file,\
$(lagda_md_file),\
$(call LAGDA_TEX_PATH,$(lagda_md_file)))))
# 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
# Compile .lagda.tex files (from LAGDA_TEX_DIR/%.lagda.tex to TEX_DIR/%.tex)
$(foreach lagda_md_file,\
$(LAGDA_MD_FILES),\
@ -127,7 +138,23 @@ $(foreach lagda_md_file,\
$(call TEX_PATH,$(lagda_md_file)))))
# Clean generated files
#################################################################################
# Tasks for files that are generated by Hakyll
#################################################################################
$(RAW_DIR)/pdf.tex: $(PDF_DIR)/pdf.tex $(MD_DIR)/plfa/toc.metadata
make build
# Generated by Hakyll
$(RAW_DIR)/plfa/backmatter/acknowledgements.md: $(MD_DIR)/plfa/backmatter/acknowledgements.md
make build
#################################################################################
# Clean up and remove generated PDF
#################################################################################
.PHONY: pdf-clean
pdf-clean:
@rm -rf $(SITE_DIR)/plfa.pdf $(LAGDA_TEX_DIR) $(TEX_DIR)

View file

@ -7,12 +7,20 @@
\setsansfont{DejaVu Sans}
\setmonofont{[DejaVu-mononoki-Symbola-Droid.ttf]}
\usepackage{soul}
\usepackage[most]{tcolorbox}
\usepackage{tcolorbox}
\tcbuselibrary{skins,breakable}
\usepackage{listings}
\usepackage{fancyvrb}
\usepackage{xcolor}
\usepackage{tikz}
\usepackage{setspace}
\usepackage{geometry}
\geometry{
a4paper,
total={170mm,257mm},
left=20mm,
top=20mm,
}
% Wrap texttt lines
\sloppy
@ -20,48 +28,37 @@
% Disable section numbering
\setcounter{secnumdepth}{0}
% Set the global text color:
\definecolor{textcolor}{111111}
\color{textcolor}
% Change background color for inline code in markdown files.
% The following code does not work well for long text as the
% text will exceed the page boundary.
\definecolor{bgcolor}{HTML}{EEEEFF}
\definecolor{background-color}{HTML}{EEEEFF}
\let\oldtexttt\texttt%
\renewcommand{\texttt}[1]{\colorbox{bgcolor}{\oldtexttt{#1}}}
% Indent verbatim to be the same as agda code blocks.
\lstdefinestyle{codeBlockStyle}{
basicstyle=\ttfamily,
numbers=none
}
% Box with background colour similar to web version:
\newtcolorbox{agda}[1][]{
frame hidden,
colback=bgcolor,
colback=background-color,
spartan,
left=5pt,
boxrule=0pt,
breakable,
}
\newtcblisting{pre}{
frame hidden,
colback=bgcolor,
spartan,
width=\textwidth,
listing only,
listing options={style=codeBlockStyle},
arc=0mm,
top=0mm,
bottom=0mm,
left=0mm,
right=0mm,
boxrule=0pt,
breakable,
}
\usepackage{geometry}
\geometry{
a4paper,
total={170mm,257mm},
left=20mm,
top=20mm,
% Verbatim environment similarly indented to Agda code blocks.
\DefineVerbatimEnvironment{verbatim}{Verbatim}{xleftmargin=0pt}%
% Adding backgrounds to verbatim environments.
\newenvironment{pre}{
\VerbatimEnvironment
\begin{agda}
\begin{verbatim}
}{\end{verbatim}
\end{agda}
}
% Use special font families without TeX ligatures for Agda code.
@ -78,7 +75,6 @@
\AgdaNoSpaceAroundCode{}
% Adjust spacing after toc numbering
\usepackage{tocloft}
\setlength\cftchapnumwidth{3em}
@ -86,11 +82,12 @@
% Style links with colors instead of boxes:
% https://tex.stackexchange.com/q/823
\definecolor{linkcolor}{HTML}{2A7AE2}
\hypersetup{
colorlinks,
linkcolor={red!50!black},
citecolor={blue!50!black},
urlcolor={blue!80!black}
linkcolor={linkcolor},
citecolor={linkcolor},
urlcolor={linkcolor}
}
\begin{document}
@ -150,6 +147,8 @@ $endif$
% Include each section.
$for(sections)$
\hypertarget{$anchor$}{%
\chapter{$title$}\label{$anchor$}}
\input{$tex_path$}
$endfor$

View file

@ -2,9 +2,12 @@
{-# LANGUAGE OverloadedStrings #-}
import Control.Monad ((<=<), forM_)
import qualified Data.ByteString.Char8 as BS
import Data.Char (toLower)
import Data.Functor ((<&>))
import Data.List (isPrefixOf)
import Data.List (isPrefixOf, stripPrefix)
import qualified Data.Text as T
import qualified Data.Yaml as Y
import Hakyll
import Hakyll.Web.Agda
import Hakyll.Web.Routes.Permalink
@ -18,6 +21,9 @@ 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 Text.Pandoc.Definition (Block(..))
import Text.Pandoc.Walk (walk)
import Text.Printf
--------------------------------------------------------------------------------
-- Configuration
@ -66,7 +72,7 @@ siteContext = mconcat
, "authors/jsiek.metadata"
]
, constField "google_analytics" "UA-125055580-1"
, defaultContext
, addAnchor defaultContext
]
siteSectionContext :: Context String
@ -77,10 +83,10 @@ siteSectionContext = mconcat
]
tableOfContentsContext :: Context String -> Context String
tableOfContentsContext ctx = Context $ \k a _ -> do
metadata <- getMetadata "src/plfa/toc.metadata"
m <- makeItem metadata
unContext (objectContext ctx) k a m
tableOfContentsContext ctx = Context $ \k a _ ->
unContext (objectContext ctx) k a
=<< makeItem
=<< getMetadata "src/plfa/toc.metadata"
acknowledgementsContext :: Context String
acknowledgementsContext = mconcat
@ -152,6 +158,41 @@ addTexPath = addDerivedField "tex_path" deriveTexPath
dropTopDirectory :: FilePath -> FilePath
dropTopDirectory = joinPath . tail . splitPath
-- Add an anchor based on the permalink, to be used as the header id.
addAnchor :: Context a -> Context a
addAnchor = addDerivedField "anchor" deriveAnchor
where
deriveAnchor :: Context a -> [String] -> Item a -> Compiler ContextField
deriveAnchor ctx a i = do
fld <- unContext ctx "permalink" a i
case fld of
StringField permalink -> StringField <$> anchor permalink
_ -> fail "Key 'permalink' does not return a String"
anchor :: String -> Compiler String
anchor permalink =
let maybeAnchor = map toLower <$> (stripSuffix "/" <=< stripPrefix "/") permalink
in maybe (fail $ printf "Key 'permalink' malformed '%s'" permalink) return maybeAnchor
stripSuffix :: String -> String -> Maybe String
stripSuffix suf str = reverse <$> stripPrefix (reverse suf) (reverse str)
-- Add the metadata back to the file as a Yaml header.
addMetadata :: Item String -> Compiler (Item String)
addMetadata item = do
metadata <- getMetadata (itemIdentifier item)
let yaml = "---\n" <> BS.unpack (Y.encode metadata) <> "---\n\n"
withItemBody (\body -> return (yaml <> body)) item
-- Shift all headers by a given value.
shiftHeadersBy :: Int -> Pandoc -> Pandoc
shiftHeadersBy n = walk shiftHeader
where
shiftHeader :: Block -> Block
shiftHeader (Header level attr inlines) = Header (level + n) attr inlines
shiftHeader block = block
--------------------------------------------------------------------------------
-- Build site
@ -241,7 +282,7 @@ main = do
route $ gsubRoute "src/" (const "raw/")
compile $ getResourceBody
>>= applyAsTemplate acknowledgementsContext
>>= loadAndApplyTemplate "templates/metadata.md" siteContext
>>= addMetadata
-- Compile raw version of index used in constructing the PDF
match "book/pdf.tex" $ do
@ -249,6 +290,12 @@ main = do
compile $ getResourceBody
>>= applyAsTemplate (addTexPath (tableOfContentsContext siteSectionContext))
-- Compile raw version of index used in constructing the EPUB
match "book/epub.md" $ do
route $ gsubRoute "book/" (const "raw/")
compile $ getResourceBody
>>= applyAsTemplate (tableOfContentsContext siteSectionContext)
-- Compile metadata XML used in constructing the EPUB
match "book/epub.xml" $ version "raw" $ do
route $ constRoute "raw/epub.xml"

View file

@ -12,19 +12,19 @@ build-type: Simple
common shared-properties
ghc-options: -Wall
default-language: Haskell2010
build-depends: aeson >=1.4 && <1.5
build-depends: aeson >=1.4 && <1.6
, base >=4.6 && <5
, bytestring >=0.10 && <0.11
, containers >=0.6 && <0.7
, directory >=1.2 && <1.4
, doctemplates >=0.8 && <0.9
, doctemplates >=0.8 && <1.0
, extra >=1.7 && <1.8
, filemanip >=0.3 && <0.4
, filepath >=1.3 && <1.5
, frontmatter >=0.1 && <0.2
, hakyll >=4.10 && <4.15
, pandoc >=2.1 && <2.11
, pandoc-types >=1.20 && <1.21
, pandoc-types >=1.20 && <1.23
, pandoc-citeproc >=0.17 && <0.18
, text >=1.2 && <1.3
, unordered-containers >=0.2 && <0.3

View file

@ -1,7 +1,7 @@
<article class="post">
$partial("templates/next.html")$
<header class="post-header">
<h1 class="post-title">$title$</h1>
<h1 class="post-title" $if(anchor)$id="$anchor$"$endif$>$title$</h1>
</header>
<div class="post-content">
$body$