History log of /seL4-l4v-10.1.1/HOL4/tools/Holmake/HM_GraphBuildJ1.sml
Revision Date Author Comments
# 4ba33079 16-Jan-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Holmake improvements (bug in caching of dep. analysis; diag change)

Two intertwined patches (bad form I know):
1. Fix the bug in tests/indepchildren.
2. Revise the internal diag function to take a function generating a
string rather than a string; then the work of generating the string
only happens if diagnostics have been asked for.


# 24d35518 13-Jul-2017 Michael Norrish <Michael.Norrish@nicta.com.au>

Fixes for Moscow ML and poly -j1 Holmake given 46ee3d3ef

Fixes compilation error for former as well as misbehaviour in the
presence of multi-step commands for multiple targets.


# 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


# 140144ea 18-Apr-2017 Michael Norrish <Michael.Norrish@nicta.com.au>

Make j1 Poly build pass on environment variable to sub-shells

Also rename reloc_build to relocbuild internally (making SML variable
name match command-line option name).


# a870a911 23-Jan-2017 Michael Norrish <Michael.Norrish@nicta.com.au>

Rebuild .uo and .ui files without forcing unnecessary extra work

This is by analogy with what has already been attempted for heaps, and
is progress with github issue #105.

Also fix a bug with the heap handling if the heap was in a
directory with script-files (not the case with the heaps in HOL/src):
the dependency graph built for the directory spotted that there was a
dependency from the heap to the script files, and even though the
heap's time-stamp was set appropriately, the existence of the link in
the graph meant that the rest of the graph got executed.

The fix for this (in both the case of the heap and the .uo/.ui file)
is for execution of graph nodes to check at the time the node is made
ready to execute if the target really does need to be redone (by
examining time-stamps). Then, the rebuild can be skipped even though
the initial analysis thought it was going to have to happen.

Future work:
- For the moment, both build and Holmake rely on having a particular
environment variable set to enable this option. I will augment
and/or replace this with command-line options. (The buildheap
program needs to retain this use of the environment variable though
because neither Holmake nor build control how that program is
called; instead this program is called by the user via
Holmakefiles.)
- Build needs to take an option to clean a HOL installation of its
heaps and ui/uo files. I don't know how to automatically identify
the heaps, but could just purge those that are identified as such in
Holmakefiles.


# bd86c2f5 03-May-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Improve error-reporting in -j1 Holmake

Includes more error messages when --dbg is set


# 18d1c2f7 20-Apr-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Enable multiplexed builds for Poly/ML

Output is horrendous at the moment


# 50c4d56b 18-Apr-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Make dep. graph store single commands per node

This is something of a reversal of 8f7f1c9; but there I was worried
about smashing multiple commands into a single string, which is clearly
still a bad thing to have happen. The problem with having multiple
commands in a single node is that a multiplexing implementation has to
execute them as an atomic block, which I don't like.


# b6dd58ef 14-Apr-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Get "build from graph" Holmake to compile

Poly/ML version fails miserably at boolScript hurdle however.