# HOL Light: an interactive theorem prover in OCaml > HOL Light is a proof checker you drive from the OCaml prompt, where a proof is a piece of OCaml code that constructs a theorem rather than a sequence of menu commands. It installs through OPAM in one command or builds from source with a camlp5 syntax extension, and a first run rebuilds the core theories before it lets you start proving. **jrh13/hol-light** — The HOL Light theorem prover - Repository: https://github.com/jrh13/hol-light - Stars: 561 · Forks: 100 - Language: OCaml - License: NOASSERTION - Published: 2026-10-22 · Updated: 2026-10-22 · Language: en - Canonical page: https://hysenlabs.com/projects/jrh13-hol-light ## A prover you talk to in the OCaml prompt The README describes HOL Light as an interactive theorem prover and proof checker, written in Objective CAML (OCaml), and using the toplevel from OCaml as its front end. That last clause is the whole design. There is no separate proof language and no separate interface. A HOL Light proof is OCaml code that constructs a theorem, and the environment in which you construct it is the ordinary OCaml toplevel. The developer of the system, John Harrison, has written it this way deliberately, and the consequence is that everything OCaml gives you is available while proving, which for a formal methods person is the point rather than a shortcut. The homepage is hol-light.github.io, and the README links a tutorial in both HTML and PDF for the detailed usage instructions, and a reference manual with per-function documentation in HTML and as a single PDF. The scale is worth understanding before you install it. The repository root holds directories for individual areas of mathematics and logic: Arithmetic, Complex, Divstep, Formal_ineqs, Functionspaces, Geometric_Algebra, Jordan, LP_arith, Multivariate, Probability, Quaternions and more, alongside the tooling directories Cadical, Minisat, QBF, Boyer_Moore and Proofrecording, and a dozen others. The core is comparatively small, and the proofs are the bulk of the work. The primary language is OCaml, the default branch is master, and the last push was on 2026-10-20. ## One OPAM command is the whole installation The README calls OPAM, an OCaml package manager, the easiest way to install HOL Light, and the command is short: ``` opam install hol_light # To compile the core module of HOL Light and use, add hol_light_module # opam install hol_light hol_light_module ``` So there are two packages rather than one, and the distinction is between the interactive version and the compiled core. The hol_light package gives you the system as the README describes it, and hol_light_module adds the ability to compile the core module and use it, which is what you want if you are building something on top of the system rather than proving things in it. The README says the install will build 'hol.sh' and copy it at the 'bin' path of your OPAM setting, making it executable at any location. That is a small but useful property: the launcher script does not care where it is run from, so a checked-in or shared installation works the same way for everyone. The manual route is described for anyone who cannot use OPAM. You need OCaml itself, and on a Debian derivative such as Ubuntu the README says you may just need: ``` sudo apt-get install ocaml ``` Alternatively you can download binaries directly, or get sources and build them, which in the author's experience is usually trouble-free. The dependency route with OPAM is a local switch, which is what keeps a checkout from disturbing the rest of your OCaml installation: ``` make switch # or 'make switch-5' for OCaml 5 eval $(opam env) ``` A local switch uses the latest OCaml version that fully supports the features needed, plus all the dependencies, and eval $(opam env) puts it in your environment. The README also points at its DEPENDENCIES chapter for installing them by hand. ## The first build is a camlp5 syntax extension If you build from source, the first thing 'make' does is build the syntax extension. The Makefile header puts it plainly: a simple make just builds the camlp4/camlp5 syntax extension pa_j.cmo, which is necessary to load the HOL Light core into the OCaml toplevel. That is the step most likely to produce a confusing error, and the README walks through it. If you have the camlp4 or camlp5 libraries in a non-standard place rather than /usr/local/lib/ocaml/camlp4 or /usr/local/lib/ocaml/camlp5, you may get an error like this: ``` Error while loading "pa_extend.cmo": file not found in path. ``` in which case you should add the right directory to CAMLP4LIB or CAMLP5LIB, for example: ``` export CAMLP5LIB=$HOME/mylib/ocaml/camlp5 ``` The error message names a file that is not the one you built, which is why the README explains it rather than leaving you to work it out. The Makefile also credits Carl Witty for the 3.07 and 3.08 ports of pa_j.ml, which is the kind of detail that tells you the extension is maintained against OCaml versions rather than frozen at one. The build is otherwise deliberately dull. The Makefile lists the core source files explicitly in the HOLSRC variable, which is a useful artefact in itself, because it is the authoritative list of what the core consists of: ``` HOLSRC=system.ml lib.ml fusion.ml basics.ml nets.ml preterm.ml \ parser.ml printer.ml equal.ml bool.ml drule.ml tactics.ml \ itab.ml simp.ml theorems.ml ind_defs.ml class.ml trivia.ml \ canon.ml meson.ml firstorder.ml metis.ml thecops.ml quot.ml \ impconv.ml recursion.ml pair.ml compute.ml \ nums.ml arith.ml wf.ml calc_num.ml normalizer.ml grobner.ml \ ind_types.ml lists.ml realax.ml calc_int.ml realarith.ml \ real.ml calc_rat.ml int.ml sets.ml iterate.ml cart.ml define.ml \ help.ml database.ml update_database.ml hol_lib.ml hol_loader.ml ``` The BINDIR variable in the Makefile defaults to ${HOME}/bin for standalone binaries, which is where the OPAM-installed hol.sh ends up too. ## The first hol.sh run rebuilds the core theories Step two of the basic approach is to run the launcher, and the README is precise about what it does. If you are using a Unix-like environment, simply run `./hol.sh`. This should rebuild all the core HOL Light theories, and terminate after a few minutes with the usual OCaml prompt, something like: ``` Camlp5 parsing version (HOL-Light) 8.03.00 # ``` And then the line that tells you it worked: ``` HOL Light is now ready for the user to start proving theorems. ``` So the first launch is not instant, and the reason is that HOL Light is a system of theories rather than a program with a fixed set of built-in facts. The core has to be reconstructed before you can use it, and the several minutes it takes is a one-off per build, not a per-session cost. Once the prompt is up, you load the system with `#use "hol.ml";;`, and the README is careful that the `#` is part of the command and not the prompt: ``` At the OCaml prompt '#', do '#use "hol.ml";;' (the '#' is part of the command, not the prompt) followed by a newline. ``` Two more details in the README matter in practice. On non-Unix systems you run 'ocaml' instead, and for OCaml 4.02 and later the author prefers 'ocaml -safe-string' to avoid mutable strings, while you may need something else like 'ocamlnum' on some platforms. And if you are using OCaml 4.14 you need to create a top-level OCaml with 'ocamlmktop -o ocaml-hol' and use 'ocaml-hol', because the default 'ocaml' does not have 'compiler-libs' that is necessary to run HOL Light. The load process also works from other directories, provided you either set the HOLLIGHT_DIR environment variable to point at the directory containing the HOL source files, or change the first line of hol.ml, which by default reads the environment variable and falls back to the current working directory: ``` let hol_dir = ref (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());; ``` or hard-code a path such as: ``` let hol_dir = "/home/johnh/hol-light";; ``` The author's own examples include "/usr/share/hol";; for a system-wide installation. ## The standalone image, and the checkpointing it depends on The README describes two alternatives: launch the OCaml toplevel and load the HOL Light source files into it, or create a standalone image with all the HOL Light sources pre-loaded. The latter is more convenient, but requires a separate checkpointing program, which may not be available for some platforms. The convenience in question is a snapshot of the whole session, so you get the system loaded instantly and can checkpoint it to disk. The README notes that as of 2025 there are three programs you can use for this. DMTCP is the first. If you have DMTCP, 'make hol' will build a checkpointed HOL Light binary 'hol'. To launch it, simply run './hol'. To launch multiple instances, run './hol -p '. DMTCP is available from its own GitHub releases, and as of 2025 it only supports Linux. You can also build your custom checkpoint using 'make-checkpoint.sh' which exists in this directory. CRIU is the second. CRIU is similar to DMTCP but faster. However, it requires sudo privilege depending on your environment, for example under WSL2, and it comes from criu.org. The third entry is cut off in the README available here, but the visible fragment shows the shape of the procedure, starting the ocaml process and loading HOL Light, which is a manual checkpointing route rather than a packaged binary. The multiple-instance flag is worth noticing on its own. The -p option with a fresh port number lets you run several independent HOL Light processes, which matters if you are working on several proofs in parallel and want each to keep its own state. ## A repository that is mostly mathematics The top-level entries are the best description of what HOL Light is. Alongside the source files at the root, arith.ml, basics.ml, canon.ml, class.ml, compute.ml and the rest, there are directories named for areas of mathematics: Arithmetic, Complex, Functionspaces, Geometric_Algebra, Jordan, LP_arith, Multivariate, Permutation, Probability, Quaternions, Realaxils under Arithmetic, Vector spaces under Functionspaces, and a directory called 100 for a hundred theorems on one topic. There are also directories named after tools and techniques rather than subjects: Cadical, Minisat and QBF for the automated reasoners, Boyer_Moore for a decision procedure, Autoformalization, Proofrecording and ProofTrace for capturing proofs, and IsabelleLight and Mizarlight for work in other provers' styles. The Examples directory shows the kind of thing that ends up there, and the file names are a good indicator of the material. There is apery.ml, after Apéry's proof that the square root of 2 is irrational, bondy.ml for the Bondy and Murty theorem, borsuk.ml and brunn_minkowski.ml for results in geometry, kb.ml for a proof, lagrange_lemma.ml, harmonicsum.ml, doomsday.ml for the doomsday algorithm, and the inverse_bug_puzzle files, which are puzzles stated as proofs. Then there are the reference aids. QUICK_REFERENCE.txt and VERYQUICK_REFERENCE.txt sit at the root for people who know the system and need a reminder, and there is a Tutorial directory and a Help directory, which is where the built-in help system lives. Two more directories suggest the scope. Unity is about reasoning with a formal model of the Unity game engine, and IsabelleLight is a port of Isabelle Light work, both of which show that HOL Light is used as a host for larger efforts rather than only for proving theorems for their own sake. ## A custom licence and a release every year or so The repository listing records the licence as one GitHub cannot classify, with a note to see the LICENSE file at the root. That is unusual enough to say plainly: anyone intending to build on HOL Light, or to redistribute it, should read that file rather than assume a standard academic or permissive grant. The release history is short and steady. The recent releases are Release-3.1.0, tagged HOL-Light-3.1.0, from 2025-06-19, and Release-3.0.0, tagged HOL-Light-3.0.0, from 2024-10-14. So the major versions come roughly every eight months, with the 3.0 release in late 2024 and the 3.1 release in mid 2025. The repository itself is not archived and the last push was on 2026-10-20, which is a few months after the 3.1 tag. The OCaml compatibility range is worth recording too, since it is the practical constraint on whether the system will run for you. The README says HOL Light should work with any recent version of OCaml, and the author lists the versions tried: 3.04, 3.06, 3.07+2, 3.08.1, 3.09.3, 3.10.0, 3.11.2, 4.00, 4.05, 4.14, 5.1.0, 5.2.0, 5.4.0 and 5.5.0. That last one, 5.5.0, tells you the system is still being kept working against current OCaml releases, and the make switch-5 target mentioned in the installation instructions exists for the same reason. The whole picture is of a long-lived personal research project that has been maintained continuously for decades and released at a steady, unhurried pace, with the source available and the terms set out in a file rather than in the README. ## Conclusion HOL Light fits a formal methods researcher or a student learning mechanised proof who wants to see a small, readable kernel rather than a large automated system, and who is comfortable in OCaml. It is the wrong choice if you want automation first and proof engineering second, because the design assumes a human drives every step, and the wrong choice if you need a system with a maintained library of formalised mathematics across many fields. Verify first which OCaml version you have and whether you are on OCaml 4.14, where the default ocaml lacks compiler-libs and you need a custom toplevel, and read the LICENSE file, because the repository listing records a custom licence rather than a standard one. ## FAQ ### What is HOL Light? It is an interactive theorem prover and proof checker written in OCaml, using the OCaml toplevel as its front end. The homepage is hol-light.github.io, with a tutorial and a reference manual published alongside it. ### How do I install HOL Light? Through OPAM with opam install hol_light, adding hol_light_module if you want to compile the core module and use it. That builds hol.sh and copies it to the bin path of your OPAM setting. To build from source you need OCaml and its dependencies, with make switch and eval $(opam env) creating a local switch. ### What does the first run of hol.sh do? It rebuilds all the core HOL Light theories and terminates after a few minutes at the usual OCaml prompt, showing something like Camlp5 parsing version (HOL-Light) 8.03.00. You then load the system with #use "hol.ml";; at the prompt, where the # is part of the command. ### What is the pa_extend.cmo error when building HOL Light? It appears when the camlp4 or camlp5 libraries are in a non-standard place rather than under /usr/local/lib/ocaml. The fix is to add the right directory to CAMLP4LIB or CAMLP5LIB, for example export CAMLP5LIB=$HOME/mylib/ocaml/camlp5, since the first make step builds the pa_j.cmo syntax extension. ### Does HOL Light work with recent OCaml versions? The README says it should work with any recent version of OCaml, listing versions tried from 3.04 through 5.5.0, and the Makefile has a make switch-5 target for OCaml 5. On OCaml 4.14 you need a custom toplevel built with ocamlmktop -o ocaml-hol, because the default ocaml lacks compiler-libs. ## Sources - [Issues](https://github.com/jrh13/hol-light/issues) - [jrh13/hol-light on GitHub](https://github.com/jrh13/hol-light) - [README](https://github.com/jrh13/hol-light/blob/master/README.md) - [Releases](https://github.com/jrh13/hol-light/releases) --- Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/jrh13-hol-light