Forward Build Systems, Formally
Sarah Spall, Neil Mitchell, Sam Tobin-Hochstadt

TL;DR
This paper formally defines the correctness of forward build systems, proves the correctness of systems like Rattle, Fabricate, and Memoize, and models them in Agda to ensure reliable dependency management in software builds.
Contribution
It provides a formal correctness definition for forward build systems and verifies the correctness of several systems using Agda, addressing a gap in build system reliability.
Findings
Rattle's optimizations preserve correctness
Fabricate and Memoize are also correct
Formal modeling in Agda supports build system correctness
Abstract
Build systems are a fundamental part of software construction, but their correctness has received comparatively little attention, relative to more prominent parts of the toolchain. In this paper, we address the correctness of \emph{forward build systems}, which automatically determine the dependency structure of the build, rather than having it specified by the programmer. We first define what it means for a forward build system to be correct -- it must behave identically to simply executing the programmer-specified commands in order. Of course, realistic build systems avoid repeated work, stop early when possible, and run commands in parallel, and we prove that these optimizations, as embodied in the recent forward build system \textsc{Rattle}, preserve our definition of correctness. Along the way, we show that other forward build systems, such as \textsc{Fabricate} and…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
