on github

Windows Installer for HOL

System requirements:

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.

Using the installer:


The self-installing executable was created with the freely available, and highly recommended, InnoSetup tool.

Unicode, UTF-8 and HOL4 on Windows

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

Use of minisat SAT solver

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.

Download the installer