Introduction

This manual attempts to provide documentation for people wishing to develop HOL4, a process that will likely involve frequent re-compilations or rebuilds of the core sources.

As per the standard installation instructions, once one has an SML installation, there are two stages to the process of building HOL4:

1. The first step is the configuration of the system (see Configuration below). This is achieved with the command

      smlsystem < tools/smart-configure.sml
   

   where smlsystem is either poly or mosml. This command must be issued from the root of the HOL installation, where the path tools/smart-configure.sml makes sense. This should complete quickly.

2. Second, one needs to build the system (see Build below). This is achieved with the command

      bin/build
   

   assuming one is still in the root HOL directory. Note however, that build can be executed from anywhere. In particular, if <holdir>/bin is in one’s path, it is reasonable to run build from any directory.

   When first executed, the build process will take a while because it proves all of the theorems in the core system, writing theories to disk as it goes. Building should terminate with the message

      Hol built successfully.
   

   Repeated calls to build should complete quickly: theorem-proving work will not be redone unnecessarily. The building of the theory graph can be slow however, and this does happen with every invocation of build by default. To avoid this, pass --no-mdbook or --no-helpdocs to build: either flag skips the documentation pipeline (which includes the theory graph).

Configuration

The configuration process is responsible for

• calculating important environmental details, such as the SML implementation, the nature of the operating system, and important paths;
• the creation of core system tools: standard SML tools (mlyacc, mllex), and HOL-specific tools (most importantly, the quotation filter, Holmake and build).

The first thing that configuration does is to figure out which SML implementation is being run. This is important because the compilation and creation of executables differs so dramatically in Poly/ML and Moscow\ ML. Once this determination is made, actual configuration work is done in either tools-poly/configure.sml or tools/configure.sml (See Sources below for more on how these sources are organised.)

One of the core outputs of configuration is the Systeml structure. This has a fixed signature, given in tools/Holmake/Systeml.sig, but has a structure that is filled with installation- and ML implementation-specific details. The generated file is tools/Holmake/Systeml.sml, which is generated from either tools/Holmake/unix-systeml.sml (for Moscow ML) or tools-poly/Holmake/unix-systeml.sml (for Poly/ML). There is an additional tools/Holmake/winNT-systeml.sml meant for Moscow ML on Windows, but this code hasn’t been tested and is probably bit-rotted.

Building (and Rebuilding) Holmake

Because Holmake is not assumed to exist when Holmake is built, the configuration script is responsible for assembling the constituent sources. In the case of Moscow\ ML, this means that it makes the successive calls to mosmlc as necessary. With Poly/ML, the work is orchestrated by tools/Holmake/poly/poly-Holmake.ML. That file is a sequence of calls to use, followed by a simple definition of a main function. This can then be compiled with polyc.

Note that we can’t simplify the Moscow\ ML build in a way analogous to what happens with Poly/ML because the complicated sequence of instructions are command-line invocations of mosmlc, rather than calls to use within a Poly/ML program. We might attempt to create a shell-script containing the calls to mosmlc, but it seems more OS-independent to invoke OS.Process.system from within configure.sml.

Quick rebuilds of Poly/ML Holmake are possible by making the call

polyc -o ../../../bin/Holmake poly-Holmake.ML

in the tools/Holmake/poly directory. It is necessary to specify the output path (with the -o option) to replace the old Holmake if one is going to test/use the new tool in the existing HOL sources. Without doing this, the new implementation will see that it is in a HOL source–tree and then switch to call the Holmake in that source-tree’s bin directory.

Build

The standard options to build are described in its help documentation, which is accessible by invoking build --help (or build -h, or build -?, but not build help because this builds the HOL documentation). The file containing this information about options is located at tools/build/buildhelp.txt.

The most frequently used options to build are those to do with “selftest” level, and the selection of kernel.

Regression Testing

The build program’s --selftest option can be given as is (in which case the selftest level is 1), or followed by a positive number, which gives the selftest level explicitly. The higher the number, the more regression tests are executed. Developers are expected to categorise their tests so that those at level 1 will complete quickly, those at level 2 will execute in moderate time, and those at level 3 can take as long as is necessary.¹ As of 2022, there are no regression tests that require a level greater than 3, and we will likely keep things this way.

There are two standard ways to the install a test that can be run by build:

