You must have MoscowML 2.01 installed
before you running the installer. In particular, this
means that the environment variables PATH and
MOSMLLIB must be correctly set. Further, these
variables must be Windows environment variables (set through
the Control Panel). It is not enough to have variables set just
for Cygwin shells.
The self-extracting installer for Moscow ML will normally set environment variables correctly as part of its installation process.
When Moscow ML is installed, you can install HOL by running the installer executable. It will prompt you for the directory to install in.
Note that both the Moscow ML and HOL installers require the user to have administrative privileges.
At the very end of the process, a DOS-like window will appear, and the system will attempt to configure itself. This process also involves the creation of many help files, and can take a little while. If this window disappears almost instantly or with an error message, you probably haven’t installed Moscow ML correctly. (See here for more details.)
If you run HOL4 in the standard “MS-DOS” command.com shell, or don’t have good enough fonts, lots of HOL output will look like gibberish. In this situation you will probably want to turn Unicode printing off when you run HOL. Use
set_trace "Unicode" 0;
to do this. (See this FAQ question.)
On some Windows systems, the automatic use of the minisat solver causes serious slowdowns as hol starts up.
For this reason, it has been disabled by default in the self-installing executable.
It can be re-enabled by renaming the file src/HolSat/sat_solvers/minisat/minisat.tmp.exe to src/HolSat/sat_solvers/minisat/minisat.exe.