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

.Dd September 8, 2026
.Dt FORGE-PAPER 7
.Os
.Sh NAME
.Nm forge-paper
.Nd HTML rendering of the Forge paper (OOPSLA 2024)
.Sh DESCRIPTION
.Nm
is a semantic HTML rendering, with an
.Sy EPUB
edition alongside it, of
.Do
Forge: A Tool and Language for Teaching Formal Methods
.Dc ,
by Tim Nelson, Ben Greenman, Siddhartha Prasad, Tristan Dyer and others,
published in
.Em Proceedings of the ACM on Programming Languages ,
volume 8, OOPSLA1, article 116 (April 2024).
It is served at
.Lk https://forge-paper.softwaregardening.org .
.Pp
The paper describes Forge, a teaching tool built on Alloy that offers a
progression of increasingly expressive languages (Froglet, Relational Forge,
Temporal Forge), custom visualisation of instances, and testing constructs
aimed at students arriving from programming rather than from logic.
.Pp
This rendering exists because the published artifact is a two-column-free but
print-shaped PDF: it does not reflow, does not read well on a phone, and is
not searchable in the way a web page is.
The HTML is reflowable, has real headings, figures, code listings and tables,
and links every citation to its bibliography entry.
.Pp
The EPUB exists for the same reason one step further on: an e-reader has no
browser, so the page cannot simply be visited on the device most suited to
reading a 29-page paper away from a desk.
It is generated from the HTML, not from the PDF, and carries the same text.
.Ss What this is not
It is
.Em not
an official version.
It is not published or endorsed by the authors or by the ACM, and it is not
the version of record.
Quote the PDF, not this page.
Every page carries a banner saying so and linking the DOI.
.Sh LICENCE
The paper states on its first page that it is licensed under a
.Lk https://creativecommons.org/licenses/by/4.0/ "Creative Commons Attribution 4.0 International License" ,
which permits redistribution in any medium or format, including reformatting,
provided attribution is given.
That is the whole basis on which this rendering may be published.
Copyright remains with the authors
.Pq \(co 2024, held by the owner/author(s) .
.Pp
The DOI of the authoritative version is
.Lk https://doi.org/10.1145/3649833 ,
and the PDF this was made from is at
.Lk https://cs.brown.edu/people/sk/Publications/Papers/Published/ngp----forge/paper.pdf .
.Pp
Attribution, the copyright line, the licence link and the DOI appear both in a
banner at the top of the page and in the footer.
Do not remove them; they are the condition on which the rendering is allowed
to exist.
.Sh METHOD
The converter is in
.Pa converter/ ,
and the rendering is reproducible: running
.Pa converter/verify
fetches the PDF, rebuilds the page and checks it is byte for byte the
.Pa paper.html
that is committed here.
This section explains
.Em why
each pass exists, which the scripts cannot; the exact invocations are in
.Pa converter/extract ,
because a flag is not prose.
.Pp
It was for a long time a one-off pipeline kept outside the repository, on
the grounds that it had done its job.
That was a mistake: the converter turned out to have a bug that left two
thirds of the paper's citations unlinked, and fixing it meant recovering the
pipeline from a scratch directory it had been luck to still have.
.Pp
The essential trick is that
.Em two
extractions of the same PDF are combined, because neither is sufficient alone:
.Bl -tag -width "pdftotext -layout"
.It Nm pdftohtml Fl xml
Gives every span's font family, size, colour and position.
The paper is typeset with
.Nm acmart ,
which uses fonts consistently enough that a line's
.Em role
follows from its font: 15pt LinBiolinumTB is a heading, LinBiolinumTI a run-in
subsubsection, Inconsolata is code, 13pt LinBiolinum a caption, 12pt Libertine
at the foot of a page a footnote.
Running heads and feet lie outside the vertical band
.Bq 100 , 1005
and are dropped.
.It Nm pdftohtml Fl wbt No 40
The same, but with a wider word-break threshold.
Poppler splits Inconsolata into single letters at the default threshold
.Pq Dq p . f a t h e r ,
because the font's advances are wide; at 40 it resolves listings correctly
.Em and
preserves the
.Aq b
runs marking Forge keywords.
It is the source for all code, inline and displayed.
.It Nm pdftotext Fl layout
Used only as a fallback for listings whose geometry cannot be matched.
It gets a listing's shape right but loses font weight and pads tokens apart
.Pq Dq X , O .
.El
.Pp
The tradeoff runs both ways, which is the part worth remembering: the
.Fl wbt No 40
pass fixes code but runs prose words together
.Pq Dq equivalentto ,
so a displayed line that mixes the two \(em page 5's
.Dq no x, y: A | ... is not equivalent to ...
\(em must take its code from one pass and its roman text from the other.
.Ss Figures that are drawn, not embedded
Some figures are vector art: boxes, arrows and text drawn on the page rather
than placed as an image.
.Nm pdfimages
cannot extract them, and their labels are ordinary page text, so leaving them
as body text shreds the page.
Figure 8 is the worst case: it is two panels side by side, and because lines
are grouped by vertical position, a diagram label at one x-coordinate and a
line of code at another that happen to share a baseline were merged into a
single line.
.Pp
Two mechanisms handle this.
A table of column boundaries splits such regions into independent columns
before lines are formed, and a table of vector regions marks text that is
rasterised instead of transcribed.
Figure 8's diagram is cropped out of a 300 dpi rendering of the page; its
right-hand panel is a code listing and deliberately stays selectable text.
Figure 9's rating matrix, drawn as vector circles, is cropped the same way.
Crops carry
.Ar alt
text describing what they show, since their words are no longer in the
document.
.Pp
Citations were recovered from the PDF's own link annotations, which poppler
exposes.
An internal annotation resolves only to a
.Em page ,
so the citation's visible text is matched against an index of the bibliography
built from surnames and years, with the annotation's target page as
confirmation.
A citation that does not match confidently is left as plain text rather than
guessed.
All 68 entries are cited, and every citation resolves.
.Pp
The two citation styles must be read differently, and this is the detail
that is easy to get wrong.
.Nm acmart
brackets only the year in the narrative form, so
.Dq Brady [2013]
arrives as three annotated pieces \(em the author, the bracket, and the
year \(em and the author is found by looking back from the year.
The parenthetical form is one piece,
.Dq Jackson 2012 ,
where the author is simply the text before the year.
An earlier version of the converter recognised only a piece
.Em beginning
with a year, so it linked the narrative form and silently left every
parenthetical citation as plain text \(em about two thirds of them, and
increasingly so in the later sections, where citations are mostly
parenthetical.
.Pp
Looking backwards is safe only in the narrative form.
In a citation list every entry shares one annotation target, so a backward
scan from
.Dq Findler et al. 2002
runs straight into the previous citation and attributes it to the wrong
author.
A self-contained piece therefore reaches back only when it demonstrably
cannot stand alone: when it begins mid-author, as
.Dq et al. 2022
does after
.Dq Macedo ,
or continues a word broken by hyphenation, as
.Dq tools.org 2023
does after
.Dq alloy- .
.Pp
The annotated pieces are walked as one sequence per page rather than line by
line, because the typesetter breaks lines inside a citation: in
.Dq following Dolev / and Yao [1983]
the surname ends one line and the rest begins the next.
Scanning per line saw only
.Dq and Yao ,
which both mis-set the link text and lost the author.
A list may also name its author once and then give only years, as in
.Dq Beierle et al. 2003, 2004b
and
.Dq alloytools.org 2023a,b,c ,
so the last author resolved on the page is carried forward.
Adjacent anchors pointing at the same entry are then fused, so one citation is
one link rather than several abutting ones.
.Pp
The resolved entry is recorded on the piece itself rather than in a table
keyed by the piece's text, because that text is not unique: a bare
.Dq 2012
occurs under both Jackson and Montaghami and Rayside, and keying by text
gives one of them the other's reference.
.Pp
Output was checked by diffing the word multiset of
.Nm pdftotext
against the text content of the HTML, which is what caught the bugs that
mattered: dropped prose, duplicated table cells, a running head leaking into a
reference, and words split across a font change.
The result validates under
.Nm tidy
with no warnings and has no dangling internal links.
.Pp
Citations need a second check, because none of the above can see them: a
citation linked to the wrong entry, or not linked at all, changes no word
in the document.
They are checked against the
.Em rendered
HTML rather than by re-running the matcher, which would only confirm the
converter agrees with itself: for each anchor, the surname and year visible
in the link text must actually occur in the entry it points at.
That is what caught the backward scan crossing into the neighbouring
citation.
.Ss The EPUB
This step is
.Pa make-epub ,
next to the page rather than under
.Pa converter/ ,
because it runs on
.Pa paper.html
and needs neither the PDF nor any of the extraction above.
It converts
.Pa paper.html
with
.Nm pandoc ,
splitting at each
.Aq h2
so the reader gets one document per section and a working position
indicator, and validates the result with
.Nm epubcheck .
Run it after editing
.Pa paper.html
and commit the result.
.Pp
Most of the script is not the conversion but the things
.Nm pandoc
gets wrong on this input, none of which are visible without checking:
.Bl -bullet
.It
.Sy Splitting breaks every non-heading cross-reference .
When the document is split,
.Nm pandoc
rewrites
.Dq #foo
to
.Dq chNNN.xhtml#foo
only for ids it generated itself, i.e. those on headings.
Ids that came from the source \(em
.Aq figure ,
.Aq table ,
each bibliography entry \(em are left as bare fragments, which then resolve
against whichever document the reader happens to be in.
Twelve figure and table references broke this way.
A pass over the generated XHTML repairs them.
.It
.Sy A role attribute silently deletes the footnotes .
.Li role="doc-noteref"
makes the HTML reader treat the anchor as a footnote reference, look for a
.Nm pandoc
footnote of that name, fail to find one \(em the notes here are inline
.Aq span
elements \(em and emit an empty note, destroying both the mark and its target.
The attribute is dropped before conversion.
.It
.Sy The title is typeset twice .
.Nm pandoc
only recognises the document's own title heading if it is the first thing in
.Aq body .
Here the
.Aq h1
sits inside
.Aq header ,
so it is treated as body text and a second title is synthesised from the
metadata, under a colliding id.
The heading is hoisted to the front and the
.Aq header
unwrapped.
.It
.Sy Bold keywords vanish from the listings .
.Nm pandoc
represents a code block as a
.Em plain string ,
so it cannot carry markup inside one and drops all 63 of the
.Aq b
runs that mark Forge keywords.
There is no flag for this: the node has nowhere to put them.
Since the
.Fl wbt No 40
pass exists partly to capture those runs, losing them here would undo that
work, so each is bracketed with a private-use character before conversion and
turned back into a
.Aq b
afterwards \(em the text of a code block passes through
.Nm pandoc
byte for byte, so the marks survive.
.El
.Pp
Three smaller corrections are for readers rather than for
.Nm pandoc .
Each split document is titled after its own heading instead of after its
filename.
A dash is inserted between an author and their affiliation, which on the web
is a CSS margin and would otherwise read
.Dq Tim NelsonBrown University
wherever the stylesheet is disabled.
And each image is given its own natural width, read out of the PNG header,
because a reading system told only
.Li max-width
may either stretch an image to the measure or shrink it to a thumbnail; the
extracted figures range from 269 to 1595 px, so no single rule suits them all.
.Pp
The EPUB is checked the same way the HTML was, and the check is an assertion
rather than a report: words may go missing only if they belong to something
the script deliberately removed, and no word may appear more times than it
does in the source.
That second half is what caught the duplicated title.
It also verifies that every image is packed, shown, and never asked to
display wider than it really is, that the keyword markup survived, and that
no internal link dangles after the split.
.Pp
The last two of those are there because a word-multiset diff cannot see them:
losing every bold run, or stretching a 269 px screenshot across a tablet,
changes no word in the document.
Both happened, and both were found by reading the output rather than by any
check \(em hence the checks.
Deleting a single paragraph during conversion likewise makes the script exit
non-zero while
.Nm epubcheck
still passes, which is the point of having both.
.Sh FILES
.Bl -tag -width "epub-metadata.xml" -compact
.It Pa paper.html
The rendering; becomes
.Pa index.html
in the served site.
Committed, but generated \(em see
.Pa converter/ .
.It Pa images/
18 PNGs extracted from the PDF.
They are roughly three times the size the PDF displayed them at, which is why
the page offers click-to-enlarge.
.It Pa forge-paper.epub
The EPUB edition, served next to the page and linked from its banner.
Committed, but generated \(em see
.Pa make-epub .
.It Pa make-epub
Regenerates
.Pa forge-paper.epub
from
.Pa paper.html .
Run it by hand after editing the HTML.
.It Pa epub.css
Stylesheet for the EPUB.
Deliberately not the one in
.Pa paper.html ,
which is built for a browser; this one sets only what the reading system
cannot infer, and lets it own the fonts, colours and measure.
.It Pa epub-metadata.xml
Dublin Core metadata: the fifteen authors as fifteen entries, the licence,
and an identifier that is the published URL rather than the DOI.
.It Pa converter/
The PDF-to-HTML pipeline that produced
.Pa paper.html
and
.Pa images/ .
.Pa extract
fetches the PDF and runs the poppler passes;
.Pa convert.py
builds the page;
.Pa verify
does both and asserts the result matches what is committed.
Nothing it derives is committed, since all of it is reproducible from the
PDF.
.El
.Sh SEE ALSO
Forge itself:
.Lk https://forge-fm.org/ .
.Pp
The NixOS module that serves this page is
.Pa users/Profpatsch/softwaregardening/module.nix .
The live site is checked with
.Nm link-check ,
in
.Pa users/Profpatsch/link-check .
.Sh CAVEATS
.Bl -bullet
.It
.Sy The EPUB is committed, and nothing checks that it matches Pa paper.html .
Editing the HTML without re-running
.Pa make-epub
leaves a book that is silently out of date, and the difference will not show
up in review: the diff shows one changed line of HTML and an unchanged binary.
If you touch
.Pa paper.html ,
run
.Pa ./make-epub
in the same change.
.It
Everything the EPUB says about itself is asserted in
.Pa epub-metadata.xml
and is not derived from the paper, so a revision of the article would not
update it.
Note in particular that
.Li dc:identifier
is the URL this file is published at and
.Em not
the DOI.
The DOI names the version of record; a file claiming it as its own identifier
would be claiming to
.Em be
the ACM's article, which is the one thing this is not.
The DOI is recorded as
.Li dc:source ,
which is the correct relation.
.It
The EPUB has no cover image, so readers will show a generic placeholder.
This is deliberate: inventing cover art for someone else's paper is exactly
the implied endorsement the banner exists to deny.
.It
In the EPUB the sidenotes become indented boxes in the text rather than
margin notes, and code lines wrap instead of scrolling.
Wrapping is the lesser evil: a reading system cannot scroll horizontally, so
an over-long line would be
.Em clipped ,
and losing a line of a listing is worse than an ugly break.
The longest line in the paper is 71 characters, so it rarely arises.
.It
.Sy Tables 1 and 2, and figure 12, were transcribed by hand .
They are drawn with vector rules in the PDF, so no text extraction recovers
them as rows and columns.
They were checked against pages 7, 14 and 23, but they are the parts most
likely to contain an error that no automated check can catch.
Verify against the PDF before relying on a number from them.
.It
The rasterised regions (figure 8's diagram, figure 9's rating matrix) are
cropped by fixed coordinates in
.Pa converter/vectorfigs.py .
Their words are no longer text on the page, so they are neither searchable
nor selectable, and the crop boxes would need adjusting if the PDF were
re-typeset.
.It
Mathematics passes through as Unicode, not MathML.
The paper is light on mathematics, so this is adequate here, but a formula
heavy paper would need different handling.
.It
Small capitals in the original mark both acronyms
.Pq Dq fm , Dq ide
and assignment names
.Pq Dq river , Dq memory .
They are rendered as styled spans rather than
.Aq abbr ,
because calling an assignment name an abbreviation would be wrong.
.It
The rendering is of one fixed revision of the PDF
.Pq last modified October 2025 ,
pinned by a
.Li sha256
digest in
.Pa converter/extract .
If the authors revise it, nothing here notices on its own \(em the page is
served from a committed file and does not re-fetch anything \(em but the
next run of
.Pa converter/verify
fails loudly rather than quietly rendering a different paper.
The digest should not simply be updated to match: the crop boxes in
.Pa converter/vectorfigs.py
and the bibliography page range used to confirm citations are tied to this
revision.
.It
Three reference links are dead
.Pq two Li 10.5555 No DOIs and a Brown thesis URL .
They are dead in the published PDF too \(em the URLs here are exactly the ones
its own link annotations carry \(em so they are reproduced rather than
repaired.
Silently correcting an author's citation would make this a different paper
from the one it claims to be.
Expect
.Nm link-check
to report them.
.El