HOL4: the canonical sources of a higher-order logic theorem prover

What this repository actually is

The README calls this the distribution directory for HOL4, and the homepage is hol-theorem-prover.org. The primary language is Standard ML, and the topic tags name the field, higher-order logic, the lambda calculus and theorem proving.

The description on the repository makes one point that anyone cloning it should read first. Branch develop is where mainline development occurs, and when develop passes the regression tests, master is merged forward to catch up.

That is an unusual arrangement and it has a practical consequence. The default branch on the repository is develop, so a clone gives you the moving development line rather than the stable one, and the stable line is master, which only moves when the tests pass. For someone who wants to use HOL4 rather than work on it, master is the branch to take, and the reason is that it is the one that is known to pass the regression suite.

The system itself is a theorem prover for higher-order logic. The distribution listing in the README shows the shape of it: the executables in bin/, the system sources in src/, the compiled signatures and code in sigobj/, the manuals in Manual/, the online help sources in help/, the release notes, the copyright and licence files, the support scripts for building the system in tools/ and tools-poly/, the developer resources, and the examples directory holding formal developments from small to large.

The examples are worth noting on their own, because the listing runs from small to large and includes AI, AKS, CCS and Crypto, a Hoare-for-divergence development, a BDD library, a model checker, the PSL, a machine learning syntax development, an ACL2 development, algebra, algorithms, an ARM development, axiomatic developments, a category theory development, computability, and a decidable separation logic example.

The project is not archived and the last push was on 2026-10-22.

The compiler choices and what each one is for

HOL4 supports multiple SML compilers, and the README explains what each is for rather than just listing them.

Poly/ML is the recommended one and the primary backend for building and running HOL4. Moscow ML at version 2.10 is an alternative backend, and the stated reason for keeping it is to ensure the HOL sources remain portable across SML implementations. MLton is optional, and if it is installed it is automatically used to build the tool executables such as Holmake, which may then run faster.

The portability argument is the interesting one. A system written in Standard ML has the advantage that it can be built by more than one implementation, and a project that supports two or three of them is not hostage to one vendor's compiler. The cost is that some Standard ML code has to be written to the common subset, and the tools-poly/ directory reflects that the build machinery is compiler-specific.

There is one practical wrinkle with Poly/ML, and the README gives the fix. You have to ensure that your dynamic library loading can find libpolyml.so and libpolymain.so, and if those are not in /usr/lib you may need to set LD_LIBRARY_PATH, for example by exporting it with /usr/local/lib and your own lib directory on the path.

So the compiler choice is not only about speed. It determines how the build is invoked, and the loader configuration has to be right before anything else works.

Building the system in place

The build sequence is short, and the first step is a configuration script rather than a make invocation.

In the HOL directory you run the smart configure script.

poly --script tools/smart-configure.sml

There is a Moscow ML equivalent, invoked as mosml with the script piped in, and then the build itself.

bin/build

If smart-configure guesses the options incorrectly, the README says to create tools-poly/poly-includes.ML with corrected ML bindings, giving the example of setting the holdir value to the path to the HOL directory. That is a hand-edited configuration file, which is a reminder that the build system is a set of scripts rather than a declarative package manager.

Once the build finishes, two executables matter.

bin/hol       The standard HOL interactive system
bin/Holmake   A batch compiler for HOL directories

The interactive system is the REPL you prove theorems in, and Holmake is the batch compiler that builds a directory of HOL sources, which is what you want for large developments and for continuous integration.

One constraint is stated plainly and it is worth knowing before you build. The system is built in place and cannot easily be moved after installation. Everything the binaries reference, including the compiled signatures and the source paths, is resolved relative to the build directory, so moving the tree afterwards breaks it. If you want it somewhere else, build it there.

The external components that need a C compiler

Two parts of the distribution are not Standard ML, and the README calls them out because they will otherwise fail in a confusing way.

The first is the MiniSat SAT solver, whose sources sit under src/HolSat/sat_solvers/minisat/ and are built by running make in that directory. The second is the BDD library in examples/muddy/, where the shared library in examples/muddy/muddyC/ has to be built.

So a build of HOL4 alone is not a complete build of the distribution. The SAT solver is part of the system, since the model checking and the propositional reasoning both lean on it, and the BDD library is part of the examples. A user who skips both will find the corresponding functionality missing.

The dealing with failure section is short and practical. If the build fails, try bin/build cleanAll before rebuilding, and to report problems come to the Zulip chat or use the GitHub issues page. Both links are given, and the Zulip channel is the one a theorem prover community actually uses, since a failed build of a Standard ML system is the kind of question that is easier to answer in a chat than in an issue thread.

There is also a Docker CI workflow badge at the top of the README, which suggests the project builds itself in a container, which is a reasonable way to get a working environment without configuring the dynamic library paths by hand.

The distribution layout and how the examples are organised

The directory listing in the README is a map of the system, and each entry has a clear role.

The README file itself, the bin/ directory of executables, a CONTRIBUTORS list, a COPYRIGHT notice, and a copyrights/ directory holding the copyright and licence files for the various components. The developers/ directory holds resources for developers, examples/ holds the formal developments, help/ holds the sources for the online help, Manual/ holds the system manuals, release-notes/ holds the release notes, sigobj/ holds the collection of all signatures and compiled code, src/ the system sources, and tools/ and tools-poly/ the support for building the system.

