UPDATE (25 Jul 2008):
Now require users to do their configuration from the root HOL
directory (updating the documentation to reflect this).  The reason is
to enable both
   mosml < tools/smart-configure.sml
   poly < tools/smart-configure.sml
The contents of tools/smart-configure.sml now figures out which
interpreter is being run (by relying on a known mosml bug), and then
runs the real configuration script for the given ML system.

This file explains how to rebuild HOL4 in the directory HOL on my
Linux machine at Cambridge. HOL sould contain:

bin	    doc       install.txt  scheme  std.prelude
COPYRIGHT   examples  Manual	   sigobj  tools
developers  help      README	   src	   tools-poly

To configure and build HOL4 go to the directory HOL and do: cd tools; mosml < smart-configure.sml ; cd ../bin; build -symlink The "-symlink" is needed so that updates to libraries, specifically HolBddLib, see below, can easily be made. N.B. If a rebuild is being done, then in occasional pathological cases you might need to precede the build by "build cleanAll" in HOL/bin --------------------------------------------------------------------- Mike Gordon Updated June 2008