Try to find dot in user's PATH during configuration

If it is not found, say little about its absence on help-graph build
time.

Make it possible to stop using MLTON; make it clear if it is used

Use mlton to compile build and Holmake if it is installed

This is based on the theory that it won't generate strange errors on
wait as some versions of Poly/ML still seem prone to. It is probably
also quicker. (The script files themselves are still executing Poly/ML
so it's an improvement at the margins only.)

POLYC + POLY_VERSION now available in Holmakefiles

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

Detect availability of polyc at config time

Work towards issue #292

DOT_PATH can now be overridden with Poly/ML

Failure to find an executable dot tool at the end of the build process
also produces a more helpful error/warning message.

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.

Exit with non-zero code if configuration fails under Poly/ML.

Issue is that you can get a Fail exception when a call to ‘use’ fails,
but this doesn’t translate into a non-zero exit code when the Poly/ML
process exits, and this means that the regression build thinks that
configuration has succeeded, and then the build keeps going. Which is
bad. This (and the fact that Poly/ML 5.20 can’t compile
tools-poly/configure.sml) explains the regressions (with commit
7c7739a8c and earlier).

Fix configuration on PolyML

Remove suggestion that Poly/ML builds can alter dynlib_available.

This variable can only be true in Moscow ML builds.

Polish the user experience in Poly's smart-configure.

In particular, if the overrides file exists (and provides sensible values),
don't tell the user to write it when the automatic setting detection fails.
In fact, if the overrides file exists and gives a value for something,
don't even attempt to determine that value automatically.

One slight change though is that you can now only override the poly
and polymllibdir values.

Thanks to Tjark for the report.

Provide better advice on writing config override files when errors occur.

(Suggested by Magnus.)

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Use OS.FileSys.fullPath to get a proper path to a file, in particular
one that is uncontaminated by symbolic links.

Get poly HOL's configure to guess the likely location of the lib
files. This should remove the need to maintain a
tools-poly/poly-includes.ML file except in weird circumstances.

Modify configuration to use PATH examination to find the poly
executable, and to allow the configuration to be done from the root
hol directory, and not just tools-poly.

A little more polish on the PolyML build.

PolyML compatibility. See tools-poly/README.