History log of /seL4-l4v-10.1.1/HOL4/tools/Holmake/Holmake_tools.sig
Revision Date Author Comments
# 7c7ec861 20-May-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Make tty-output (Holmake and testutils) terminal-width aware

Holmake even checks for resizing every second so that long-running
jobs can have the terminal resized by the user and have the pretty
columns of jobs adjust accordingly.

Closes #526


# 1bdfad7e 05-Mar-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Reduce and prettify Holmake's recursive invocation verbiage


# 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.


# 151eb099 13-Jan-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Move holmake-recursion code into Holmake.sml

The move of this code into separate Holmake_tools.sml happened in
order to try to share code between MoscowML and PolyML
implementations. I imagined then that I would have to have the
top-level functions trapped in language-specific implementations, but
that various leaf-level things could be reused. I noticed that the
recursion logic governing the way INCLUDES specs were followed could
be stripped out of Holmake and so moved maybe_recurse into
Holmake_tools.

But now, the much more sensible scheme whereby only specific leaves in
the code-tree are language specific is used, and so the quite
high-level recursion stuff can come back into Holmake.sml.


# 7c949327 04-Jan-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Fix Holmake bug to do with --no_prereqs

Bug is identified in previous commit (and in accompanying test-cases).
It comes down to the fact that even with --no_prereqs specified,
Holmake needs to scan ancestor directories in order to get
dependencies correctly recorded in generated files, particularly
Theory.uo files.


# d56fd8b3 22-Aug-2017 Michael Norrish <Michael.Norrish@nicta.com.au>

Update Holmake to cope with Theory.dat files

No tests specific to that feature yet.

Still also need to update for Moscow ML.


# 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


# f0590a52 29-Jan-2017 Michael Norrish <Michael.Norrish@nicta.com.au>

Implement build cleanForReloc

This sub-command deletes heaps, .uo and .ui files, at least under
Poly/ML. These are the files that embody absolute path values, and
which will cause breakages if a source tree gets moved. The Theory.sig
and Theory.sml files don't contain those paths, so they don't need to
be deleted. Given that its their generation that takes all the time,
we may be able to regenerate an installation by only doing the
relatively quick generation of heaps, .uo and .ui files.


# 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.


# e765035a 05-Sep-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Move Holmake & test verdicts one character left

This stops the rightmost character (the 'K' in 'OK', for example) from
being blanked by the clear-to-end-of-line formatting that gets output
after Holmake verdicts (as per 6828af9a21). If your screen is wider than
80 columns, you don't see this effect.


# 7098f9c7 05-Jun-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Handle opentheory intermediate leftovers better

In particular, the parallel process for building .art files creates an
intermediate thyname.artScript.sml file that shouldn't be regarded as a
normal script file. (Indeed, it can't work as a normal script file
because of the presence of the full-stop in the theory name, so there's
a warning emitted for other occurrences of this if seen.)

These intermediates can be cleaned by Holmake as well if they're
found. (Normal execution of Holmake will remove these files after
they're used, but if the build is interrupted for some reason, they get
left behind.)


# ac18d770 10-May-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Make check_distrib fn visible in Holmake_tools API


# 186637a4 28-Apr-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Emit CHEAT when non-qof tactic fails; get nice colours

By having the tactic cheat, and the non-qof handling of prove both emit
the string "CHEAT" as part of their behaviour, Holmake's multibuild can
give you a CHEATED verdict on scripts that do either. Strictly,
speaking the tag attached to non-qof failure is not cheat, but I don't
think that's really important here.


# 20eb6cc0 21-Apr-2016 Michael Norrish <michael.norrish@nicta.com.au>

Make parallel Holmake's output prettier

When a process fails, a chunk of its output up to the failure point is
output to the main screen. Also, a process that is killed because of a
general desire to give up (a failure elsewhere and no -k option, say),
now gets a red M-KILLED ("monitor killed") report.


# 1c326356 20-Apr-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Make multibuild output prettier


# bf1164c0 15-Apr-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Make Holmake less chatty by default

Enable old level of chattiness with -v or --verbose command line option.


# 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.


# 4121aab1 13-Apr-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Start to implement building from dependency graph

This code is as yet unconnected to any execution, and is attempting to
replicate the behaviour that we have at the moment (corresponding to
what will eventually be -j 1).

Slightly adjust some types along the way, including changing a
bool*bool*string tuple into a record that identifies what the bools are.


# 7b43df0a 30-Mar-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Remove diffs between poly and mosml Holmake impls

Next step is to actually remove as much as possible of the
tools-poly/Holmake directory.


# 60a69fd8 30-Mar-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Pass more info to the impl-specific BuildCommand

In particular, pass
- the full Holmakefile-derived envlist function (which turns $(...)
references into string lists);
- output functions (warn, die, etc)
- quit_on_failure, which is derived from the Holmakefile and core
command-line options


# 4aa9adb2 28-Mar-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Purge Holmake.sml of much Moscow ML specific code

The Moscow ML stuff has moved into mosml/BuildCommand etc

