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.
For Kananaskis-10 and earlier, the Moscow ML installer for 2.10 is not compatible with the HOL4 installer; you must use the older installer for Moscow 2.01.
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.)
A new trace variable PP.avoid_unicode is set to true (strictly, 1) on Windows by default.
This prevents the appearance of “gibberish” in the standard “MS-DOS” command.com shell.
If you are running within emacs or some other setting where UTF-8 characters will work, you can set this trace variable to 0:
set_trace "PP.avoid_unicode" 0;
to get back the nice Unicode output. Note that Unicode input in UTF-8 will continue to work regardless. (See also 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/DELTHISminisat.exe to src/HolSat/sat_solvers/minisat/minisat.exe.