NOTE: This project is moved to https://github.com/hol-light/hol-light-web. This repository will not be maintained.

HOL Light in the browser via js_of_ocaml

This directory is an experiment in running HOL Light in JavaScript using js_of_ocaml. All the moving pieces from hol.sh (the OCaml toplevel, camlp5 with HOL Light's backquote syntax, zarith big integers, the full hol_lib) end up linked into a single .js bundle that runs unmodified in node and in modern browsers.

The browser demo (index.html + hol_top_worker.js) loads HOL Light into a Web Worker so the UI stays responsive during the ~1–2 minute kernel bootstrap, and stdout/stderr stream live to the page as Format buffers flush — same hook jsoo's own lwt_toplevel example uses.

Run it without building

The site/ directory in this repo is pre-built and self-contained — just serve it. No opam, no make, no compiler:

python3 -m http.server -d site 8000
# then open http://localhost:8000/

You only need the "Build" section below if you want to rebuild the bundle (e.g. you edited hol_top_worker.ml or want to bump the parent HOL Light version).

Whoever rebuilds site/ should update the commit hash of HOL Light in the sidebar link in index.html (search for "Built from" to find it).

What's here

Hand-written sources

These files are the actual contributions of this directory; they live in git and are what you edit:

Current patches

Note: update_database.ml is not shipped to site/ (excluded in the Makefile) and is not loaded by the worker. Under HOLLIGHT_USE_MODULE=1 the env walker has to round-trip every candidate name through the typechecker, which makes search unusably slow in the browser. Users who want it can paste loadt "update_database.ml";; themselves.

Refreshing a patch after upstream churn

If make site reports PATCH FAILED: patches/foo.ml.patch:

# 1. Mirror the latest parent file untouched, then apply the old patch
#    by hand, fix any rejects, and regenerate the .patch file.
cp ../foo.ml /tmp/foo.ml.orig
cp /tmp/foo.ml.orig /tmp/foo.ml.new
# ... edit /tmp/foo.ml.new to re-introduce the hook ...
diff -u /tmp/foo.ml.orig /tmp/foo.ml.new \
  | sed 's|/tmp/foo.ml.orig|a/foo.ml|; s|/tmp/foo.ml.new|b/foo.ml|' \
  > patches/foo.ml.patch
make site   # should now apply cleanly

Generated artefacts

These are produced by make. Most are excluded from git (see .gitignore); the exception is site/, which is checked in pre-built so the demo runs without building anything (see "Run it without building" above).

Build

This directory must live inside a checkout of jrh13/hol-light — ideally cloned as hol-light-web/. The Makefile links the parent tree's bignum.cmo, hol_loader.cmo, hol_lib.cmo, and pa_j.cmo directly (see HOL := .. in Makefile), and make site rsyncs the parent's .ml sources into site/.

Prerequisites:

1. Parent switch + hol_lib.cma. The worker bundle links the parent's .cmos directly, so the parent tree's opam switch must exist and hol_lib.cma must have been built at least once:

   cd ..
   make switch-5
   eval $(opam env --set-switch)
   export HOLLIGHT_USE_MODULE=1
   make            # one-time, in the parent tree
   cd hol-light-web
   

2. Extra opam packages for jsoo (the parent switch doesn't install these by default):

   opam install -y js_of_ocaml js_of_ocaml-toplevel zarith_stubs_js
   

   js_of_ocaml provides the compiler and runtime, *-toplevel provides JsooTop (the in-bundle REPL machinery), and zarith_stubs_js ships the JS implementation of zarith's C primitives. The other packages this Makefile pulls in (zarith, camlp5, fmt, pcre2, camlp-streams) come along with make switch-5 and the parent build.

Then, from this directory:

Try it

For the browser demo, open http://localhost:8000/ after make serve.

The page boots the Worker immediately and shows the kernel's bootstrap output (the 0..0..1..solved at N lines) live in the terminal pane. Once * HOL-Light syntax in effect * and the printer-install lines appear, the input is enabled and you can type phrases.

Don't open index.html directly via file://. Browsers treat every file:// URL as a unique origin and refuse to construct a Web Worker from one (SecurityError: Failed to construct 'Worker': … cannot be accessed from origin 'null'). Always serve the directory over HTTP — make serve handles this, or run python3 -m http.server -d site 8000 against an already-built site/ and open http://localhost:8000/. Once deployed to GitHub Pages / Netlify the constraint goes away because the page is served over https://.

Deploy

The make commands produce a self-contained site/ directory you can upload to GitHub Pages, Netlify, or any other static host:

site/
├── index.html, hol_top_worker.js                   (Web/ outputs)
├── 100/, Library/, Multivariate/, Probability/, …  (HOL Light .ml sources)
├── *.ml                                            (kernel sources)
└── …

The layout mirrors the parent HOL Light tree, so loadt "Library/words.ml" resolves to <origin>/Library/words.ml over plain HTTP — see the next section.

make site excludes the opam switch, build artefacts (*.cmo, *.byte, checkpoints, native binaries), and a few sub-projects that aren't needed at proof-load time (TacticTrace, UnitTests, Proofrecording, ProofTrace, Minisat, Cadical, mcp, pa_j/, update_database/, *.ckpt). Everything else from the parent tree comes along.

Caveats / known gotchas

• First-load cost. ~140 s in node v22 to bootstrap the whole kernel (vs ~33 s native bytecode). After that, individual proofs run at jsoo speed. A make-checkpoint-style serialized image would skip the bootstrap; Marshal works under jsoo so that is feasible.
• No Unix. Filesystem reads (Sys.file_exists, open_in, loadt) are served by Sys_js.mount + sync XHR (see "How loads/loadt/needs work" above), so plain .ml loads work. But anything that needs Unix proper — fork, sockets, file metadata beyond Sys.file_exists — won't.
• .cma loading is not wired up. Only .ml sources can be loaded at runtime. Loading additional .cmas would require Dynlink-on-jsoo; for now the only way to get extra modules into the bundle is to link them into hol_lib.cma ahead of time.
• Memory. node --max-old-space-size=8192 … is recommended for bigger proofs; the default 4 GiB is sometimes tight.
• pcre2 stubs are shims; if camlp5 ever lexes an OCaml {%foo|…|} quoted-extension the match call will throw a Failure we can detect.

How things work

How loads/loadt/needs work

HOL Light's loadt "Library/words.ml" (and loads, needs) read .ml files off disk and feed them through the toplevel. Under jsoo there is no disk — so we synthesize one out of Sys_js.mount plus synchronous XHR.

The wiring, all in hol_top_worker.ml:

1. Sys_js.mount ~path:"/" hol_fs_handler — when the OCaml runtime tries Sys.file_exists "/Library/words.ml" or open_in "/Library/words.ml" and the file isn't already in the in-memory FS, jsoo calls hol_fs_handler with the path, which runs a synchronous XMLHttpRequest GET /Library/words.ml. Sync XHR is allowed inside Web Workers (only deprecated on the main thread), so loadt's assumption that file reads are synchronous is satisfiable. The fetched bytes get cached in the in-memory FS, so Digest.file works (HOL Light's loaded_files de-dup) and re-loadt is a no-op.
2. Hol_loader.hol_dir := "/" — HOL Light's default load_path is ["."; "$"], with $ substituted by !hol_dir. Pointing it at / means loadt "Library/words.ml" resolves to /Library/words.ml, which our handler then fetches over HTTP.
3. Hol_loader.file_loader := (fun fname -> ...) — the worker installs a custom loader that reads the (now cached) file and calls JsooTop.use Format.std_formatter on its contents. That runs each ;;-terminated phrase through the same toplevel as the REPL, so camlp5's backquote syntax extension is in effect for loaded files.

Net effect: with the deployed site/ layout, you can paste

loadt "Library/words.ml";;

into the REPL and the worker will fetch the source from <origin>/Library/words.ml, evaluate it phrase by phrase with output streaming live, and remember it so subsequent needs/loadt calls short-circuit.

(Limits: only .ml sources work — loadt "foo.cma" would need Dynlink-style support, not yet wired up. And anything loadt's file ends up referencing must also be reachable under the deploy root.)

How the printers get installed

The browser toplevel doesn't run hol.ml, so HOL Light's printer registrations there don't fire. After the kernel finishes loading, the worker emits these phrases via JsooTop.execute so the toplevel resolves the names against the just-opened Hol_lib environment:

open Hol_lib;;
#install_printer pp_print_num;;
#install_printer pp_print_fpf;;
#install_printer pp_print_colored_qterm;;
#install_printer pp_print_colored_qtype;;
#install_printer pp_print_colored_thm;;
#install_printer pp_print_colored_goal;;
#install_printer pp_print_colored_goalstack;;

The colored variants emit raw ANSI escape sequences (e.g. \x1b[36m for types, \x1b[31m for invented type variables); index.html translates them to <span class="ansi-N">…</span> on the page side.

How the camlp5 trick works

Without camlp5, the in-browser OCaml parser refuses identifiers like ARITH_TAC in expression position.

1. Static-link camlp5o.cma (which already bundles Pcaml/Grammar/Camlp5_top_funs) plus pa_j.cmo into the bytecode that becomes the JS toplevel.
2. Provide JS stubs for pcre2's C primitives (camlp5 imports pcre2 for its Quotedext lexer). HOL Light never triggers that path, so the stubs need only be no-ops.
3. Pass the assembled bytecode through js_of_ocaml --toplevel --export export.txt, including the right -I directories so jsoo embeds Hol_lib's CMI alongside Stdlib's.

The * HOL-Light syntax in effect * banner now prints inside the JavaScript runtime, and g \...`;; e ARITH_TAC;; top_thm()` works end-to-end.

How streaming works

hol_top_worker.ml opens four Sys_js channels (stdout, stderr, /dev/sharp, /dev/caml) and registers a flusher on each that calls Worker.post_message ({kind:"out", stream, text}). The flushers are installed before JsooTop.initialize, so even the kernel's bootstrap output (~140s of "solved at N" lines) reaches the page as it's produced.

index.html listens for these messages and appends them to the output <pre> with a CSS class per stream. Because all of this happens on the main thread, the page can repaint between flushes — the browser feels responsive even while the worker is busy.