HOL4 mode for Visual Studio Code

Support for working with the HOL4 interactive theorem prover in Visual Studio Code. This plugin provides the required functionality to maintain a HOL session in an editor window, basic syntax highlighting, and basic unicode input completion. Everything else — diagnostics, hover, go-to-definition, the outline, symbol search and completion — comes from the HOL language server; see below.

Requirements

Expects a HOL4 installation to exist, and the environment variable $HOLDIR to point to this installation. The HOL4 homepage can be found here and its GitHub repository here.

HOL4 LSP integration

When hol4-mode.lsp.enabled is true (the default), the extension starts a HOL4 Language Server Protocol client that speaks to bin/hol lsp. This delivers:

• Compile-driven diagnostics in the Problems panel and inline squiggles as you edit.
• Hover with type information from the running HOL session, and a theorem's statement when the cursor is on one.
• Outline, symbol search and completion — Ctrl+Shift+O for a file's declarations, Ctrl+T to search stored theorems, and completion of names in scope. Symbol search covers the theories this script loads and, beyond them, any theory built in the project: those are marked not an ancestor, since using one means adding it to Ancestors first.
• Theorem search — Ctrl+H Ctrl+Shift+M, or HOL: Search for theorems in the command palette, asks the theorem database what matches. It prompts for one selector at a time and searches when you submit an empty one, Escape abandoning the search instead. A selector is a theory in single quotes, a fragment of a theorem's name in double quotes, or a term pattern, and several of them narrow rather than widen — so x + 0n = x and then 'arithmetic' asks for that theory's theorems matching the pattern. Two term patterns are as good as one, since both have to hold, and a pattern's free variables are wildcards. The hits arrive as a quick pick that filters as you type; picking one opens the script where it was proved. This is emacs's M-h M-M, and searches statements, where Ctrl+T searches names.
• HOL Goals side pane — press Ctrl+H Ctrl+G to open a pane that follows the cursor and shows the proof state at each tactic step inside a Proof … QED block.

The Ctrl+H prefix, on every platform including macOS

Every HOL command chord starts with Ctrl+H, macOS included. Cmd+H would be the platform-native choice, but it is the key equivalent of Hide on the application menu, and AppKit gets first refusal on it: whenever the chord's when clause does not hold, the window hides instead. That makes a Cmd+H prefix intermittent rather than wrong, which is worse.

The cost is that Ctrl+H is an emacs-style delete backwards in macOS text fields, and the chord shadows it — but only where these bindings are active, which is HOL scripts and the Goals pane. It still deletes backwards everywhere else. To use something else, rebind the prefix in keybindings.json.

Most of these bindings also hold while the Goals pane has focus, not only in a script: they act on the script whose goals the pane is showing. The exceptions are the three that send editor text — starting a session, sending the selection, sending up to the cursor — which need a cursor and so stay confined to the editor.

Positions and the pane width

The server picks its LSP position encoding from what this client advertises, which is utf-16 — so hover, go-to-definition and the squiggles in the Problems panel land on the right characters even on lines carrying ∀, ⇒ or ‘…’, which used to be off by the difference between bytes and code units. Nothing in the extension translates positions any more.

The Goals pane measures its own width and tells the server, so HOL's pretty printer breaks lines to fit the pane you actually have rather than a fixed 75 columns. Resizing the pane re-renders at the new width.

A script whose ancestors will not load is left alone

The server refuses to compile a script that names a theory or library it cannot load — one that has not been built yet, or that raises on load. With an ancestor missing there is nothing to elaborate the file against, so every name the file takes from that ancestor would draw its own error; instead you get one diagnostic, on the Ancestors / Libs entry that named the missing module, and nothing else in the file is compiled. The status bar reads HOL LSP: not compiling and the Goals pane says why rather than reporting "no goal state at this position".

Build the missing dependency with Holmake, then edit the file's Ancestors / Libs header — any change to that list, including a change and its undo — and the server tries again. If the header is already right, HOL: Compile the active script again retries without touching the file.

One server per script

A bin/hol lsp process can serve exactly one theory script for its lifetime. Loading a script's ancestors puts them in the theory graph and seals them, and the seal is a process-global soundness gate against cross-theory redefinition: a second script's ancestors can then be neither re-read nor withdrawn. A shared server does not fail loudly, it answers with wrong goal states and dead hovers.

