Make KERNELID var get its proper value in Holmake

Issue was that Poly/ML evaluates many things at compile time rather than
run-time.

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

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.

POLYC + POLY_VERSION now available in Holmakefiles

Also change POLYC from string option to string in Systeml (and "" in
Moscow ML environments).

Export Systeml's CC value to Holmake.

Solves a problem when some (shell) environments may not have CC
defined.

if[n]def in Holmakefiles wasn’t treating non-null environment vars as defined.

Make sure HOL variables in 'base' environment include POLY.

Implement ifdef/ifndef conditional directives for Holmake. (Progress for #11.)

For the moment, only ifdef and ifndef are supported. It'd be good to
also do ifeq and ifneq. The behaviour should be as per GNU make.

In other words, if your Holmakefile looks like

ifdef POLY
mytarget: mydeps
command1
command2
endif

then the delimited text will only be seen if the POLY variable has a
non-empty value (which will happen if you're running Poly/ML HOL, or
if you've got an environment variable called POLY).

You can also use 'else' to do things if the head condition is false.
Thus:

ifdef POLY
text...
else
alternative text
endif

Finally, these directives can be nested, and you can chain else-if on
the same line:

ifdef POLY
text...
else ifdef FOOBAR
text...
else
text...
endif

Get mosml Holmake to build with new Holmake_types.

Revised Holmake_types implementation.

Intention is to allow correct interleaving of variable definition and rule
specification.

Use String.concatWith rather than bespoke 'commafy'.

Alter $(MV) on Windows to use move rather than rename.

move with a /y flag will replace existing files; rename will
never do so. This causes a problem in src/TeX where the
holindex-grm.sig file needs to be renamed to
holindex-grm-sig.sml. Once this had been done once,
subsequent build attempts started to fail.

Allow Holmake variable references to contain variable references themselves.

This can be useful. Document this extension, including an example.

Add OS variable to those exported by Holmake; tidy up Description of these vars.

Correct tokenising of makefile function arguments (ignore nested commas).

Augment base Holmake environment with ML_SYSNAME, MLLEX and MLYACC.

Also move code implementing this into shared Holmake_types module.

Start to implement the Basis 97 extensions that Moscow ML hasn't got
in order to force our codebase to get up-to-date. It should also
mean less bodging around for the Poly/ML code. I haven't checked that
my changes to tools-poly/poly/poly-init2.ML have done all that is
required yet. Feel free to fix problems arising there (I hope it will
just be a matter of deleting things).

Introduce new makefile function called dprot for quoting file-names that
may include spaces and which need to be mentioned as dependencies in
Holmakefiles. Document its existence in the Description. Tighten up
some of the text-processing done inside Holmakefiles.

Handle windows style \r\n newlines more carefully. This now allows
Holmake to cope with the Holmakefile in examples/sunrise/src which
has such endings. (Not that it should; CVS is supposed to normalise these
things, but that's another story.)

Fix a bug found by Joe whereby the special .PHONY target gets treated as
something that Holmake might build by default.

Failing a catastrophic bug, this should be my last Holmake check-in for a
while. This fixes the behaviour when a Holmakefile contains multiple
rules for the same target. If there is more than one rule with
accompanying commands, then the later rule takes precedence and earlier
command-accompanied rules are ignored. However, it is always OK to have
rules that specify just dependencies. These dependencies are merged together
and added to the last command-accompanied rule, if there is one, or
are merged together and left as they are (without commands).

Implement patsubst internal function, and shift some useful code into
a separate file.

Edging ever closer to a complete re-implementation of GNU make with
HOL-shaped knobs on. :-) Added subst and if built-in function. I
actually need the former for my C stuff (believe it or not).
Still to do: handle multiple instances of the same target correctly.

Fairly drastic change to the way in which Holmake interprets Holmakefiles.
These can now contain arbitrary variable definitions and references, just
like in normal make-files. Rules can also use have multiple targets, and
the special variables $< and $@ have the appropriate meaning. These are
Feature Requests 597666 and 597668. I will attempt to document the changes
more thoroughly in the DESCRIPTION.

Can now use $(VARNAME) references anywhere inside a Holmakefile. At the
moment, may only refer to two known variables HOLDIR and SIGOBJ, but the
intention is to allow users to define their own variables. This is useful
for constructing rules that depend on the mkword executable, which lives
within the source tree, and for referring to theories that live in
SIGOBJ.

Implemented a new feature for Holmake. You can specify "EXTRA_CLEANS" at
the head of a Holmakefile, and these files will be removed along with the
obvious ones when you do a Holmake clean (or cleanAll). The
help/src and quote-filter Holmakefiles now take advantage of this.

Slew of changes, giving Holmake the ability to read makefiles that
override its usual techniques for building files. This is really done
for the benefit of Kananaskis where the kernel has to built in a
particular way, but should be more generally useful. It is the
responsibility of the configuration script to either give Holmake the
ability to use overlays or not. This is done by setting up the
DEFAULT_OVERLAY variable appropriately.