forge-paper(7)

NAME

forge-paper - HTML rendering of the Forge paper (OOPSLA 2024)

DESCRIPTION

forge-paper is a semantic HTML rendering, with an EPUB edition alongside it, of "Forge: A Tool and Language for Teaching Formal Methods" , by Tim Nelson, Ben Greenman, Siddhartha Prasad, Tristan Dyer and others, published in Proceedings of the ACM on Programming Languages, volume 8, OOPSLA1, article 116 (April 2024). It is served at https://forge-paper.softwaregardening.org.

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.

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.

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.

What this is not

It is 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.

LICENCE

The paper states on its first page that it is licensed under a 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 (© 2024, held by the owner/author(s)).

The DOI of the authoritative version is https://doi.org/10.1145/3649833, and the PDF this was made from is at https://cs.brown.edu/people/sk/Publications/Papers/Published/ngp----forge/paper.pdf.

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.

METHOD

The converter is in converter/, and the rendering is reproducible: running converter/verify fetches the PDF, rebuilds the page and checks it is byte for byte the paper.html that is committed here. This section explains why each pass exists, which the scripts cannot; the exact invocations are in converter/extract, because a flag is not prose.

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.

The essential trick is that two extractions of the same PDF are combined, because neither is sufficient alone:

pdftohtml -xml

Gives every span's font family, size, colour and position. The paper is typeset with acmart, which uses fonts consistently enough that a line's 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 [100, 1005] and are dropped.

pdftohtml -wbt 40

The same, but with a wider word-break threshold. Poppler splits Inconsolata into single letters at the default threshold ("p. f a t h e r"), because the font's advances are wide; at 40 it resolves listings correctly and preserves the <b> runs marking Forge keywords. It is the source for all code, inline and displayed.

pdftotext -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 ("X, O").

The tradeoff runs both ways, which is the part worth remembering: the -wbt 40 pass fixes code but runs prose words together ("equivalentto"), so a displayed line that mixes the two — page 5's "no x, y: A | ... is not equivalent to ..." — must take its code from one pass and its roman text from the other.

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. 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.

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 alt text describing what they show, since their words are no longer in the document.

Citations were recovered from the PDF's own link annotations, which poppler exposes. An internal annotation resolves only to a 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.

The two citation styles must be read differently, and this is the detail that is easy to get wrong. acmart brackets only the year in the narrative form, so "Brady [2013]" arrives as three annotated pieces — the author, the bracket, and the year — and the author is found by looking back from the year. The parenthetical form is one piece, "Jackson 2012", where the author is simply the text before the year. An earlier version of the converter recognised only a piece beginning with a year, so it linked the narrative form and silently left every parenthetical citation as plain text — about two thirds of them, and increasingly so in the later sections, where citations are mostly parenthetical.

Looking backwards is safe only in the narrative form. In a citation list every entry shares one annotation target, so a backward scan from "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 "et al. 2022" does after "Macedo", or continues a word broken by hyphenation, as "tools.org 2023" does after "alloy-".

The annotated pieces are walked as one sequence per page rather than line by line, because the typesetter breaks lines inside a citation: in "following Dolev / and Yao [1983]" the surname ends one line and the rest begins the next. Scanning per line saw only "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 "Beierle et al. 2003, 2004b" and "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.

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 "2012" occurs under both Jackson and Montaghami and Rayside, and keying by text gives one of them the other's reference.

Output was checked by diffing the word multiset of 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 tidy with no warnings and has no dangling internal links.

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 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.

The EPUB

This step is make-epub, next to the page rather than under converter/, because it runs on paper.html and needs neither the PDF nor any of the extraction above. It converts paper.html with pandoc, splitting at each <h2> so the reader gets one document per section and a working position indicator, and validates the result with epubcheck. Run it after editing paper.html and commit the result.

Most of the script is not the conversion but the things pandoc gets wrong on this input, none of which are visible without checking:

• Splitting breaks every non-heading cross-reference. When the document is split, pandoc rewrites "#foo" to "chNNN.xhtml#foo" only for ids it generated itself, i.e. those on headings. Ids that came from the source — <figure>, <table>, each bibliography entry — 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.

• A role attribute silently deletes the footnotes. role="doc-noteref" makes the HTML reader treat the anchor as a footnote reference, look for a pandoc footnote of that name, fail to find one — the notes here are inline <span> elements — and emit an empty note, destroying both the mark and its target. The attribute is dropped before conversion.

• The title is typeset twice. pandoc only recognises the document's own title heading if it is the first thing in <body>. Here the <h1> sits inside <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 <header> unwrapped.

• Bold keywords vanish from the listings. pandoc represents a code block as a plain string, so it cannot carry markup inside one and drops all 63 of the <b> runs that mark Forge keywords. There is no flag for this: the node has nowhere to put them. Since the -wbt 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 <b> afterwards — the text of a code block passes through pandoc byte for byte, so the marks survive.

Three smaller corrections are for readers rather than for 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 "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 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.

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.

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 — hence the checks. Deleting a single paragraph during conversion likewise makes the script exit non-zero while epubcheck still passes, which is the point of having both.

FILES

paper.html

The rendering; becomes index.html in the served site. Committed, but generated — see converter/.

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.

forge-paper.epub

The EPUB edition, served next to the page and linked from its banner. Committed, but generated — see make-epub.

make-epub

Regenerates forge-paper.epub from paper.html. Run it by hand after editing the HTML.

epub.css

Stylesheet for the EPUB. Deliberately not the one in 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.

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.

converter/

The PDF-to-HTML pipeline that produced paper.html and images/. extract fetches the PDF and runs the poppler passes; convert.py builds the page; 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.

SEE ALSO

Forge itself: https://forge-fm.org/.

The NixOS module that serves this page is users/Profpatsch/softwaregardening/module.nix. The live site is checked with link-check, in users/Profpatsch/link-check.

CAVEATS

• The EPUB is committed, and nothing checks that it matches paper.html. Editing the HTML without re-running 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 paper.html, run ./make-epub in the same change.

• Everything the EPUB says about itself is asserted in epub-metadata.xml and is not derived from the paper, so a revision of the article would not update it. Note in particular that dc:identifier is the URL this file is published at and not the DOI. The DOI names the version of record; a file claiming it as its own identifier would be claiming to be the ACM's article, which is the one thing this is not. The DOI is recorded as dc:source, which is the correct relation.

• 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.

• 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 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.

• 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.

• The rasterised regions (figure 8's diagram, figure 9's rating matrix) are cropped by fixed coordinates in 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.

• 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.

• Small capitals in the original mark both acronyms ("fm, "ide"") and assignment names ("river, "memory""). They are rendered as styled spans rather than <abbr>, because calling an assignment name an abbreviation would be wrong.

• The rendering is of one fixed revision of the PDF (last modified October 2025), pinned by a sha256 digest in converter/extract. If the authors revise it, nothing here notices on its own — the page is served from a committed file and does not re-fetch anything — but the next run of converter/verify fails loudly rather than quietly rendering a different paper. The digest should not simply be updated to match: the crop boxes in converter/vectorfigs.py and the bibliography page range used to confirm citations are tied to this revision.

• Three reference links are dead (two 10.5555 DOIs and a Brown thesis URL). They are dead in the published PDF too — the URLs here are exactly the ones its own link annotations carry — 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 link-check to report them.