h t t p s : / / n d m i t c h e l l . c o m / d o w n l o a d s / p a p e r - b u i l d _ s y s t e m s _ a _ l a _ c a r t e _ t h e o r y _ a n d _ p r a c t i c e - 2 1 _ a p r _ 2 0 2 0 . p d f

Ingest: Build systems à la carte: Theory and practice

Type: types/ingest-report.md

Classification

This is a peer-reviewed journal paper (Journal of Functional Programming 30, e11, 2020, 55 pages). It extends the ICFP 2018 conference paper with executable Haskell models, a formal correctness definition, and new experience and engineering sections. The genre is scientific-paper: the contribution is a formal framework plus design reports, not a controlled experiment. Author: Andrey Mokhov (Newcastle University / Jane Street), Neil Mitchell (Facebook; author of Shake), Simon Peyton Jones (Microsoft Research). High credibility on build-system mechanics. The authors also built the systems they report on (Shake, Cloud Shake, Hadrian), so the experience sections are reports from interested builders.

Summary

The paper models any build system as a scheduler, which decides the order in which tasks run (topological, restarting or suspending), composed with a rebuilder, which decides whether a task must rerun (dirty bit, verifying traces, constructive traces or deep constructive traces). It classifies Make, Excel, Shake, Bazel, Buck, Nix, Ninja and CloudBuild as cells of this 3×4 grid. A task is a function over a fetch callback; its constraint (Applicative or Monad) decides whether dependencies are static or discovered while it runs. Correctness (§3.6) means that recomputing any non-input key from the final store gives exactly the stored value. Relative to the conference-version ingest, the new material is the substance here. §5.2.2 describes verifying step traces. §7 reports that Cloud Shake, the predicted suspending × constructive-trace cell, was built and used for GHC's build system. That section adds rule and script versions to cache keys, and it reports that missing dependencies and undeclared outputs caused most cloud-migration failures. §8 covers untracked dependencies, non-determinism and volatility (§8.3); the "Frankenbuild" failure of deep traces under non-determinism (§8.4); self-tracking (§8.8); and file watching (§8.9). §9.1 names Fabricate, a script replayed top to bottom with OS-traced commands, as the one system the framework cannot model cleanly.

Contribution assessment (our opinion)

The problem matters: build systems are widely used and rarely studied, and before this work there was no shared vocabulary for comparing them. The main contribution is an explanatory decomposition. Properties that looked like system idiosyncrasies (early cutoff, minimality, support for dynamic dependencies, shallow builds) become consequences of two orthogonal choices. The executable models make the claims precise enough to check. The framework also passed a real test of its consequences. It predicted that an empty cell would give a workable system, and Cloud Shake was then built and deployed (§7). That is stronger support than the classification alone. The evidence is still qualitative: one deployment anecdote, mixed CI results for GHC, and no measured comparison across cells. The §8 corrections show that the clean correctness definition stops at impure tasks; the authors adjust it rather than fold impurity into the core model. These limits narrow the framework's reach to pure-function tasks; they do not undermine the decomposition. I cannot judge priority over the incremental-computation literature beyond the paper's own §9; the "first cloud build system with early cutoff and monadic dependencies" claim is the authors' own.

Quotes

No source quotes have been retained yet.

Connections Found

For the occasion, this paper is the classification basis, and its §8.3 is the diagnosis. A workflow engine that replays its definition from the top on every step has a script-ordered scheduler; §9.1 shows this shape in Fabricate and says it fits the framework only as a linear chain of monadic tasks. If replay stops at the first job whose inputs are not ready and resumes from the top on the next step, the scheduler is a restarting one. Storing an input hash and an output hash per accepted job makes the rebuilder a verifying trace (§5.2). That combination is the restarting × verifying-traces cell, which Table 2 leaves uninhabited and the paper calls workable. This placement is our mapping; the paper does not discuss workflow engines or acceptance validators. A validator that reads undeclared files is a task with untracked dependencies in the §8.3 sense, so the job's recorded trace cannot predict the validator's verdict.

For the KB, the paper is the formal anchor for the derived-artifact freshness cluster, and it adds the limits the conference ingest lacked. It is evidence for Criteria edits invalidate verdicts; process edits invalidate artifacts. §8.8 says systems whose tasks are full programs must pessimistically assume that any script change may change any task. §7.3 puts script and rule versions into Cloud Shake's cache keys to avoid stale products. It is evidence for A derived copy of recomputable truth must be checked or absent: §3.6 is a formal definition of "checked". It is also evidence for LLM recompute cost shifts the store-vs-recompute balance: §8.3 replaces exact equality with membership in the set of possible results for non-deterministic tasks, and §8.4 shows that deep traces then return results inconsistent with their own dependencies. It supplies failure modes for Link graph plus timestamps enables make-like staleness detection: a timestamp dirty bit cannot support early cutoff, and backup software can move timestamps backwards (§5.1). It is evidence for First-principles analysis maps a design space before selecting within it. That note says Cloud Shake "remained a blueprint", which is accurate for the 2018 paper but is overtaken by §7 of this version.