Progress with github issue #77


# c0d1d17f 28-Mar-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Cleanup more Holmake code

This is in pursuit of more unification between Moscow ML and Poly/ML
implementations (github issue #77).


# fdc5cae7 07-Mar-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Make KERNELID variable available to Holmake

This is the value of the kernel option that was passed to build when the
system was built. The build program stores it in the filesystem in a
"canonical location", and this file is read by Holmake when it starts
up.


# 51de37ac 01-Nov-2015 Ramana Kumar <ramana@member.fsf.org>

Initial stab at making Holmake aware of article files (#310)

It builds, and Holmake's normal behaviour appears not to have broken.
But the new functionality is not at all tested yet.


# 227f4708 22-Feb-2015 Michael Norrish <michael.norrish@nicta.com.au>

More progress with Holmake and recursive dependencies

Both depchain selftests pass now on both Poly and Moscow ML.

The treatment of relative and absolute directories is more careful,
for which see the hmdir structure within Holmake_tools. This stuff is
really only as complicated as it is for cosmetic reasons: the various
messages printed to the user try to avoid absolute paths for as long
as possible. However, more/most/all internal uses will now be with
absolute paths, which should help.


# a72d68fc 16-Feb-2015 Michael Norrish <michael.norrish@nicta.com.au>

Most of a fix for recursive holdep problem.

See test-case in Holmake/tests/depchain1

Test-case still not re-enabled as I don't think this quite works for
Moscow ML yet.

Some incidental progress with sharing more code between Moscow ML and
Poly/ML (github issue #77).


# 07480c25 12-Feb-2015 Michael Norrish <michael.norrish@nicta.com.au>

Slightly adjust Holmake's internal interface.

Just a refactoring to make the recursive calls return a record-option
rather a straight set. Intention is to next make the return value a
bigger record so that it can return a list of extra includes, thereby
allowing a fix for issue illustrated by the holdep test-case under
Holmake/tests.


# 4522c28a 02-Feb-2015 Michael Norrish <michael.norrish@nicta.com.au>

runholdep function moves to Holmake_tools (Poly/ML Holmake affected)

In the latter module, it can be used in the Poly/ML implementation.
This is progress with github issue #77

The Poly/ML implementation now fails the regression test in

tools/Holmake/tests/depchain1/dir3

so comment out that test from the build sequence temporarily. I
believe there will be a Holmake failure in machine-code until the
behaviour is properly fixed. I hope selftest 2 will go through
correctly.

Holmake's output also changes slightly because I've been more
consistent about using the built-in 'info' function instead of print.


# 91e46ef1 21-Oct-2014 Michael Norrish <michael.norrish@nicta.com.au>

Move generate_all_plausible_targets into common Holmake_tools.

Progress with #77


# 732be988 24-Feb-2014 Michael Norrish <michael.norrish@nicta.com.au>

Share more code between mosml and poly Holmake.

Work on github issue #77


# e63d42fc 17-Jul-2013 Michael Norrish <michael.norrish@nicta.com.au>

Implement recursive cleaning for Holmake.

Closes #125; not extensively tested.


# f5f11785 15-Aug-2012 Michael Norrish <michael.norrish@nicta.com.au>

Get recursive Holmake to handle absolute paths in INCLUDES.

This was broken by 44cef4623, handling #64.


# 44cef462 14-Aug-2012 Michael Norrish <michael.norrish@nicta.com.au>

Improve Holmake's messages about recursive invocation.

Closes #64.

Also helps with #77 because the code controlling the recursive
invocations is now in Holmake_tools rather than in both versions of
Holmake.sml.


# 239b7fad 22-Mar-2011 Michael Norrish <Michael.Norrish@nicta.com.au>

Move more code (including directory cleaning) into common Holmake_tools.


# cadb3c61 22-Mar-2011 Michael Norrish <Michael.Norrish@nicta.com.au>

Move Holmake's structured file type into shared Holmake_tools module.


# d7631584 09-May-2010 Michael Norrish <Michael.Norrish@nicta.com.au>

New Holmake feature: check to see if it should be being used as builder.

If, as I do, you have multiple HOL installations on the same machine,
it can be a pain to remember to build things with the correct Holmake.
On the other hand, it's certainly convenient having a Holmake in one's
PATH. So, this change gets Holmake to determine if it should be the
Holmake being used, and if it thinks another Holmake should be being
used instead, that other Holmake gets called out to instead. This
"calling out" is done through Systeml.exec, so can even be across
Poly/ML-mosml boundaries.

There are two ways in which a Holmake can decide determine the correct
Holmake to be used. If it sees a .HOLMK/lastmaker file containing a
path, then this is used. This file is written to when a Holmake does
decide it's the rightful make executable. Secondly, if Holmake
determines (by jumping up through the file-system) that it is being
called inside a HOL installation already containing a bin/Holmake,
then that is taken to be correct.

When a second Holmake is called as part of this process, it also gets
passed the --nolmbc flag ("no last made by check") to stop it going
through the whole process all over again.