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.
Other HOLs are described elsewhere.
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:
The current version, and successor to those above, is HOL4. Its development was partly supported by the PROSPER project. HOL4 is based on HOL98 and incorporates ideas and tools from HOL Light.
HOL is developed by people at (among other places):
![[ANU]](images/cropped-anu-logo.png){kind=logo}
![[Chalmers]](images/chalmers.png)
We would also like to acknowledge the support of Sourceforge (for file downloads and mailing lists), and GitHub (for our code repository and issue tracker).
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.gitAlternatively, 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 HOL.
You will now have a copy of the sources and should be able to build hol as follows:
sml-system < tools/smart-configure.smlbin/build
(where sml-system is one of mosml or 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.
Also, the 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.smlbin/build cleanAllbin/build
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 trindemossen-1Alternatively, 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.
Another good resource for newcomers is the Tutorial. It provides an introduction to the system for new users, as well as detailed installation instructions. The tutorial is also available in Italian (though for Kananaskis-10 only).
In winter 2019/2020 a course about HOL was given at KTH aimed at the needs of the STEP group and tried to provide some hands-on experience with HOL. The course homepage and the github repository contain lecture slides, homework exercises and relevant code. For a predecessor course slides (printer friendly version, LaTeX sources) as well as the exercise sheets are available.
Beginners and advanced users sometimes consult this Cheatsheet. 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/help/HOLindex.html, where 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.
The HOL theorem prover is a collaborative project hosted on GitHub. We welcome contributions (e.g. code via pull requests) and provide help and advice via mailing lists and chatrooms:
hol-info mailing 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) ]
#hol channel in its Discord — join!
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.