1. Create a selftest.exe executable in an existing directory that build works on. The Holmakefile in this directory will need to specify how to build this executable, and then additionally include an

    ifdef HOLSELFTESTLEVEL
    endif
   

   block to get the executable to be run. Just checking if the variable is set, will cause execution at all non-zero levels. To fire a test only at particular levels, use the ifeq and related commands. It may also be a good idea to have this block produce a log-file recording the execution of the selftest; this can be done effectively with the Holmake function $(tee ...).

   There are a number of examples of constructing selftest.exe executables in the sources. See for example src/boss/selftest.sml and src/boss/Holmakefile. Though the Holmakefile gives build commands in terms of $(HOLMOSMLC), the selftest.exe executable will also be built correctly if running Poly/ML.

2. Create a new directory for build to operate on. This directory can be inserted into the early stages of the build sequence, as explained in the documentation at the head of tools/build/build-sequence. If the testing happens after bossLib and (in Poly/ML) the creation of the standard hol.state heap, the directory should be included in the Holmakefile in src/parallel_builds/core. The various tests in that file can be used to insert regression test directories into the big parallel build of all the post-bossLib directories. Using a test-directory is necessary if the tests need to examine behaviours to do with theory export and loading.

Kernel Selection

There are currently three kernels that can be built to underlie a HOL installation. The standard kernel uses a de\ Bruijn representation for terms, with bound variables represented as numbers. Free variables are represented as a pair of name and type. This kernel also implements explicit substitutions internally, allowing for efficient call-by-value execution with tools such as EVAL. This kernel is the default choice, and can be explicitly selected by passing the --stdknl option to build.

The experimental kernel uses name-type pairs for all sorts of variables. This means that the functions mk_abs and dest_abs operate in constant time. (In the standard kernel, these functions must switch between de\ Bruijn indices and free variables in the body when called, making them run in time linear in the size of the body.) The experimental kernel can be selected by passing the --expk option to build.

The OpenTheory kernel is based on the experimental kernel, but adds proof-logging to the primitive inference rules so that OpenTheory theory packages can be exported from HOL. This kernel can be selected by passing the --otknl option to build.

The tracing kernel uses the same proof-logging to the primitive inference rules as OpenTheory, but exports inference rules without additional translation. This kernel can be selected by passing the --trknl option to build.

Build Sequences

When build runs, it choreographs its calls to Holmake by referring to a specified sequence of directories. By default this sequence is that specified in the file tools/build/build-sequence, which in turn refers to other files via #include directives. It is possible to provide a different sequence by using the --seq commandline option to build. Such sequences can be constructed more easily by referring to sequence fragments in the tools/sequences directory, and including these with #include commands. The details of the required format for sequence files is spelled out in a comment at the head of the tools/build/build-sequence file.

Past the initial prefix of this process, most directories in the build sequence are actually listed in the Holmakefile in src/parallel_builds/core. This arrangement allows parallel processing of lots of directories at once. The sequence file upto-parallel gives the sequence of build targets up this point, so is a reasonable argument to --seq for tests of the core system.

Poly/ML Build Phases

When building under Poly/ML, build proceeds through three phases, distinguished by which Poly/ML heap the per-directory Holmake invocations use. The transitions are driven by the phase_extras function in tools-poly/build.sml.

1. Initial. No HOL-specific heap exists yet, so Holmake is invoked with --poly_not_hol. This phase covers the kernel through src/proofman, the directory in which the bare heap, bin/hol.state0, is built (along with its accompanying proofManagerLib.uo).

2. Bare. Once both bin/hol.state0 and sigobj/proofManagerLib.uo exist, subsequent Holmake invocations are passed --holstate <HOLDIR>/bin/hol.state0 so that they load against the bare heap. This phase covers everything from after src/proofman up to and including src/boss, in which the full bin/hol.state heap (which embodies bossLib) is built.

3. Full. After src/boss (signalled by the build reaching the bin/hol entry in the sequence), Holmake is invoked with no --holstate argument and so falls back to the default bin/hol.state heap. This phase covers all post-bossLib directories, including src/parallel_builds/ and the examples/ tree.

When editing in a directory that the build visits in the Initial or Bare phase (e.g., src/marker, src/q, src/combin, src/simp/src, src/IndDef, src/list/src, …), a plain Holmake invocation in that directory will either fail — when bin/hol.state hasn't been built yet, as on a fresh tree — or, worse, succeed by compiling against bin/hol.state, processing the file under edit in a context that already contains material built on top of it. To do a local re-compile before re-running the full build, pass --holstate $HOLDIR/bin/hol.state0 to Holmake. Otherwise, just rerun bin/build; on incremental changes this is fast and rebuilds downstream theories as well.

