HOL
HOL copied to clipboard
Holmakefile options per directory only
I notice that if one has CLINE_OPTIONS
in the Holmakefile
set to -j1
, then this is propagated to recursive Holmake
calls in INCLUDES
directories as well. I guess this fits the semantics of CLINE_OPTIONS
: it's would happen if you'd included this option on the command line.
But how would one indicate that a particular directory should be built with -j1
but not its dependencies? (They should instead use their own Holmakefile
s' CLINE_OPTIONS
or the defaults.)
This issue is a feature request for that capability.
Hmm, I suppose a definition setting something like LOCAL_CLINE_OPTIONS
might work. You only pick up CLINE_OPTIONS
if you start the make in that directory, but LOCAL_CLINE_OPTIONS
are always applied, but only locally.
On the other hand, what happens when Holmake
builds all directories at once? What happens if something from a -j1
directory is scheduled to run at the same time as something from a -j8
directory?
I think the desired semantics is if some -j<n>
option is specified for a directory, then any job in that directory can only be run in a pool of n
or fewer jobs. (The work required to implement this may be larger than its benefit.)