So the extension starts one server per *Script.sml file, when that file first becomes visible, and stops it when the file is closed. Each server runs in its script's own directory, so it picks up the Holmakefile (and any HOLHEAP) that governs that script.

Two consequences worth knowing:

• Each server loads a HOL heap, which costs a few seconds and a few hundred megabytes. Opening ten scripts at once starts ten of them.
• .sig files and non-script .sml files get no server. They declare no theory of their own, so there is no goal state to show.

Requirements: a HOL4 build recent enough that bin/hol lsp is a valid subcommand. See tools-poly/lsp/README.md in the HOL4 repository for the server contract.

Related settings:

• hol4-mode.lsp.enabled (default: true) — toggle the client entirely. With false the extension behaves as it did before the LSP integration.
• hol4-mode.lsp.executable (default: empty) — override the path to bin/hol. Falls back to hol4-mode.holdir/bin/hol, then $HOLDIR/bin/hol.

Palette commands: HOL: Toggle HOL Goals pane, HOL: Restart LSP server for the active script, HOL: Show LSP output channel for the active script, HOL: Compile the active script again. All but the first, and the status bar item, act on the server belonging to the script in the active editor.

Recording the protocol traffic

A server that misbehaves only under VS Code is a question about what the client asked for and in what order, which no server-side log can answer. Set

"hol4-lsp.trace.server": "verbose"

and every request, notification and reply is written to a HOL4 LSP Trace: <file> output channel, one per server, beside the HOL4 LSP: <file> channel carrying that server's own output. messages names each message without its parameters, which is enough to establish ordering and much shorter. The setting takes effect without a restart, and it is a lot of output, so leave it off otherwise.

The section is hol4-lsp, not hol4-mode: vscode-languageclient resolves it from the client's id, and that id is shared by every server so one setting covers them all.

Extension Settings

There is no longer a hol4-mode.indexing setting. The symbol indexer it governed has been removed: the language server answers the same requests from HOL itself rather than from a regex scan of the sources, so there is one implementation and it is the one that knows what the names mean. Any .hol-vscode directory left in a workspace (or in $HOLDIR) is now unused and can be deleted.

Suggested additions to settings.json for use with VSCodeVim, somewhat corresponding to the HOL4 Vim mode defaults:

        {
            "before": [ "<leader>", "s" ],
            "commands": [ "hol4-mode.sendSelection" ]
        },
    ],
    "vim.normalModeKeyBindings": [
        {
            "before": [ "<leader>", "h" ],
            "commands": [ "hol4-mode.startSession" ]
        },
        {
            "before": [ "<leader>", "<leader>", "x" ],
            "commands": [ "hol4-mode.stopSession" ]
        },
        {
            "before": [ "<leader>", "s" ],
            "commands": [ "hol4-mode.sendSelection" ]
        },
        {
            "before": [ "<leader>", "<leader>", "s" ],
            "commands": [ "hol4-mode.sendUntilCursor" ]
        },
        {
            "before": [ "<leader>", "y" ],
            "commands": [ "hol4-mode.toggleShowTypes" ]
        },
        {
            "before": [ "<leader>", "a" ],
            "commands": [ "hol4-mode.toggleShowAssums" ]
        },
        {
            "before": [ "<leader>", "c" ],
            "commands": [ "hol4-mode.interrupt" ]
        }
    ]
}

Known Issues

• Syntax highlighting is lacking. Logical terms are especially bad. The situation could be improved by implementing a HOL language server.
• There is some hacky code that attempts to strip ML comments from input that is being sent to HOL. Currently, this does not properly deal with nested comments, or comment tokens that exist within string literals.
• Comments are not stripped from tactic text.
• load calls are not inserted when calls to qualified ML code is made.
• Location pragmas are not inserted at calls to {Co}Inductive, Datatype, Theorem, nor in term quotations.
• Symbol search reaches only theories that have been built; a script never compiled by Holmake contributes only the declarations of the buffers you have open.
• .sig files and library .sml files get no IDE features: the server binds to one theory script per process.