Running HOL on Windows

System requirements:

Unix on Windows

You must have either

• a recent version of Cygwin installed (which probably implies you need to be running Windows Vista or later); or
• the Microsoft Linux subsystem for Windows 10 (see, for example, this Wikipedia page for more on this subsystem)

Poly/ML

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.

Installing HOL:

Follow the standard instructions (see the Tutorial for details). Namely, after installing the source-code from the tar file, in the HOL directory:

           $ 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.

Unicode, UTF-8 and HOL4 on Windows

The trace variable PP.avoid_unicode can be set to true to prevent 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, this trace variable should be set 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. 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.)

---

Using Moscow ML

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 Holmake).

Using Moscow ML may be required if one cannot use Cygwin or the Windows Linux subsystem.

---