Mike Gordon Tom Melham Robin Milner Larry Paulson Konrad Slind

and many other HOL and LCF researchers

**HOL Light is now a Google Code
project** so you can get the sources from the Google Code repository. You can
browse individual source files online, or check out all the code using subversion. For
example, the following command will copy all the code from the trunk of the
Google Code repository into a new directory `hol_light`:

svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_lightHOL Light is written in Objective CAML (OCaml), and it should work with any reasonably recent version. To build with OCaml 3.10 and later you will also need to install camlp5, version 5.07 or higher. See the README file in the distribution for detailed installation instructions.

For those who prefer to download a packaged version directly instead of using
subversion, a **snapshot from 10th January 2010** is available as
a gzipped tar file or as a zip file. The last numbered release, now quite
old, is 2.20, which you can get here.
(**Note that 2.20 doesn't work under OCaml >= 3.10, owing to changes to
camlp4. If you really want to use HOL Light with these versions of OCaml, use
one of the more recent versions listed above.**)
Experimental Linux binaries for version 2.20 are also now available, created
using CryoPID. NB: I'm not sure how
portable these are across Linux versions; better to build from source if you
can. The files are hol (core system), hol.sosa (preloaded with analysis and sum-of-squares
tools), hol.multivariate (preloaded with
multivariate analysis) and hol.card (preloaded with
cardinal arithmetic). Note that although these work as standalone executables,
if you are planning to work much with the system, you'll probably still want to
download the HOL sources to give access to additional library directories and
to the help files. For example, if you download the HOL Light source tree to
"`/home/myself/hol_light`", you might start a HOL Light session with the
following so that HOL Light can find all the files (`#` is the OCaml
prompt):

# hol_dir := "/home/myself/hol_light";; val it : unit = () # load_path := ["."; !hol_dir];; val it : unit = ()The following lists some available documentation and resources:

- Reference Manual available as online crosslinked HTML or as one PDF file (also an older variant keyed to version 2.20).
**Tutorial**, which tries to teach HOL Light through examples.- Quick Reference Guide compiled by Freek Wiedijk (text, PDF, Postscript, DVI, LaTeX)
- Jeremy Bem's hol-online, and the earlier project Formalpedia, use a processed version of HOL Light to produce an online repository of software and formal mathematics.
- Summary of many HOL source files, written by Carl Witty (text)
- Old user manual, not fully updated from the older CAML Light version (DVI, Postscript and PDF).
- The hol-info mailing list is a good place for HOL-related discussion
- Josef Urban's HOL Proof Advisor uses automated data mining to produce proof advice.

- Formalization of floating-point arithmetic, and the formal verification of
several floating-point algorithms at Intel.

See this paper for a quick summary and more references, and this one for a more detailed presentation. - The Flyspeck project
to machine-check Tom Hales's
proof of the Kepler conjecture.

Tom has already proved the Jordan Curve Theorem and other relevant results in HOL Light. - Many other mathematical results of varying degrees of difficulty have been
verified in HOL Light.

See for example the HOL Light entries on the Formalizing 100 Theorems page.

Last updated by John Harrison on 16th October 2011.