Two things stand out for a new user. The help/ and Manual/ directories together mean the documentation is part of the distribution rather than something to fetch separately, which is how a system that is twenty years old stays usable. And the copyrights/ directory, which is where the licensing story of the many components lives, is worth reading before you redistribute anything.

The examples directory is the more interesting one for the examples themselves, and the README calls it example formal developments, from small to large. The entries in the listing cover both domains and techniques. AI and Crypto are applied, AKS and CCS are industrial, Hoare-for-divergence and computability are foundational, HolBdd and HolCheck are verification tools, MLsyntax concerns the syntax of the ML language itself, PSL is the property specification language, and algebra, algorithms, category, bnf-datatypes and axiomatic-developments are the foundations. There is also an ACL2 development, and a decidable separation logic example.

That spread is a reasonable way to judge whether HOL4 fits your area, because a theorem prover is not much use outside the theories it has been developed for.

Where HOL4 is the wrong choice

The first limitation is the build. There is no package manager route, no prebuilt binary in the repository, and the system has to be compiled in place with an SML compiler you install yourself, plus a C compiler for two components, plus a dynamic library path configured correctly. For a theorem prover whose competitors ship as installable packages, that is a real barrier, and it is the barrier a new user meets first.

The second is the language and the ecosystem. Standard ML is a fine language but a small one, so the surrounding tooling, editor support and community are all smaller than for the proof assistants that now dominate. A system from this era accumulates workarounds that newer tools have solved.

The third is the library coverage relative to the alternatives. A modern proof assistant has libraries for the fields people actually work in, and a proof in HOL4 may need a development written from scratch. The examples directory shows what exists, and for a project outside those areas the starting point is thin.

The fourth is the branch model. The default branch is develop, which is the moving line, and master is the stable one that only advances after the regression tests pass. A team that clones the default and pins nothing is building against unreviewed mainline work, and the README does not say which branch a release corresponds to.

The fifth is the release tagging. The recent releases are named after contributors, trindemossen-2 from 2025-08-12, trindemossen-1 from 2024-04-25 and kananaskis-14 from 2021-02-03, which tells you the project ships snapshots named for whoever prepared them rather than version numbers, so pinning a release means pinning a snapshot tag rather than a semantic version.

How HOL4 compares with Lean, Coq and Isabelle

The comparison with Lean is the one that comes up first now, and the difference in approach is the background library and the tooling. Lean has a large library of formalised mathematics and a well-integrated editor and build system, and the community is far larger. HOL4 is older and its origins are in hardware verification and in the LCF family of provers, and its strengths lie in the developments that have been done in it and in the discipline of its design.

The comparison with Coq is about the calculus and the proof style. Coq's system is built on the calculus of inductive constructions, and its interaction tactics and the shape of a proof are different from HOL4's term-based approach. Both are complete, and both are the right choice for different bodies of existing work, since a proof written in one is not portable to the other.

Isabelle is the third comparison, and it is the closest in spirit in one respect, with its emphasis on higher-order logic, and the furthest apart in mechanics, with a different proof language built on Isabelle/HOL and a different integration model.

The honest framing is that a theorem prover is chosen by the theory you need to formalise, not by the features. If your area has a mature library in one of them, that is the one to use, and the formal developments in this repository's examples directory are the best guide to what HOL4 has been used for.

The last comparison is with not formalising at all. For most problems, a proof assistant is a heavy answer, and the value here is in the specific cases where a machine-checked proof is needed and the theory is within reach.

Licence, project state and what to check before you build it

The licence field on the repository records a custom licence that GitHub cannot classify, with the terms in the LICENSE file, and the distribution includes a COPYRIGHT notice and a copyrights/ directory holding the copyright and licence files for the individual components. For a system that bundles a SAT solver, a BDD library, an SML compiler ecosystem and decades of accumulated source, that directory is the place where the actual terms live, and it is worth reading before redistribution.

The project is not archived and the last push was on 2026-10-22, so it is very much alive. The primary language is Standard ML, the homepage is hol-theorem-prover.org, and the recent releases are the contributor-named snapshots already mentioned.

Four things to check before you build it.

Which compiler you will use. Poly/ML is the recommended backend, Moscow ML is the portability alternative, and MLton is optional and used for the faster tool executables if it is present.

That your dynamic library path is right for Poly/ML, because libpolyml.so and libpolymain.so have to be findable, and that is the most common first failure.

That you build it in place, because the system cannot easily be moved after installation, and a container is the easier way to get a disposable environment.

And which branch you are on. develop is where mainline development happens, and master is merged forward once develop passes the regression tests, so master is the branch to take for use and develop is the branch to take for work on the system itself.

Editorial conclusion

This repository suits someone who wants to work on HOL4 itself, or to use it to formalise something where an existing proof assistant would not do, and who is prepared to build a Standard ML system by hand. It is the wrong choice for a general theorem proving setup, since a modern proof assistant with a larger library and better tooling will serve most purposes, and it is the wrong choice if you want a binary you can install from a package manager. Before you start, read the build instructions on the project homepage, because the system is built in place, the compiler choice matters, and the two extra C components have to be built by hand.

Frequently asked questions

Official sources

1. HOL-Theorem-Prover/HOL on GitHub
2. Issues
3. Project website
4. README
5. Releases