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. ↩

Overview

The HOL manuals (Description, Tutorial, ...) are built from a single set of .smd source files into two different formats:

• A PDF via pandoc + latexmk, for archival / cite-able use.
• An mdbook HTML site via mdbook, for online browsing.

Both formats are driven by the same .smd ("scripted markdown") source files, which are an extension of CommonMark. The extensions are interpreted by the polyscripter tool, which runs an embedded Poly/ML session to evaluate HOL fragments inline and splice their pretty-printed output back into the document.

This document is the developer-facing reference for the authoring pipeline. It is concerned with how to write and build a manual; the content of each manual is the responsibility of its individual chapters.

Per-manual file layout

A manual lives in its own subdirectory of Manual/ (Manual/Description/, Manual/Tutorial/, ...). Inside, the moving parts are:

All generated files are listed in .gitignore and EXTRA_CLEANS.

The mdbook page template (index.hbs) and stylesheet overrides (custom.css) live in Manual/theme/, shared by every manual via theme = "../theme" in each book.toml. The pandoc Lua filter (pdf-macros.lua, e.g. HOL → smallcaps) lives in Manual/Tools/, referenced from each Holmakefile as ../Tools/pdf-macros.lua.

Canonical sources of truth

• The manual's title lives in book.toml's title = "...". The mdbook menu bar and HTML <title> consume it directly. The SUMMARY.md rule and the book-title.tex rule both extract it with a one-line awk invocation, so the PDF cover (title.tex via \HOLbookTitle) and the hyperref pdftitle stay automatically in sync. Renaming the manual is therefore a single-line edit to book.toml.
• The chapter ordering lives in chapters.txt. Top-level (unindented) lines are chapters; indented lines are nested sub-files of the most recent top-level stem. Blank and #-comment lines are ignored. gen_chap_lists reads it twice — once to emit SUMMARY.md (the mdbook sidebar) and once to emit chapters-include.tex (the LaTeX \include block).
• The chapter content lives in <chapter>.smd. Top-level chapters start with # Title (H1), which becomes a \chapter{} in the PDF and the page title in mdbook. Nested sub-file chapters start with ## Title (H2) and become \section{} in the parent's \input{<stem>}.

The .smd format

An .smd file is CommonMark plus polyscripter directives. The polyscripter reference lives in Manual/Tools/README; the high-level summary:

• Lines starting with >> (after stripping leading whitespace!) are HOL inputs. Variants: >> (run + show I/O), >>_ (show input, elide output), >>__ (silent), >>- (run, show output only), >>+ (run; tolerate an unhandled exception).
• Lines starting with ##xxx are inline commands: ##thm, ##eval, ##assert, ##parse, ##use, ##linelen_limit, etc.
• Anything else is plain CommonMark.

Two raw-block flavours let a chapter target one renderer specifically:

 ... HTML/Markdown-only content, dropped by pandoc ...

Use these for diagrams (e.g. \begin{picture} / \begin{tikzpicture} for the PDF) and their mdbook equivalents (descriptive prose, <pre> blocks, ...).

Math macros that need to render on both sides

LaTeX \newcommands in the driver .tex or in commands.tex exist for the PDF only; MathJax in mdbook doesn't see them. For any math command that appears inside $...$ or $$...$$ in chapter prose, both sides must declare it:

• PDF side: a \providecommand{...} in a {=latex} raw block at the top of the chapter. YAML header-includes: does not survive pandoc -t latex and is silently discarded — use the raw block.
• mdbook side: a matching entry in Manual/theme/index.hbs's MathJax Macros table.

See Manual/Tutorial/combin.smd's top-of-file block and Manual/theme/index.hbs's con/KC/SC/mathpredn entries for a worked example.

The shared smdpp Poly/ML session

smdpp runs one Poly/ML session that processes every chapter in chapters.txt order. Anything a chapter does to global state — load "X", overload changes, Globals.show_X := true, custom pretty-printers — leaks forward into later chapters.

This is normally what you want (later chapters can rely on earlier Datatype: definitions, etc.), but it has two specific gotchas worth highlighting:

