Skip to content
<open-source>
Oeiuwq Faith Blog OpenSource Porfolio

HOL-Theorem-Prover/HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
Source code at GitHub https://hol-theorem-prover.org
HOL-Theorem-Prover/HOL.json
{
  "createdAt": "2009-10-29T02:47:31Z",
  "defaultBranch": "develop",
  "description": "Canonical sources for HOL4 theorem-proving system.   Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.",
  "fullName": "HOL-Theorem-Prover/HOL",
  "homepage": "https://hol-theorem-prover.org",
  "language": "Standard ML",
  "name": "HOL",
  "pushedAt": "2026-01-07T22:43:55Z",
  "stargazersCount": 708,
  "topics": [
    "higher-order-logic",
    "lambda-calculus",
    "theorem-proving"
  ],
  "updatedAt": "2026-01-07T22:43:59Z",
  "url": "https://github.com/HOL-Theorem-Prover/HOL"
}

Build Status

This is the distribution directory for HOL4. See http://hol-theorem-prover.org for online resources.

Installation

Section titled “Installation”

See the HOL homepage for more detailed installation instructions, including for Windows.

Prerequisites

Section titled “Prerequisites”

HOL4 supports multiple SML compilers:

  • Poly/ML (recommended) — The primary backend for building and running HOL4.
  • Moscow ML (version 2.10) — An alternative backend, ensuring HOL sources remain portable across SML implementations.
  • MLton (optional) — If installed, automatically used to build tool executables (Holmake, etc.) which may run faster.

For Poly/ML, ensure that your dynamic library loading can find libpolyml.so and libpolymain.so. If these are not in /usr/lib, you may need to set LD_LIBRARY_PATH, e.g.:

export LD_LIBRARY_PATH=/usr/local/lib:$HOME/lib

Building

Section titled “Building”

In the HOL directory, run:

poly --script tools/smart-configure.sml

(or mosml < ... for Moscow ML). Then:

bin/build

If smart-configure guesses options incorrectly, create tools-poly/poly-includes.ML with corrected ML bindings (e.g., val holdir = "/path/to/hol").

Once the build completes, the key executables are:

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

Note that the system is built in place and cannot easily be moved after installation.

External tools

Section titled “External tools”

Some components include C/C++ code that requires a C compiler:

  • src/HolSat/sat_solvers/minisat/ contains the MiniSat SAT solver sources. Run make in that directory to build.
  • examples/muddy/ contains the BDD library, which requires building the shared library in examples/muddy/muddyC/.

Dealing with failure

Section titled “Dealing with failure”

If the build fails, try bin/build cleanAll before rebuilding. To report problems, come find us on Zulip, and/or use the GitHub issues page.

Distribution contents

Section titled “Distribution contents”

The following is a brief listing of what’s available in the distribution.

 README.md      * This file
 CONTRIBUTORS   * List of contributors
 COPYRIGHT      * Copyright notice
 bin/           * Executables
 developers/    * Resources for developers
 doc/           * Release notes
 examples/      * Example formal developments, from small to large
 help/          * Sources for online help
 Manual/        * System manuals
 sigobj/        * Collection of all signatures and compiled code
 src/           * System sources
 std.prelude    * File loaded at the beginning of each HOL session
 tools/         * Support for building the system
 tools-poly/    * Poly/ML-specific support for building the system