Rebuilding

It is often possible to repeat build to get the system to rebuild itself in the face of changed source files. If source files have moved directories, or disappeared entirely, build (more accurately Holmake when build calls it) may get confused by stale dependency information. In this situation, cleaning everything first with build cleanall may be necessary.

Things in bin

The build process deposits various tools in the bin directory. Under both Moscow ML and Poly/ML the following are created:

build

The build tool as above

hol

The standard executable, which loads a bossLib based logical context. This is designed for use by “every user”.

hol --bare

the “bare” mode, which includes boolLib and the goalstack infrastructure but no theories past bool.

Holmake

The Holmake tool, again designed for every user.

linkToSigobj

When the multi-directory, potentially parallel, build begins, this special-purpose tool is run in every directory after that directory’s build completes. It is responsible for linking to relevant src files in the sigobj directory, allowing HOL users to see/find those files without needing to explicitly mention the original src directory in an INCLUDES-directive.

mkmunge.exe

This tool creates LaTeX mungers, as described in the DESCRIPTION manual.

unquote

This is the quotation filter embodied as a Unix filter, with a variety of options to specify behaviour. Note that this is not used by Poly/ML HOL, but can be useful there to see what the filter (as embodied by the HOLSource module) is doing when it messes with user input.

Under Poly/ML, the following additional files will appear:

hol

this is the main Poly/ML HOL executable with subcommand-based CLI. It supports the following subcommands:

• hol or hol repl: Start an interactive REPL (default)
• hol --bare: Start REPL with minimal heap (hol.state0)
• hol lsp: Start LSP server
• hol buildheap -o <file>: Build a heap from object files
• hol run: Run script files for side effects (used by Holmake)
• hol heapname: Print the heap path (reads HOLHEAP from Holmakefile)

It embodies the quotation handling by implementing a copy of the standard Poly/ML REPL that fiddles with the lexer.

genscriptdep

Given a filename, this utility executable will generate a list of a script files dependencies.

hol.state

The Poly/ML heap used by hol by default. This embodies bossLib and is created in src/boss.

hol.state0

the Poly/ML heap used by hol --bare. This is built in src/proofman.

Sources and Their Organisation

HOL comes with two tools directories, tools and tools-poly, as well as a developers directory. The tools-poly directory is for sources that are specific to the Poly/ML implementation. The tools directory is for general sources, and for sources specific to the Moscow\ ML implementation. Apart from sources for tools that are genuine command-line executables, the tools directory also includes some configuration files and editor “modes”.

Tool Executables

The tools distributed with HOL are described below. Unless otherwise noted, they are built by the configuration process.

build

Described above. The top-level driver code is in files called build.sml in tools/build and tools-poly. Shared code is in tools/build/buildutils.sml. The executable is in bin/.

cmp

A simple-minded tool for comparing two files, returning (via exit code) 0 (success) if the two command-line arguments are byte-for-byte identical. Useful in regression testing of other tools. Built on demand via a Holmakefile. The executable is in tools/cmp.

dat-printer

A utility designed to pretty-print the theorem statements from theory files, using a simple-minded s-expression based format. The source files are located in src/portableML/rawtheory/.

Holmake

The user-facing tool for building HOL developments. Use of this tool is described in the Description manual. The tools/Holmake directory contains almost all of the sources, but the Poly/ML-specific template for the Systeml module (on top of which everything else in the system is built) is in tools-poly/Holmake. The Poly/ML specific code implementing concurrent Holmake is in tools/Holmake/poly. The executable is in bin/.

mllex.exe

The tool from SML/NJ. The executable is in tools/mllex.

mlyacc.exe

The tool from SML/NJ. The executable is in tools/mlyacc/src/.

theorytool

A dependency and definition analysis tool. Running it allows you to dynamically dump .dat keys, or output a full hierarchical ancestry graph of the theories using dot format via the --thygraph option. The source files are located in src/portableML/rawtheory/.

unquote

The quotation filter that runs over sources before they are seen by SML implementations. This is used interactively (via a Unix filter that preprocesses all user-input under Moscow ML, or built into the Poly/ML REPL), and non-interactively (by being applied to source files). The core sources are in tools/Holmake, but the standalone executable is built in tools/quote-filter and it is moved to bin/ as part of configuration.

h4pedant

Our tool for enforcing code style (as documented below). The command-line specifies the directories to scan, and options dictate which requirements are enforced/checked for. The enforcing of style is done by the Holmakefile in src/portableML/testsrc. The executable is in tools/h4pedant.