• Overload leakage. load "intLib" in one chapter makes */+ overloaded for int as well as num for every later chapter, which can make polymorphic definitions ambiguous and break metis_tac searches that were fine in isolation. The fix is to bracket the affected chapter with a grammar save/restore against a pristine theory's grammar:

  >>__ val euclid_initial_grammars =
          (Parse.type_grammar(), Parse.term_grammar());
  >>__ Parse.temp_set_grammars $
          valOf $ grammarDB {thyname="numeral"};
  
  ... chapter body ...
  
  >>__ Parse.temp_set_grammars euclid_initial_grammars;
  

  See Manual/Tutorial/euclid.smd for a worked example.

• Global flag persistence. set_trace "show_X" 1 or show_assums := true similarly stays set for every subsequent ##thm/##eval. Always pair the enable with a matching reset at the end of the relevant block.

Both gotchas are invisible in the per-chapter pipeline (Holmake <chapter>.md starts a fresh polyscripter session per chapter). Always rebuild via Holmake mdbook before assuming a translated chapter is healthy.

Display-only HOL code (>> inside non-running blocks)

polyscripter strips leading whitespace before checking the directive prefix. A line >> mp_tac (...) inside a fenced code block intended for display only is still parsed as a >> directive and executed against the live goalstack — almost always with a confusing error.

The workaround is to emit the display block as parallel {=latex} / {=mdbook} raw blocks whose lines begin with \verb+ (PDF) or <pre> + >> HTML entities (mdbook), so neither side has >> at line start. See the EUCLID box in Manual/Tutorial/euclid.smd for the pattern.

\cite{} and bibliography

Both pipelines resolve \cite{key} against the manual's .bib file, in a Chicago-author-date house style.

• The author writes \cite{Foo:2020} (or \citep/\citet variants) literally in the .smd source.
• mdbook side: the Holmakefile runs smdpp render-bib <manual>.bib ../Tools/csl/chicago-author-date.csl $(SMDS), which delegates to pandoc --citeproc and produces two sidecar artefacts:
  • references.md — the rendered bibliography chapter. Hook it into the sidebar by listing references as the last entry in chapters.txt; gen_chap_lists latex-include is hard-wired to skip that stem on the PDF side (natbib handles bibliographies there).
  • cite-labels.tsv — preprocessor-time lookup mapping each cite key to its rendered label (e.g. Foo:2020 → (Foo 2020)). smdpp's \cite pass reads this and rewrites in-prose \cite{Foo:2020} to a link into references.html.
• PDF side: natbib [authoryear,round] plus \let\cite\citep in the driver .tex renders the bibliography directly from the same .bib, sharing the Chicago-author-date style with the mdbook through the CSL the smdpp pass uses.

Per-manual moving parts:

• <manual>.bib — the BibTeX database (hand-edited; the same file feeds both pipelines).
• chapters.txt lists references as the last entry so mdbook picks up the bibliography chapter.
• Holmakefile's references.md cite-labels.tsv rule runs smdpp render-bib; both outputs are listed in EXTRA_CLEANS.
• The shared CSL lives at Manual/Tools/csl/chicago-author-date.csl and is the source of truth for the mdbook citation style.

Building a single manual

From the manual's directory:

The two top-level targets (mdbook and <manual>.pdf) are the gating checks before committing.

The unified manual site

All manuals are also served as a single mdbook-style site under Manual/book/, with a top-level lander, a cross-manual switcher strip above each manual's menu bar, and a unified search index that queries every manual.

Top-level layout

Each per-manual book.toml references the shared theme and the searcher:

[output.html]
theme = "../theme"
additional-css = ["custom.css"]
additional-js = ["hol-searcher.js"]

custom.css and hol-searcher.js in each manual's directory are symlinks to ../theme/<file>. mdbook copies additional-* entries by URL-path rather than following filesystem relative paths, so the symlinks keep a single source of truth in Manual/theme/.

Cross-manual references

