Build

Build systems and the properties they should ensure.

Build

type Build c i k v = Tasks c k v -> k -> Store i k v -> Store i k v

A build system takes a description of Tasks, a target key, and a store, and computes a new store, where the key and its dependencies are up to date.

Properties

correctBuild :: (Ord k, Eq v) => Tasks Monad k v -> Store i k v -> Store i k v -> k -> Bool

Given a description of tasks, an initial store, and a result produced by running a build system on a target key, this function returns True if the result is a correct build outcome. Specifically: * result and store must agree on the values of all inputs. In other words, no inputs were corrupted during the build. * result is consistent with the tasks, i.e. for every non-input key, the result of recomputing its task matches the value stored in the result.