You must have either
You must also have Poly/ML.
This must have been installed from sources, and within a Unix shell so that
poly believes itself to be running on Unix rather than on Windows.
If you can type
poly at a shell-prompt and have it start up the Poly/ML read-eval-print loop, you are good to go.
Follow the standard instructions (see the Tutorial for details).
Namely, after installing the source-code from the
tar file, in the
$ poly < tools/smart-configure.sml $ bin/build
The output of the configure script should indicate that the system believes itself to be on a Unix system.
The trace variable
PP.avoid_unicode can be set to true
to prevent 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, this trace variable should be set 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.
Moreover, as the installation instructions above should make HOL believe it is on a Unix system, this variable will be set to
0 by default.
(See also this FAQ question.)
It is possible to build HOL4 using Moscow ML in a standard Windows console setting (i.e., without emulating Unix).
This is not recommended: Moscow ML runs many times slower than Poly/ML, and lacks libraries that make the Poly/ML version of HOL4 much more fully-featured (e.g., Moscow ML HOL does not support concurrent builds with
Using Moscow ML may be required if one cannot use Cygwin or the Windows Linux subsystem.