History log of /seL4-l4v-10.1.1/HOL4/tools/Holmake/tests/coproduct/Holmakefile
Revision Date Author Comments
# 46ee3d3e 13-Jul-2017 Michael Norrish <Michael.Norrish@nicta.com.au>

Allow an indication of side-products of theory builds

Basically, write something like

foo: *theorynameScript.sml

to indicate that foo will be built when the theory theoryname is
built. As part of the process, provide much better testing of the
parallel execution of multiple target rules and completely change the
way these are handled.

In particular, the dependency graph that Holmake maintains now does
not have multiple targets for a single node, but instead makes sure
that when a command is executed for a single target, all nodes that
would execute the same command are considered to be running at the
same time, and get the same success/failure status when the command
finishes.

Needs documentation, but is progress with Github issue #429