• \ref{Book:label} — resolves to the URL of \label{label} in Book (e.g. ../Description/system.html#some-anchor). Each manual's Holmakefile runs ../Tools/smdpp dump-labels . to produce labels.tsv, a sidecar that maps every \label{...} and heading slug to its rendered URL. Every manual's mdbook target lists every other manual's labels.tsv as a prerequisite, so siblings are built first and resolutions are cross-checked at preprocess time.
• \refentry{Foo.bar} — resolves to the URL of the corresponding Reference entry (../Reference/Foo.bar.html). Manual/Reference/entries.list is the canonical "what entries exist" file; smdpp loads it at startup and dies on an unknown name.

Cross-manual search

hol-searcher.js walks window.HOL_MANUALS.books (set in index.hbs's <head>), loads each book's searchindex.js into its own Elasticlunr index, queries them all on each keystroke, and groups results by book with the current book first.

mdbook hashes the filename of each book's emitted searchindex.js (it's content-addressed), so cross-book loads can't reference the hashed name directly. Each per-manual Holmakefile's mdbook target therefore ends with

cd ../book/<Manual> && \
  ln -sf $$(ls searchindex-\*.js | head -1) searchindex.js

to provide a stable, predictable name for the searcher to load.

Building and serving the unified site

From Manual/ (not from inside any specific manual's directory):

Holmake mdbook from Manual/ is the gating check before committing changes that touch more than one manual (cross-book \\ref{...}, theme/template tweaks, etc.); the per-manual Holmake mdbook doesn't exercise the cross-book references.

Adding a new chapter

1. Write <stem>.smd. If the chapter is a top-level entry, start with # Title; if it is a nested sub-file, start with ## Title.
2. Add the stem to chapters.txt in the desired position. Indent for nested sub-files.
3. Add per-chapter <stem>.md / <stem>.tex rules to the Holmakefile, following the existing pattern (most chapters use $(PS\_NOUMAP) for .md and $(PANDOC\_MD) for .tex).
4. Add <stem>.md and <stem>.tex to .gitignore and the EXTRA\_CLEANS list.
5. Run Holmake mdbook and Holmake <manual>.pdf to verify both pipelines.

Adding a new manual

1. mkdir Manual/<NewManual> and copy book.toml and a minimal Holmakefile from Manual/Tutorial/ as a starting template. (The mdbook theme is shared from Manual/theme/, picked up automatically via the theme = "../theme" line in the copied book.toml; the pdf-macros.lua pandoc filter is shared from Manual/Tools/ and referenced from the copied Holmakefile as ../Tools/pdf-macros.lua.)

2. Edit book.toml's title and description (the description shows up on the lander card emitted by gen\_lander); set build-dir = "../book/<NewManual>"; add an entry for the new manual to the PORTS table in Manual/Tools/mdbook-preview.py (3000–3006 are taken; 3002 is the unified site).

3. Symlink the shared theme assets into the manual directory:

   cd Manual/<NewManual>
   ln -s ../theme/custom.css custom.css
   ln -s ../theme/hol-searcher.js hol-searcher.js
   

4. Write <NewManual>.tex (or manual.tex) as the LaTeX driver; both use \\HOLbookTitle from the auto-generated book-title.tex.

5. Populate chapters.txt and add the chapters per the previous section.

6. Wire the new manual into the unified site:

   • Add '<NewManual>' to window.HOL\_MANUALS.books in Manual/theme/index.hbs.
   • Add a <a data-hol-manual="<NewManual>"> link to the manual-switcher strip in the same template.
   • Add Manual/<NewManual>/book.toml to the book/index.html recipe's gen\_lander argument list in Manual/Holmakefile.
   • Add <newmanual>-mdbook as a .PHONY target and a prereq of the aggregate mdbook target in Manual/Holmakefile.
   • Add ../<NewManual>/labels.tsv to every sibling manual's mdbook target prerequisites so cross-book \\ref{<NewManual>:...} resolves in either direction.

Related reference docs

• Manual/Tools/README — exhaustive polyscripter directive reference (>>/##xxx semantics, prompt sizing, expected-failure handling, ...).
• Manual/Guide/ — style guidance for writing HOL documentation prose.
• Manual/LaTeX/commands.tex — shared LaTeX macros (\\HOL, \\ml, \\holtxt, \\theoryimp, ...) available to every manual's PDF build.
• Manual/Description/desc-unicode.sty — \\DeclareUnicodeCharacter table covering the Unicode codepoints HOL's pretty-printer emits. Shared by both Description and Tutorial via \\usepackage{../Description/desc-unicode}.

LSP server

The Language server protocol is a standard protocol by Microsoft used for communicating between "language servers" which provide contextual language-specific information about files and "clients" or text editors. LSP client implementations exist for VSCode, Vim, Emacs among others so this makes a convenient common point for implementing HOL specific behaviors.

Usage

TODO The server does not yet handle multiple files as well as it could

To start a server, use hol lsp. This should be run in the project root (containing the files you are editing).

It will communicate using the LSP format (on stdio). This covers most of the basic operations of a language server, in particular:

• Initialization/shutdown
• Opening, modifying, closing files
• Hover and go to definition

Initialization

The client sends a message describing the features it supports, and the LSP server responds by describing what features it has enabled.

This LSP server also supports the $/setConfig command for setting additional HOL-specific features.

File operations

When opening or modifying a file, the server will compile the file and report any warnings or errors in a Diagnostic notification. It is also responsible for caching intermediate states in order to minimize the amount of work needed to update the list of diagnostics.

Extensions

In addition to the usual LSP commands, the server supports the following extensions:

• Notification $/cancelRequest:

  This is a "standard" extension that allows cancelling a pending request. This is useful in particular for the $/eval command to terminate a long-running user evaluation.

  Parameters:

  • id: integer | string - The request id to cancel

• Request $/setConfig: This sets additional global state for the server.

  Parameters:

  • elabOn?: ElabOn where enum ElabOn { None = 0, Change = 1, Save = 2 } (default: Change)

    This controls whether elaboration/compilation should be triggered after every modification to the file, on save, or not at all.

• Request $/eval: This runs a chunk of HOL text, to allow for a similar behavior as hol repl.

  Parameters:

  • uri: URI - The file (or virtual path) associated to this chunk
  • code: string - The HOL text to compile
  • incr?: Incr where enum Incr { None = 0, Chunk = 1, Stream = 2 } (default: None)
  • holdep?: HoldepKind where enum HoldepKind { None = 0, Quiet = 1, List = 2 } (default: Quiet) - controls whether it should first call holdep to collect and preload any opens and other qualified names, and whether to print bindings (List) or not (Quiet).

  Depending on the options set, it will send various notifications back, in the following order:

  • If holdep = List, it will give a $/eval/holdep notification:

    • uri: URI - the original file
    • id: integer | string - the current request
    • files: [string] - The list of modules to load

  • It then loads the modules (if holdep != None).

  • If holdep = List, it will give a $/eval/holdepCompleted with the same uri,id when loading is complete

  • It then runs the code and reports results:

    • If incr = None, then the final response of the request is a [report] list containing all of the errors, warnings, etc.
    • If incr = Chunk, then it returns null immediately, but it compiles asynchronously, sending each report in a $/eval/P notification:
      • id: integer | string - the current request
      • pos: Range - the chunk of the text that was evaluated
      • out: [Report] - the results from this chunk
    • If incr = Stream then each report is sent as soon as possible in a $/eval/1 notification:
      • id: integer | string - the current request
      • out: Report - the report

  The Report object is a possible output of the compiler:

  type Report = ErrorReport | CompilerOutReport | ToplevelOutReport | CompileProgressReport | { kind: "compileCompleted" } | { kind: "interrupted" };
  interface ErrorReport {
    kind: "error";
    hard: bool; // true = error, false = warning
    pos: Range;
    msg: string;
  }
  interface CompilerOutReport {
    kind: "compilerOut";
    pos: Range;
    body: string;
  }
  interface ToplevelOutReport {
    kind: "toplevelOut";
    pos: Range;
    body: string;
  }
  interface CompileProgressReport {
    kind: "compileProgress";
    pos: Range;
  }
  

  An asynchronous compile is always terminated by "compileCompleted" or "interrupted".

• The $/compileProgress notification is sent during an asynchronous compile caused by a file open or modification event.

  • uri: URI - the file being compiled
  • pos: Range - the chunk of the text that was evaluated

• The $/compileCompleted notification is sent when an asynchronous compile caused by a file open or modification event is completed.

  • uri: URI - the file being compiled

• The $/compileInterrupted notification is sent when an asynchronous compile caused by a file open or modification event is interrupted.

  • uri: URI - the file being compiled

• TODO unimplemented; this is an API proposal

  $/getState request to get the current goal view state:

  • uri: URI - the file being compiled
  • pos: Range - the selection

  The response is either null if it is not in a proof, or an object containing:

  • tactic: Range
  • goals: [Goal] where struct Goal { asms: [string], concl: string }

  goals contains the list of goals that would be operated on by a tactic at this position.