Before installing HOL, check that you have the pre-requisites. In particular HOL requires a Standard ML compiler, one of
HOL also supports MLTon (an optimizing compiler for Standard ML) that can be used to build tool executables.
Once you have installed PolyML (resp. Moscow ML), ensure that the installation path for libpolyml (resp. libmosml), typically /usr/lib/local/ is added to
your dynamic library search path.
This can be accomplished by appending the following line to your shell configuration file.
(This is ~/.bashrc for the bash shell.
You can determine your shell on your terminal with the command echo $0.)
If you are using bash, appending the following line will allow polyml to locate libpolyml.
export LD_LIBRARY_PATH="/usr/local/lib:$LD_LIBRARY_PATH"
Now the next thing you need to do is to 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-2Alternatively, 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.
Browse the full documentation online →
All of HOL's manuals can be browsed online as a single, searchable site, which also includes the reference documentation and the theory dependency graph. The individual manuals are also available as PDFs, as linked below.
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 documentation to look up information while they work. Note that a local copy of the reference is also built when you install HOL. 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.