论文标题
正式的向前构建系统
Forward Build Systems, Formally
论文作者
论文摘要
构建系统是软件构建的基本组成部分，但相对于工具链的更突出的部分，它们的正确性受到相对较少的关注。在本文中，我们解决了\ emph {forward build Systems}的正确性，该系统会自动确定构建的依赖关系结构，而不是由程序员指定。 我们首先定义了向前构建系统正确的含义 - 它必须相同的行为简单地按顺序执行程序员指定的命令。当然，逼真的构建系统避免重复工作，尽可能提早停止并并行运行命令，我们证明，这些优化在最近的前向构建系统\ textsc {rattle}中体现出来，保留了我们对正确性的定义。一路上，我们表明其他正向构建系统（例如\ textsc {fabrate}和\ textsc {memooize}也是正确的。 我们在\ agda中执行所有工作，并详细描述\ textsc {rattle}本身以及我们对其建模的基础假设。
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 \textsc{Memoize}, are also correct. We carry out all of our work in \Agda, and describe in detail the assumptions underlying both \textsc{Rattle} itself and our modeling of it.
