Make Holmake monitor show times instead of just !!! on slow builds

I have just three characters to show times, so the precision of the
times moves to minutes and then hours.

Closes #568

Polish some code (semantic no-op) in Holmake/MB_Monitor

Removes somewhat inscrutable integer constants

Delete some unused code in Holmake/MB_Monitor.sml

Slight tweak monitor output for tty-multiprocess scenario

In particular, text at the very right-most edge can be obscured by the
cursor (depends on your style of cursor of course), so this commit
ensures that there is always a right-most space. This fixes the
previous situation for single processes (which output successive lines
of their output to the screen) when that didn't happen.

Hopefully finalising issue #526

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

Report more information about why a sub-process hasn't succeeded

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

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.

Ensure ANSI CLR_EOL code doesn't go to non-ttys

Without this, 6828af9a21 caused a regression

Make final tag lines prettier when running -j n>4

Running something like Holmake -j8 works OK on a terminal with lots of
columns except that verdict lines used to retain junk text off to the
right of the OK. This can be fixed by using ANSI codes to clear to the
end of the line when printing the final "OK" (or "FAILED" etc).

Clear to EOL when printing 1 status in Holmake

Also insert an extra space between output string and status, which gets
to be up to 3 characters, and thereby be immediately adjacent to a long
output.

Flush Holmake-monitor output to .hollog file

This should help if you are watching a .hollog file with tail -f (or
analog).

Correct spacing of stalling status strings

Fix last monitor change (86a81e78) to use LargeInt

See also earlier 6ac06ad3

Make stalling status string be elapsed time

Colour larger numbers, and if it should ever get longer than 999
seconds, it switches to red !!! to save the formatting.

Allow monitors to kill over-stalled processes

API allows for it, but no way to set a non-NONE value so far.

Display stalling info in one-line Holmake statuses

If there is text scrolling past, then it's clear that something is
happening (and what it is), but if the process stalls, one only used to
see the last line of text. Now, that line of text will pick up the
stall-indicators (up to 3 red exclamation marks) if the underlying
process does nothing for a while.

Get poly-monitoring to spot use of cheating prove

In particular, Holmake builds that weren't --qof were not spotting
cheated calls to prove if the resulting theorem wasn't being used
anywhere.

With test-case

Improve feedback for Holmake.

Theorems proved with `fast_proof` are now regarded as cheated. The use of other oracle theorems is identified, though not marked as cheating.

Patch glitch in Holmake output.

The "usepfx" flag is no longer set when `CLINE_OPTIONS = -j1` appears in the Holmakefile. It will only be set when `-j1` is in the actual command line.

This avoids lines that is too long (due to `Holmake: ` being printed) when recursing into a directory that doesn't have `CLINE_OPTIONS = -j1` in it's Holmakefile.

I suspect `Holmake: ` is not printing when recursing into a directory that does have `CLINE_OPTIONS = -j1`, but this wouldn't result in lines that are too long.

Move monitoring code out of multibuild

This separates fancy, possibly ANSI-based, monitoring output from the
logic of running builds over dependency graphs.