Forward build systems, formally
Forward build systems, formally
复制标题
正向构建系统，正式
DOI：
10.1145/3497775.3503687
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Tobin-Hochstadt, Sam
中科院分区：
文献类型：
--
作者：
Spall, Sarah;Mitchell, Neil;Tobin-Hochstadt, Sam
构建系统是软件构建的基本部分，但相对于工具链中更重要的部分，它们的正确性相对较少受到关注。在本文中，我们解决了正向构建系统的正确性，它会自动确定构建的依赖结构，而不是由程序员指定。我们首先定义了正向构建系统正确的含义-它的行为必须与简单地执行程序员指定的命令相同。当然，现实的构建系统避免重复的工作，尽可能早地停止，并并行运行命令，我们证明了这些优化，体现在最近的前向构建系统Rattle，保持我们的正确性的定义。沿着这条路，我们展示了其他正向构建系统，如Fabricate和Memoize，也是正确的。我们在Agda中进行了所有的工作，并详细描述了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 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 Rattle, preserve our definition of correctness. Along the way, we show that other forward build systems, such as Fabricate and Memoize, are also correct.We carry out all of our work in Agda, and describe in detail the assumptions underlying both Rattle itself and our modeling of it.
影响因子：
2
作者：
Stevens, Perdita
通讯作者：
Stevens, Perdita
具有动态依赖关系的健全且优化的增量构建系统
DOI：
10.1145/2814270.2814316
发表时间：
2015
期刊：
Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
影响因子：
--
作者：
Sebastian Erdweg;Moritz Lichter;Manuel Weiel
通讯作者：
Manuel Weiel
Agda 中的依赖类型编程
DOI：
--
发表时间：
2009
期刊：
ACM SIGPLAN International Workshop on Types In Languages Design And Implementation
影响因子：
--
作者：
U. Norell
通讯作者：
U. Norell