---------------------------------------------------------------------- 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 and 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