Let ANSI colouring happen on screen terminals

screen is documented as explicitly supporting these codes

Fix bug where Holmake would die with Subscript exception

Issue was terminal environments where `stty size` and/or `tput
cols` (these are Unix shell commands) would return suggesting that the
width of the terminal window was 0. Fix the getWidth function to not
allow this.

Preserve a diagnostic message in poly/BuildCommand.sml that was of
some help in tracking this down.

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

Holmake: Handle / occurring after an 'open' more gracefully

Closes #518

Reduce and prettify Holmake's recursive invocation verbiage

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.

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.

Canonicalise directory names better in Holmake

Previous behaviour saw it unnecessarily distinguishing foo//bar and
foo/bar (when the former was coming from something like
$(MAKEVAR)/bar, with MAKEVAR set to foo/).

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.

Update Holmake to cope with Theory.dat files

No tests specific to that feature yet.

Still also need to update for Moscow ML.

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

First hack at providing mlton Holmake

Make a clean-for-reloc only delete HOL heaps

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.

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.

Stop Holmake generating default targets from *Theory.{sig,sml}

If a directory has a fooScript.sml file, then fooTheory.uo will still
be generated as a default target, so there's no need to generate
fooTheory.uo from fooTheory.sml. If fooTheory.sml is stale or
orphaned (perhaps its script file has been moved to another
directory), attempting to build in this directory will just cause an
annoying Holmake error. If fooScript.sml is generated from a special
rule in a Holmakefile, then that Holmakefile can equally take
responsibility for making fooTheory.uo a target.

This is part of an approach to github issue #295.

The second part of this would be automatically remove the
stale/orphaned theory files.

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.

Clean all generated .art files (raw or processed)

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

Make check_distrib fn visible in Holmake_tools API

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.

Clean out .hollogs at the same time as .HOLMK.

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.

Make multibuild output prettier

Make Holmake less chatty by default

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

Replace 'print' with Holmake's output functions

Get "build from graph" Holmake to compile

Poly/ML version fails miserably at boolScript hurdle however.

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.

Remove diffs between poly and mosml Holmake impls

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

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

Purge Holmake.sml of much Moscow ML specific code

The Moscow ML stuff has moved into mosml/BuildCommand etc

Progress with github issue #77

Cleanup more Holmake code

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

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.

Simplify build output by not printing out the full path of "Holmake".

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.

Use printf instead of echo for added portability

use /bin/sh instead of /bin/bash (which is not available on all UNIX systems)

also, use cc instead of gcc (no need to compile HOL4 with gcc)

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.

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

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.

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.

Empty command-line Holmake only builds first target in Holmakefile.

If there is no Holmakefile, or if there is a Holmakefile with no
targets, then the old behaviour of attempting to build everything
possible happens.

Documented in release notes and DESCRIPTION.

Many of the distribution's Holmakefiles were harmed in the creation of
this commit, but, for the reasons given in the release notes, I don't
think this should happen that often for typical user developments.

Closes #175

Move generate_all_plausible_targets into common Holmake_tools.

Progress with #77

Share more code between mosml and poly Holmake.

Work on github issue #77

Put information about Holmake's current directory into terminal title

This relies on magic escape sequences supported by xterm,
gnome-terminal and MacOS's Terminal.app. Nothing extra is done under
Windows.

Implement recursive cleaning for Holmake.

Closes #125; not extensively tested.

Improve diagnostic output when Holmake switches to execute another Holmake.

Holmake now explains why it is switching: either because it is in
another Holmake’s distribution, or because another Holmake was used to
build this directory last time.

Get recursive Holmake to handle absolute paths in INCLUDES.

This was broken by 44cef4623, handling #64.

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.

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

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

Adjust order in which 'last-made-by analysis' considers options.

In particular, if running Holmake inside a HOL distribution, this will take
precedence over a last-made-by file. I.e., the 'local' Holmake will be used
rather than something appearing in a last-made-by file.

Update use of exec to reflect its proper practice (name of executable in args).

When you call execv (the Unix system call), you pass the thing to run as well
as an argv. Tradition has that the first thing in argv is the name of the
thing being executed (in shell scripts, this is bash, for example). This change
makes our use of exec match this.

Make call to CommandLine.name() happen inside Holmake rather than the compiler.

If you are compiling

val execname = CommandLine.name()

with this phrase at the top-level, then it will get "poly" (or some
variant thereof). If arrange to have the code above called first
within an executable generated from compilation, it will get the right
name (i.e., "Holmake" in this setting).

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.