1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
|
#!/usr/bin/env nix-shell
#!nix-shell -i bash -p pandoc epubcheck "python3.withPackages(ps: [ ps.beautifulsoup4 ps.lxml ])"
#
# Regenerate forge-paper.epub from paper.html.
#
# Run this by hand after any edit to paper.html or images/, and commit the
# result. The EPUB is a committed artifact derived from another committed
# artifact, and nothing checks that the two agree -- see the CAVEATS section
# of forge-paper.7.
#
# Unlike the PDF -> HTML converter (a one-off pipeline that is not in this
# repository), this step is deterministic and cheap, so it lives here rather
# than being described in prose.
#
# Usage: ./make-epub from the directory containing paper.html
set -euo pipefail
cd "$(dirname "$0")"
src=paper.html
out=forge-paper.epub
work=$(mktemp -d)
trap 'rm -rf "$work"' EXIT
test -f "$src" || { echo "make-epub: no $src here" >&2; exit 1; }
# ---------------------------------------------------------------------------
# 1. Preprocess.
#
# Strip the parts of the page that only make sense in a browser. Everything
# removed here is either interactive (and dead in an EPUB) or duplicated by
# the reading system.
# ---------------------------------------------------------------------------
python3 - "$src" "$work/clean.html" <<'PY'
import os, struct, sys
from bs4 import BeautifulSoup
src, dst = sys.argv[1], sys.argv[2]
soup = BeautifulSoup(open(src, encoding="utf-8").read(), "html.parser")
def drop(sel):
n = 0
for el in soup.select(sel):
el.decompose()
n += 1
return n
report = {}
# The click-to-enlarge lightbox. Without this, pandoc turns the dialog's
# "Close x" button into a stray paragraph at the end of the book and its 1x1
# transparent placeholder GIF into a stray image.
report["dialog.lightbox (removed)"] = drop("dialog.lightbox")
# The script that drives it.
report["script (removed)"] = drop("script")
# The in-page table of contents. EPUB has a mandatory navigation document,
# and the reading system offers it through its own UI; keeping this one would
# show the reader two tables of contents.
report["nav.toc (removed)"] = drop("nav.toc")
# The page stylesheet: it is built for a browser (floats, dialog,
# prefers-device-scheme, a fixed measure). epub.css replaces it.
report["style (removed)"] = drop("style")
# The affiliation follows the author's name with no separator in the markup;
# on the web a CSS margin makes the gap. A reading system with the publisher
# stylesheet disabled -- which is a button on most of them, and the default
# on some -- renders "Tim NelsonBrown University, USA". Put a real separator
# in the text so the meaning does not depend on the stylesheet surviving.
affs = 0
for aff in soup.select("ol.authors .aff"):
aff.insert_before(" — ")
affs += 1
report[".aff (separator inserted)"] = affs
# Anything paper.html marks as web-only. Currently that is the sentence
# offering the EPUB download, which inside the EPUB would point at a file
# that is not there and describe the file being read. Marking it in the HTML
# rather than matching its wording here means the two cannot drift apart.
report["[data-web-only] (removed)"] = drop("[data-web-only]")
# Browser-only attributes that epubcheck flags as unknown in XHTML.
lazy = 0
for img in soup.select("img[loading]"):
del img["loading"]
lazy += 1
report["img[loading] (attr removed)"] = lazy
# The zoom buttons are unwrapped rather than dropped: the <img> inside each
# one must survive. pandoc already discards <button> and keeps its children,
# but doing it here keeps the intermediate file honest and lets the count be
# checked.
buttons = 0
for btn in soup.select("button.zoom"):
btn.unwrap()
buttons += 1
report["button.zoom (unwrapped)"] = buttons
# role="doc-noteref" makes pandoc's HTML reader intercept the anchor as a
# footnote reference. It then looks for a *pandoc* footnote called "fn1",
# does not find one (the note here is an ordinary inline <span>), warns
# "Reference not found for 'fn1'", and emits an empty Note. The result is
# that both the mark and its id vanish, pandoc synthesises its own empty
# footnote section carrying a second id="fn1", and the file has duplicate
# ids and a footnote with no text.
#
# Dropping the attribute makes the anchor an ordinary link again, which is
# what this markup actually is: the note is inline, next to its mark, and is
# meant to stay there. role="doc-biblioref" on the citation links is
# harmless and stays.
norefs = 0
for a in soup.select('a[role="doc-noteref"]'):
del a["role"]
norefs += 1
report['a[role=doc-noteref] (role dropped)'] = norefs
# pandoc wraps each heading in an implicit <section> whose id is derived
# from the heading text. The <h1> inside <header class="paper-head"> repeats
# the document title, so its generated id collides with the one pandoc gives
# the first split document, and epubcheck rejects the duplicate. Naming the
# heading explicitly takes the slug out of pandoc's hands.
h1 = soup.select_one("header.paper-head h1")
if h1 is not None:
h1["id"] = "paper-title"
report["h1 (id pinned)"] = 1
# pandoc only recognises the document's own title heading if it is at the
# top level of <body>. Nested inside <header>, or preceded by any other
# content, it is treated as ordinary text and pandoc synthesises a title
# heading of its own from the metadata -- so the book opens with the
# title printed twice, under two colliding ids.
#
# So: hoist the <h1> to the front of <body>, and unwrap the <header>
# around it. On the web the provenance banner comes before the title;
# here it follows it, which keeps it on the same opening screen and just
# as unmissable, at the cost of one line of reading order.
header = soup.select_one("header.paper-head")
body = soup.body or soup
body.insert(0, h1.extract())
header.unwrap()
report["header.paper-head (h1 hoisted, header unwrapped)"] = 1
# Bold runs inside displayed listings mark Forge keywords. pandoc's AST holds
# a code block as a *plain string* -- CodeBlock ("",[],[]) "sig Board {..." --
# so it cannot represent markup inside one, and every <b> is silently
# discarded. There is no flag for this; the node has nowhere to put them.
#
# The extraction went to real trouble to capture these runs in the first
# place (the -wbt 40 pass exists partly for them; see forge-paper.7), so
# losing them here would undo that work. Instead, bracket each run with a
# sentinel: the *text* of a code block passes through pandoc byte for byte,
# so the marks survive and the relinking pass below turns them back into
# <b> elements.
#
# The sentinels are Unicode private-use characters rather than ASCII markers
# because they cannot occur in Forge source, in the paper's prose, or in
# anything pandoc might escape. Neither appears in paper.html.
BOLD_ON, BOLD_OFF = "\ue000", "\ue001"
keywords = 0
for block in soup.select("pre code"):
for b in block.find_all(["b", "strong"]):
b.insert_before(BOLD_ON)
b.insert_after(BOLD_OFF)
b.unwrap()
keywords += 1
report["pre code b (marked for restore)"] = keywords
# Reading systems need to be told how wide an image wants to be. Without a
# width some stretch every image to the measure, which turns the 269px
# screenshots into mush; with width:100% they all do. The natural size lives
# in the PNG header (IHDR, big-endian, bytes 16..24 of the file), so read it
# from there rather than adding an image library for two integers. epub.css
# caps this with max-width:100% for screens narrower than the image.
sized = 0
for img in soup.select("img[src]"):
src = img["src"]
if not src.startswith("images/"):
continue
with open(src, "rb") as fh: # cwd is the directory holding paper.html
head = fh.read(24)
if head[:8] != b"\x89PNG\r\n\x1a\n" or head[12:16] != b"IHDR":
continue
width = struct.unpack(">I", head[16:20])[0]
img["style"] = f"width: {width}px;"
sized += 1
report["img (natural width set)"] = sized
open(dst, "w", encoding="utf-8").write(str(soup))
for k, v in report.items():
print(f" {v:>3} {k}", file=sys.stderr)
PY
# ---------------------------------------------------------------------------
# 2. Convert.
#
# --split-level=2 one document per <h2>: the header, the abstract, the
# nine numbered sections, and the references. A single
# 144K document makes some readers slow to page and
# renders their position indicator useless.
# --toc-depth=3 subsections reach the navigation document, restoring
# the detail the dropped in-page TOC used to give.
# --epub-title-page off: pandoc would generate a title page from the
# metadata, duplicating the real <header class="paper-head">
# and losing the fifteen author affiliations.
# ---------------------------------------------------------------------------
pandoc "$work/clean.html" \
--from=html \
--to=epub3 \
--output="$out" \
--epub-metadata=epub-metadata.xml \
--css=epub.css \
--split-level=2 \
--toc-depth=3 \
--epub-title-page=false \
--resource-path=.
# ---------------------------------------------------------------------------
# 3. Repair cross-document links.
#
# When pandoc splits a document it rewrites "#foo" to "chNNN.xhtml#foo" only
# for ids it owns, i.e. those attached to *headings*. Every other id in the
# source -- <figure id="fig1">, <table id="tab1">, <li id="ref12"> -- is left
# as a bare fragment, which after the split points into whichever document
# the reader happens to be in rather than the one holding the target. In this
# paper that silently breaks the figure and table cross-references (16 of
# them); epubcheck reports them as "Fragment identifier is not defined".
#
# Rewriting them here, rather than not splitting at all, keeps the split and
# costs one pass over the generated XHTML.
# ---------------------------------------------------------------------------
echo "== relinking ==" >&2
python3 - "$out" <<'PY'
import os, re, shutil, sys, zipfile
path = sys.argv[1]
tmp = path + ".tmp"
with zipfile.ZipFile(path) as z:
items = [(i, z.read(i.filename)) for i in z.infolist()]
docs = {n: b.decode("utf-8") for n, b in
((i.filename, b) for i, b in items) if n.endswith(".xhtml")}
# Which document holds each id?
home = {}
for name, body in docs.items():
for i in re.findall(r'id="([^"]+)"', body):
home.setdefault(i, os.path.basename(name))
# pandoc titles each split document after its own filename, so a reader that
# shows the document title (or a screen reader announcing the page) says
# "ch004.xhtml" instead of "1 Introduction". Take the title from the first
# heading in the document.
titled = 0
BOOK_TITLE = "Forge: A Tool and Language for Teaching Formal Methods"
def retitle(body):
global titled
h = re.search(r"<h[1-6][^>]*>(.*?)</h[1-6]>", body, re.S)
if h:
text = re.sub(r"<[^>]+>", "", h.group(1))
else:
# Two split documents have no heading at all: the ACM reference
# format block and the licence footer. Use their leading bold run
# if there is one, and otherwise the book's title -- never the
# filename, which is what pandoc would leave behind.
lead = re.search(r"<(?:strong|b)[^>]*>(.*?)</(?:strong|b)>", body, re.S)
text = re.sub(r"<[^>]+>", "", lead.group(1)) if lead else BOOK_TITLE
text = text.rstrip(": ") or BOOK_TITLE
text = " ".join(text.split())
if not text:
return body
new, n = re.subn(r"<title>[^<]*</title>",
"<title>" + text.replace("&", "&") + "</title>",
body, count=1)
titled += n
return new
docs = {n: retitle(b) for n, b in docs.items()}
# Turn the sentinels planted before conversion back into <b> elements. This
# is safe to do with a regex on the generated XHTML precisely because the
# characters are private-use: they exist nowhere else in the document, and
# pandoc passed them through the code block untouched.
BOLD_ON, BOLD_OFF = "\ue000", "\ue001"
restored = 0
def unmark(body):
global restored
body, n = re.subn(BOLD_ON + r"(.*?)" + BOLD_OFF, r"<b>\1</b>", body, flags=re.S)
restored += n
return body
docs = {n: unmark(b) for n, b in docs.items()}
leftover = sum(b.count(BOLD_ON) + b.count(BOLD_OFF) for b in docs.values())
if leftover:
print(f" ERROR: {leftover} unpaired bold sentinels left in the text")
sys.exit(1)
fixed = 0
def relink(name, body):
global fixed
here = os.path.basename(name)
def sub(m):
global fixed
frag = m.group(1)
target = home.get(frag)
if target is None or target == here:
return m.group(0) # same file, or unknown: leave alone
fixed += 1
return f'href="{target}#{frag}"'
return re.sub(r'href="#([^"]+)"', sub, body)
docs = {n: relink(n, b) for n, b in docs.items()}
with zipfile.ZipFile(tmp, "w", zipfile.ZIP_DEFLATED) as z:
for info, blob in items:
# mimetype must be first and stored uncompressed
data = docs[info.filename].encode("utf-8") \
if info.filename in docs else blob
if info.filename == "mimetype":
z.writestr(info, data, compress_type=zipfile.ZIP_STORED)
else:
z.writestr(info, data)
shutil.move(tmp, path)
print(f" rewrote {fixed} cross-document links, {titled} document titles")
PY
# ---------------------------------------------------------------------------
# 4. Check.
# ---------------------------------------------------------------------------
echo "== epubcheck ==" >&2
epubcheck "$out"
echo "== fidelity ==" >&2
python3 - "$src" "$out" <<'PY'
# Diff the word multiset of the source HTML against the text of every XHTML
# document in the EPUB. This is the same test the manpage records for the
# HTML itself, and it is what catches the failures that matter: a section
# silently dropped, a table cell duplicated, a word split across a tag.
import collections, html, os, re, struct, sys, zipfile
def words(text):
# Compare *body* text only. <head> holds a <title> on each side (one in
# the source, sixteen in the split book) which would otherwise show up as
# a spurious loss and gain and mask a real one.
body = re.search(r"<body[^>]*>(.*)</body>", text, re.S)
text = body.group(1) if body else text
text = re.sub(r"<(script|style).*?</\1>", " ", text, flags=re.S)
text = re.sub(r"<[^>]+>", " ", text)
return collections.Counter(re.findall(r"\w+", html.unescape(text)))
source = words(open(sys.argv[1], encoding="utf-8").read())
book = collections.Counter()
with zipfile.ZipFile(sys.argv[2]) as z:
names = z.namelist()
for name in names:
# nav.xhtml is the reading system's table of contents, generated from
# the headings; counting it would double every heading.
if name.endswith((".xhtml", ".html")) and not name.endswith("nav.xhtml"):
book += words(z.read(name).decode("utf-8"))
lost = source - book
gained = book - source
# Words are allowed to go missing only if they belonged to something this
# script deliberately removed: the in-page table of contents (whose entries
# repeat the headings) and the lightbox's "Close" button. Subtracting those
# turns a vague "90 words differ, looks about right" into an assertion that
# either holds or fails.
raw = open(sys.argv[1], encoding="utf-8").read()
allowed = collections.Counter()
for pattern in (r'<nav class="toc".*?</nav>',
r'<dialog class="lightbox".*?</dialog>',
r'<span data-web-only>.*?</span>'):
for m in re.finditer(pattern, raw, re.S):
allowed += words("<body>" + m.group(0) + "</body>")
unexplained = lost - allowed
print(f" lost {sum(lost.values())} words "
f"({sum(unexplained.values())} unexplained), gained {sum(gained.values())}")
if unexplained:
print(" DROPPED TEXT:", dict(sorted(unexplained.items(),
key=lambda kv: -kv[1])[:30]))
if gained:
print(" DUPLICATED TEXT:", dict(sorted(gained.items(),
key=lambda kv: -kv[1])[:30]))
if unexplained or gained:
sys.exit(1)
# Every image the source shows must be in the book, and every <img> in the
# book must point at a file that is actually packed. pandoc renames the
# images (images/fig8a.png becomes EPUB/media/fileN.png), so the names
# cannot be compared directly -- count on one side, resolve on the other.
refs = set(re.findall(r'src="images/([^"]+)"',
open(sys.argv[1], encoding="utf-8").read()))
packed = {n for n in names if n.lower().endswith(".png")}
print(f" images: {len(refs)} referenced by paper.html, {len(packed)} packed")
if len(refs) != len(packed):
print(" IMAGE COUNT MISMATCH")
sys.exit(1)
used, broken = set(), []
with zipfile.ZipFile(sys.argv[2]) as z:
for name in names:
if not name.endswith((".xhtml", ".html")):
continue
base = name.rsplit("/", 1)[0]
for src in re.findall(r'<img[^>]+src="([^"]+)"',
z.read(name).decode("utf-8")):
target = os.path.normpath(os.path.join(base, src))
(used.add(target) if target in packed else broken.append(src))
if broken:
print(" BROKEN IMAGE REFERENCES:", broken)
sys.exit(1)
orphans = packed - used
if orphans:
print(" PACKED BUT NEVER SHOWN:", sorted(orphans))
sys.exit(1)
# No image may be asked to display wider than it actually is: that is what
# upscales a 269px screenshot to the width of a tablet. Check the declared
# width against the PNG's own header rather than trusting the markup.
overblown, unsized = [], 0
with zipfile.ZipFile(sys.argv[2]) as z:
natural = {}
for name in packed:
head = z.read(name)[:24]
if head[:8] == b"\x89PNG\r\n\x1a\n" and head[12:16] == b"IHDR":
natural[name] = struct.unpack(">I", head[16:20])[0]
for name in names:
if not name.endswith((".xhtml", ".html")):
continue
base = name.rsplit("/", 1)[0]
for tag in re.findall(r"<img[^>]+>", z.read(name).decode("utf-8")):
src = re.search(r'src="([^"]+)"', tag)
want = re.search(r"width:\s*(\d+)px", tag)
if not src:
continue
target = os.path.normpath(os.path.join(base, src.group(1)))
if want is None:
unsized += 1
elif int(want.group(1)) > natural.get(target, 1 << 30):
overblown.append((target, int(want.group(1)),
natural.get(target)))
print(f" image widths: {len(natural)} known, {unsized} without a width")
if unsized or overblown:
if overblown:
print(" UPSCALED:", overblown)
sys.exit(1)
# The paper sets Forge keywords bold inside its listings. pandoc cannot carry
# markup inside a code block at all, so without the sentinel round-trip every
# one of these is silently lost -- and no word goes missing, which is why the
# word-multiset check above cannot see it.
src_bold = sum(len(re.findall(r"<b>", m)) for m in
re.findall(r"<pre><code>(.*?)</code></pre>",
open(sys.argv[1], encoding="utf-8").read(), re.S))
book_bold = 0
with zipfile.ZipFile(sys.argv[2]) as z:
for name in names:
if not name.endswith((".xhtml", ".html")):
continue
for m in re.findall(r"<pre><code>(.*?)</code></pre>",
z.read(name).decode("utf-8"), re.S):
book_bold += len(re.findall(r"<b>", m))
print(f" bold keywords in listings: {src_bold} in source, {book_bold} in book")
if book_bold != src_bold:
print(" KEYWORD MARKUP LOST")
sys.exit(1)
# Splitting into 14 documents turns same-page anchors into cross-document
# links; a mistake here silently breaks every citation.
targets, links = set(), []
with zipfile.ZipFile(sys.argv[2]) as z:
for name in names:
if not name.endswith((".xhtml", ".html")):
continue
body = z.read(name).decode("utf-8")
base = name.rsplit("/", 1)[-1]
for i in re.findall(r'id="([^"]+)"', body):
targets.add((base, i))
for href in re.findall(r'href="([^"]+)"', body):
if href.startswith(("http:", "https:", "mailto:", "data:")):
continue
doc, _, frag = href.partition("#")
links.append((doc.rsplit("/", 1)[-1] or base, frag))
dangling = sorted({l for l in links if l[1] and l not in targets})
print(f" internal links: {len(links)}, dangling: {len(dangling)}")
if dangling:
print(" DANGLING:", dangling[:20])
sys.exit(1)
PY
echo "wrote $out" >&2
|