Windows NT, Windows 2000, Windows XP, Windows Vista, or Windows 7. We assume Windows 8 will work as well. In addition to the space required to store the installer executable (35MB), you will need approximately 300 MB of disk-space.
MOSMLLIBmust 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.
The self-installing executable was created with the freely available, and highly recommended, InnoSetup tool.
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”
If you are running within
emacs or some other setting where UTF-8 characters will work, you can set this trace variable to
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