It compares with the conference-version ingest on evidential scope: the 2018 paper supplies the grid, and this version supplies experience and impurity handling. It compares with the Eigenius review on memo-key completeness. That review finds a memo key that omits the component-definition version, which is the missing-self-tracking failure that §7.3 and §8.8 name. Freshness architecture is a see-also: Commonplace's role-labelled input hashes per target are a verifying-trace rebuilder in this vocabulary.

Extractable Value

  1. Classification of the occasion's engine -- In the paper's terms, an engine that replays its definition from the top and stores per-job input and output hashes is a script-ordered (restarting) scheduler with a verifying-trace rebuilder. Fabricate (§9.1) is its nearest named relative. If the stored output hash can be used to restore content without rerunning, the rebuilder moves toward constructive traces (§5.3). The classification predicts that the engine supports dynamic dependencies and early cutoff but not shallow builds. It also predicts that minimality fails wherever replay repeats work before a job aborts (§4.2). [quick-win]
  2. The smallest stabilising change is to track the validator's reads -- The paper offers three responses to an untracked dependency (§8.3, §7.4): track it, mark the task volatile, or leave it untracked. Marking the validator volatile reruns it on every step, which is exactly the current instability. Leaving the reads untracked and skipping the rerun makes recheck stable but incorrect under §3.6. Tracking the reads keeps both stability and correctness. In this design the validator counts as part of the job's task. The engine records the paths and content hashes the validator read, plus the validator's own version (§7.3, §8.8), in the job's trace. On replay, the engine verifies those hashes first and reruns the validator only when one has changed. Run-time tracking of reads is the paper's track (§3.7); the FSATrace lint (§7.4) is the automated form when reads cannot be declared by hand. This prescription is our derivation from the paper's mechanisms; the paper does not test it on validators. [experiment]
  3. Exact recheck has a stated boundary -- §3.6 correctness depends on deterministic tasks. §8.3 weakens it to set membership for non-deterministic tasks, and §8.4 shows that caching on terminal inputs alone yields a Frankenbuild. For LLM-produced artifacts, exact-equality rebuilders therefore apply only to the deterministic envelope (hashes, marks, generated regions). Judgment-produced outputs need versioned task identity plus a membership check, which in practice is review. This sharpens the derived-copy and recompute-cost notes. [deep-dive]
  4. Task identity belongs in the key -- §7.3's two Ver arguments and §8.8's pessimistic self-tracking give a reusable rule: a trace or memo key that omits the version of the producing rule will reuse stale products after a rule edit. This applies to both the occasion's validator and the Eigenius finding. [quick-win]
  5. Predicted-cell evidence for design-space mapping -- §7 reports that a cell predicted from the grid was implemented and used in daily work. This is a stronger example for the first-principles note than the 2018 "blueprint" wording. [quick-win]
  6. Undeclared outputs and inputs fail first when results are shared -- §7.4 reports that most of GHC's cloud-migration failures came from undeclared produced files, and that a cloud build may build an output only once. Any engine that reuses accepted results across runs or agents faces this risk directly. [just-a-reference]

Limitations (our opinion)

The evidence for the framework's practical value is a small set of reports from the authors' own systems: one user quote, GHC's mixed CI results, and no cross-cell measurements. The correctness definition and the grid assume pure tasks. §8 handles untracked dependencies, non-determinism and volatility as adjustments, not as part of the model, so the grid says little about how to choose among those adjustments. That gap matters for the occasion, because an acceptance validator with undeclared reads falls exactly in the §8 territory. The paper's suspending-versus-restarting cost claims are qualitative ("may often be just a fraction"). The Fabricate discussion is short, so placing a replay-from-top workflow engine in the restarting column is our interpretation and not a classification the paper makes. A simpler account of Cloud Shake's success is that Shake already had verifying traces and adding constructive traces was a modest engineering step; §7.3 itself calls it a "bolt-on". The framework's predictive credit is real but modest. Nothing here addresses tasks whose output is judged rather than computed, which the LLM recompute cost note treats as the central case.

Write a short design note in kb/reference/proposals/ for the workflow engine. It should classify the engine as a restarting scheduler with a verifying-trace rebuilder, citing this ingest. It should also specify the minimal change: record the acceptance validator's read set (path plus content hash) and validator version in each accepted job's trace, and rerun the validator on replay only when a recorded hash differs.