Give build an --mt flag as well; it's passed on to Holmake

Implement logging kernel on top of stdknl terms

The code from logging-kernel/Thm.{sig,sml} lives on but the other
stuff (duplicates of code from experimental-kernel) can be deleted.

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.

Reimplement build cleanForReloc using rebuild-excludes file

Also correct name of numheap in the latter

Update build help output regarding --nograph option

See e.g., ccf751b703e333fb71513690430a2633e1536df5

Fix build to correctly report seq file containing bad directory.

Also adjust error message which talks of skipping bad directories but
then dies (see 217b05b8cd2 for the change from "skip" to "die").

Give build --dbg flag that gets passed on to Holmake

Complete basic Poly implementation of TheoryIO (separate dat files)

Still to tweak Holmake and to make sure it all works on Moscow ML

Use _Theory.dat for loading theory data into _Theory.sml

Remove more things when cleaning for relocation

Make cleanForReloc remove platform-specific files in src/HolSat/

Complete relocation-build feature

Closes #105

To be explicit, after building HOL in one directory one can then

$ bin/build cleanForReloc
$ cd ..
$ mv HOL somewhere_else
$ cd somewhere_else
$ poly < tools/smart-configure.sml
$ bin/build --relocbuild

The last step (the "relocation" build) takes less than a minute and
results in a functional system that is housed in a different location.

Next step on this branch of work is to provide tools allowing other
developments (those not under HOLDIR) to be moved in a similar way.

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.

Remove a superfluous definition of "mem" in buildutils

Make more build-related cleanups

Consistently use dehyphenated version of name to stand as
kernelid (i.e., "expk", "stdknl", "otknl", rather than anything with
leading hyphens). This requires change to Holmakefiles that wanted to
build OpenTheory articles when being executed under otknl.

Also make

build cleanAll

clean in all directories, not just those belonging to stdknl.

Incorporate new c/line option-handling into build

The build in relocation option doesn't do anything at the moment.

Implement check to stop build running in wrong dir

Build "belongs" to a particular HOL directory, and it can be annoying to
mistakenly run one (perhaps because it is in your PATH) thinking that it
will build in one's current directory, but actually end up building some
other instance of HOL. Stop that scenario by having build detect if it's
being run somewhere within a HOL directory, and then aborting if it
isn't the build associated with that directory.

Get build to honour selftest commandline argument

This behaviour was broken by 80833d8884

Make build's warnings all come prepended with ***

Implement -j option for build

This is passed onto the Holmake calls that build makes. It is also made
persistent from invocation to invocation, just as sequence, kernel and
theory-graph choices are.

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

Use bold text to make build output prettier

Make KERNELID var get its proper value in Holmake

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

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.

Remove some unused code in build

Update fail-to-find-dot message

We no longer have hol.builder0 but have instead hol.state0 as the thing
that is built as part of src/proofman's action.

Tweak "couldn't build thy graph" message in build

Remove more invocations of poly in favour of POLYC

In the developers directory and the building of the help system's tools.

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

Get build to check for need to rebuild Holmake

Previous behaviour was to look for things being fresher than the build
executable, but if changes are made to the Holmake sources, then that
executable should also be rebuilt.

Thanks to Jeremy Dawson for bringing the issue to my attention.

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.

fix read_buildsequence for kernelnames

the comment in build-sequence says the kernel names are "otknl",
"stdknl" and "expk", but in the code they have a hyphen at the front. I
guess this isn't used for anything apart from otknl so hadn't been
tested much.

Correct treatment of minisat.exe in Windows build (issue #92)

Don't install minisat when building on Windows.

This is a shotgun approach to issue #92.

Implement #includes for build sequence files.

Closes #14

Fix build to use new Systeml.DOT_PATH API.

Use POSIX facilities so build alters Holmake’s environment under Poly.

This can’t be done under Moscow ML because it doesn’t implement the
POSIX structure. This is used so that the invocations of Holmake can
pick up a SELFTESTLEVEL environment variable.

More refactoring in build.sml code.

This moves shared code into buildutils and makes progress with #77.

Theory graph automatically built as part of bin/build.

Closes #84.

Move build's usage message into separate text file.

This message is data and it's annoying having to recompile build just
to change the message.

Improve bin/build's usage message.

Closes #88.

This is also progress with #84 inasmuch as it mentions the new -graph
and -nograph options.

Recognise -graph and -nograph options to build.

These options are completely ignored at the moment, but they are
stored in the "last build options" file so that they don't need to be
repeated.

Progress with #84

Fix #83: -h/-?/-help/--help always bring up build option help.

Refactor more code from 2 build.sml files into common buildutils.

Functions moved:
build_dir
clean_sigobj
check_against
SYSTEML
transfer_file

Progress with #77 and #83.

Add -otknl option to bin/build for logging-kernel

Allow build-sequence paths to be filtered by which kernel is in use,
using (kernelname) akin to the existing [mlsys] filter.

Remove tools/logging-build-sequence.

This makes commits like 84c602e312 unnecessary as future changes are
made to the build sequence.

Make some warnings in build fatal errors instead.

In particular, warnings related to faults in the build-sequence now
get to be fatal errors so that the regression machinery will catch
these problems immediately.

Get mosml Holmake to build with new Holmake_types.

Document bin/build IO failure better. Fixes #4

Slightly tweak build's help message.

Make build handle 'cleaning' rather than calling out to Holmake.

This makes it considerably faster under Poly/ML, and also means that it
can properly recursively clean following INCLUDES and PRE_INCLUDES links
in Holmakefiles (important in the examples).

Allow Moscow ML build to happen using (as yet unreleased) v2.10.

Basic strategy is to make adoption of basis 2002 even more
thorough. In particular, the Timer structure is now as per
the 2002 Basis.

It is possible to detect that one is working with Moscow ML 2.10 or
later by checking the Holmakefile variable $(HAVE_BASIS2002), which is
set (to value "1") when in 2.10 or later. It is unset elsewhere. See
an example of its use in help/src-sml/Holmakefile.

Move duplicated functionality into common buildutils module.

bin/build's internal warn function now adds a newline to its argument.

bin/build uses earlier (cached) options when not explicitly overridden.

In particular, kernel specifications (-expk, and the new -stdknl), and
build-sequence file specifications are cached in
tools/lastbuildoptions so that one can subsequently do just bin/build
to build again with those same options. To override a -seq foo
option, you can use the -fullbuild option.

Other options (-symlink, -selftest) are not cached.

Drop trailing whitespace on lines in the build-sequence.

Directories before kernel in the sequence now appear in the build-sequence file.

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!

Fixes to ensure that Poly/ML build will build the hol.builder heaps
even when not called from HOLDIR.

Further adjust buildutils and tools-poly/build.sml so that it can use
the same build-sequence file as the Moscow ML implementation. The
extra build targets that poly uses are prefixed with [poly] in this
file, and the Moscow ML build will simply ignore these.

Make buildutils really work under Poly/ML, and set up its building of
build.sml to use that module.

Start to factor out some code from build.sml that can be built in both
Moscow ML and Poly/ML so that it can then be shared between both
implementations.