The HOL interactive theorem prover is a proof assistant for higher-order logic: a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems (users may have to prove the hard theorems themselves!) An oracle mechanism gives access to external programs such as SMT and BDD engines. HOL is particularly suitable as a platform for implementing combinations of deduction, execution and property checking.
HOL is free software, released under the Modified (3-clause) BSD licence.
New developers are welcome.
During the last 30 years there have been several widely used versions of the HOL system:
HOL is developed by people at (among other places):
The first thing you need to do is check out a copy of the HOL repository from GitHub. This is easy! There’s just one step:
git clone https://github.com/HOL-Theorem-Prover/HOL.git
Alternatively, if you’re happy to work with GitHub yourself, you can always create a fork of our code there. This is a good way to then be in a position to make your own contributions to HOL.
Cloning will download a complete copy of all the current sources and install them in a directory called
You will now have a copy of the sources and should be able to build hol as follows:
sml-system < tools/smart-configure.sml
sml-system is one of
poly; we strongly recommend Poly/ML).
The really nice thing about this copy of the sources is that if there is a check-in changing the sources, you can automatically patch your copy of the sources to reflect this by typing
git pull in the HOL directory.
git status command will tell you if you have modified any of the files in the distribution.
You can tell if there’s been a check-in to the main git repository by subscribing to the hol-checkins mailing list. You can check the archives for the list (and see what you might be letting yourself in for) by following the link on the list-info page.To update an existing install you should perform an additional clean operation:
sml-system < tools/smart-configure.sml
To switch from the development version to a released version of the sources, simply check out the branch corresponding to the desired version in your copy of the HOL repository.
git checkout kananaskis-14
Alternatively, you can download a released version of the sources.
HOL can also be installed under Windows.
Starting from scratch, it takes on average about a month to become comfortable using HOL. Many people learn from the tutorials and guidebooks mentioned below, together with support from the community.
One should first learn to interact with HOL4. For Emacs users, there is an 11-page guide to HOL interaction and basic proof using Emacs. There is also a page with more complete documentation of the Emacs mode. Vim users might like to consult the documentation for the Vim plugin.
In spring 2017 a course for advanced master students about HOL was given at KTH. The course aimed at the needs of the PROSPER project and tried to provide some hands-on experience with HOL. The slides (printer friendly version, LaTeX sources) as well as the exercise sheets are available. More information can be found on the course webpage.
There is also a work-in-progress Guidebook which aims to present a gentle but comprehensive account of the system.
There is also an FAQ that can help troubleshooting.
The Description manual provides a detailed description of all of HOL's facilities. This includes not only high-level libraries, but also some of the core ML functions in the HOL API.
Most HOL users use the online reference page to look up documentation while they work. Note that a local copy of this page is built when you install HOL. This page is located at
HOL is root of your HOL installation. The reference also exists as a PDF document.
The Logic manual (also available in Italian) provides a detailed mathematical description of higher-order logic, as it is implemented in HOL. In particular, it demonstrates a model for the logic and its definitional principles in ZFC set theory.
hol-infomailing list is for discussion, questions and announcements related to the HOL System (HOL4 and HOL Light discussions are both welcome) [send a message | subscribe | archives at (mail-archive.com; SourceForge) ]
#holchannel in its Slack
#holIRC channel on freenode provides an alternative chatroom to Slack
Bug reports: Please use the GitHub issue tracker to report problems, and make feature suggestions.
As git is a distributed version control system, it is easy for you to make your own local commits to your copy of the repository. If you’d additionally like to have those commits incorporated into the official repository, you need to issue what is known as a “pull request”. You will first need to push your version of the repository onto GitHub (which you may already have set up if you forked our code there). Then you follow the process described here (GitHub documentation). Developers might like to subscribe to the developers' mailing list in addition to the hol-info users' list.