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

correct :: (Ord k, Eq v) => Build Monad i k v -> Tasks Monad k v -> Bool

Given a build and tasks, check that build produces a correct result for any initial store and a target key.

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.

idempotent :: Eq v => Build Monad i k v -> Tasks Monad k v -> Bool

Check that a build system is idempotent, i.e. running it once or twice in a row leads to the same resulting Store.