Other Tools Directories

tools/build-logs and tools-poly/build-logs

As each build proceeds, log files recording execution times per theory are generated and stored in these directories.

tools-poly/poly

Implementations of Binarymap, Binaryset, Listsort and Help (from the Moscow\ ML library) so that these libraries can be used in Poly/ML. These implementations are all use-d in poly-init.ML. That file also provides an implementation of a structure called Mosml, which provides a simple way of calling a shell command-line and getting back the string of that command’s output.

In poly-init2.ML, there is a definition of load, which implements the functionality that automatically loads “object code” and dependencies into running sessions. The poly-init2.ML file also use-s poly-init.ML. Calls are made to use "poly-init2.ML" in the construction of the first HOL heap (hol.state0), and in the scripts generated by Holmake run before that heap is built. These calls ensure that load is available to interactive and non-interactive uses thereafter.

The module holpathdb implements a very simple mapping from “environment variables” to paths. These environment variables are used by load to let “object files” list dependencies without having to use absolute paths. This file is use-d in, and so made available by, poly-init.ML. Subsequently, there needs to be a call made to initialise the database with an entry for the HOLDIR key. This is done in Holmake within poly/BuildCommand.sml, and also within poly-init2.ML (for interactive use). User-supplied entries come from holproject.toml files: when a project file's name key is set, the project root is registered under that name during Holmake's upward walk for project files. An optional holpath key overrides name for this registration only, leaving name free to serve as a human-facing project label distinct from the variable name (e.g. name = "cakeml" together with holpath = "CAKEMLDIR"). Conflicting registrations (same name pointing at different directories) are reported as fatal startup errors.

tools/sequences

Build sequence files. These are “modularised” so that, in principle, custom build sequences can be constructed more easily.

tools/editor-modes

Implementation of the editor modes.

Coding Standards/Requirements

We are fairly liberal in the style of code we accept, which is almost required given the long history of our sources (see arithmeticScript.sml for lots of old comments). However, the regression machinery does enforce some coding requirements, and these requirements may tighten over time. As of March 2025, the requirements are:

• No use of TABs anywhere.

• No trailing whitespace.

We encourage developers to keep their lines under 80 columns in width.

Glossary of Common Abbreviations in the Source Code

These appear with either capitalisation. There is a slight tendency to having all upper-case SML identifiers refer to theorems, or functions that return theorems.

abs

Abstraction.

ant

Antecedent of an implication.

asl, asm

Assumptions of a theorem or goal. The asl name is particularly commonly used to name a goal’s assumptions (used, e.g., when writing tactics).

conseq

Consequent of an implication.

_conv

Optional suffix to indicate a conversion. Useful to distinguish between a conversion, tactic and derived inference rule that perform the same basic function.

dest_

“destroy”, i.e.: decompose an object into simpler constituents.

g

Goal of a tactic.

gen_

As a prefix of functions indicates that this function is the more general version of the function without the prefix.

ho

“higher-order”, as opposed to first-order. Typically in the context of term matching.

l

• A list.

• Suffix for a variant of a function whose difference is that it operates on a list instead of a single element. E.g: the tactical THENL compared to THEN.

lhs

Left-hand side of an equation.

mk_

“make”, i.e.: create an object from simpler constituents.

prim_

“primitive”. Optional prefix for the name of internal functions that contain most of the implementation. The function without the prefix is a thin wrapper that implements the public interface.

q_ or just q

Optional prefix in the name of a tactical to indicates that it takes a term quotation which is parsed in the context of the goal. Example: qabbrev_tac.

rand

Operand of a combination.

rator

Operator of a combination.

rhs

Right-hand side of an equation.

_rule

Optional suffix to indicate a derived inference rule. Often used for a variant of a conversion that applies the conversion to the conclusion of a theorem. See CONV_RULE.

t

A term.

_tac

Optional suffix for tactics or tacticals.

th

A theorem.

_then

Optional suffix for theorem-tacticals. See the section on tactics in the HOL description manual.

thm

A theorem.

x_

• Optional prefix to indicate a variant that takes a term or quotation. E.g.: The tactical X_GEN_TAC compared to GEN_TAC.

• In a tactical that takes a theorem-tactic and applies it to assumptions, indicates a variant that removes the assumption which was acted on.

1. As of 2022, our automatic testing infrastructure runs one selftest at level 3 each day, and one at level 2, with the latter testing the experimental kernel. Yes, this means that things only in level 3 are not getting tested for the experimental kernel. ↩