Let users pass additional options to hol{,.bare} executables

These are passed through to the underlying buildheap executable. This
might be used to get additional files loaded on startup, as well as to
use the new --mt flag.

Provide quoting/protecting system variant with output collection

Systeml.systeml tries to be smart about quoting command-line arguments
to protect them from the shell. It can be useful to be able to
execute such protected commands and to also capture the output in a
specified file.

Get basic interactive executables to work

Factor out name of special rebuilding-heaps environment variable

The name of this variable is now specified in just one place.

Progress with github issue #105

POLYC + POLY_VERSION now available in Holmakefiles

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

Put POLY_VERSION into Systeml.

This allows code that might be compiled with Moscow ML to also
work (there the POLY_VERSION value will be 0).

Use PolyML.SaveState instead of executable heaps

Interface in terms of "HOLHEAP" declarations in Holmakefiles stays the
same. Implementation uses hierarchical saved states. All command-line
executables should also now be compiled with polyc.

Closes #292

Systeml's mk_xable returns status, not string

It previously used to return the string of the executable version of the
file. On Windows, this makes sense because making things executable
consists of adding the string ".exe", changing the filename. But we
already have the xable_string function for doing this calculation.

Detect availability of polyc at config time

Work towards issue #292

Make copy of portable pointer_eq available in Systeml.

This then allows regexpMatch to be portable too.

Allow user to configure location of dot tool for theory graph building.

The default is /usr/bin/dot, because that’s where it is on my Linux machine. If you need it to be somewhere else, create a config-override or poly-includes.ML file, depending on which ML you’re using.

Make Systeml.sig the same in Moscow ML and Poly builds.

This additional uniformity allows me to delete the
tools-poly/Holmake/Systeml.sig file. This then requires a bunch of
changes to compilation of the early tools which have to point at
tools/Holmake/Systeml.sig rather than the version in
tools-poly/Holmake.

This should fix the configuration errors on MoscowML introduced by
0a0988fc.

Make the hol executable use a directory's HOLHEAP, if given.

This is achieved with a heapname executable that runs before hol
starts, returning the name of the appropriate heap for the current
directory. This determination is made by looking at the local
Holmakefile, if there isn't one, or if it doesn't specify a HOLHEAP
variable, then the usual bin/hol.builder heap is used.

This also works for the hol.noquote executable (though it's hard to
believe anyone uses this).

Use Posix.Process.exec on Poly when not on MacOS.

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.

New find_my_path function figures out where the currently running program is.

Addition of POLY_LDFLAGS_STATIC variable. This variable is used for static linking whereas the recently added POLY_LDFLAGS triggers dynamic linking.

Store (calculated) Poly/ML linker flags into Systeml.

This allows build to read these flags from Systeml, rather than having to
recalculate them.

Put a variable ML_SYSNAME into the Systeml structure recording what ML
implementation is being used.

Realised that putting the quietdec thing into Systeml wouldn't work in
Moscow ML because this code needs compiling and you can't compile
references to the Meta structure. So, I just put it into the
respective prelude files.

Put a toggle_quietdec function into the Systeml structure, allowing a
common interface to be relied on by the emacs mode.

Fix interactive ctrl-c handling in the Poly/ML version.

Improve the building process under Poly/ML.

Streamline the PolyML compatibility support a bit.

PolyML compatibility. See tools-poly/README.