Conversation
* mcp: add MCP server for HOL Light with structured proof tools
FastMCP stdio server for LLM-assisted theorem proving. Embeds HOL
Light as a subprocess with OCaml-side JSON serialization for
structured goal states.
Tools:
- eval: raw OCaml/HOL Light evaluation
- set_goal: set proof goal, return JSON goal state
- goal_state: inspect current goals as JSON
- apply_tactic: apply tactic, return new state or proved theorem
- backtrack: undo N tactic steps
- search_theorems: search by name, return JSON results
- hol_type: get the type of a term
- hol_load: load a HOL Light file via needs
Features:
- DMTCP checkpoint support for instant startup (~2s vs ~75s)
- 14-check MCP smoke test + 12 unit tests
- OCaml helpers (mcp_helpers.ml) for JSON serialization
- Auto-detects checkpoint, falls back to cold start
Docs:
- README: setup, quick start, checkpointing, related work
- TUTORIAL: 6 worked proof examples of increasing difficulty
- SKILL: LLM tactic reference and proof patterns
* mcp: add hol_interrupt, named checkpoints, config file, ARM tutorial
New features:
- hol_interrupt tool: sends SIGINT to cancel hung tactics
- Named checkpoints: make_checkpoint.py --name <name> creates
hol-<name>.ckpt/, allowing multiple checkpoints (e.g. base, s2n)
- hol-mcp.toml config file: set checkpoint name and timeout,
auto-discovered in CWD or passed via --config
- Configurable timeout via config or HOL_TIMEOUT env (default 600s)
Docs:
- Security considerations section in README
- s2n-bignum ARM proof examples in TUTORIAL (simple, branch, loop)
- ARM tactic reference in SKILL.md
- kceren acknowledgment in README
Fixes:
- Smoke test updated for hol_interrupt (14/14 passing)
- .gitignore wildcards hol-*.ckpt
* mcp: use ephemeral coord port for dmtcp_restart
Pass --coord-port 0 so each server instance gets its own
coordinator port, allowing multiple instances to run in parallel
instead of failing with broken pipe when port 7779 is taken.
* mcp: add hol_restart tool for recovering from dead subprocess
Kills the existing HOL Light process, resets state, and starts a
fresh one. Useful when the subprocess dies mid-session instead of
requiring a full MCP server restart.
* mcp: add hol_status tool and per-call timeout
- hol_status: reports alive/dead, pid, checkpoint name, uptime, and
default timeout — useful for diagnosing issues without eval
- Per-call timeout: eval and apply_tactic accept an optional timeout
parameter (seconds) that overrides the global default, so slow
tactics like ARM_STEPS_TAC can get more time without raising the
global timeout for everything
* mcp: add tests for hol_status, hol_restart, and per-call timeout
* mcp: update smoke test, docs, and acknowledgments for new tools
- smoke_test.py: add checks for hol_status, hol_restart, per-call
timeout, and post-restart eval; update expected tool list to 11
- README.md: add hol_restart and hol_status to tools table, update
acknowledgments
- SKILL.md, TUTORIAL.md: add hol_status and hol_restart to workflow
* mcp: add hol_help tool, Agent Skills frontmatter, update docs
- Add hol_help tool that serves SKILL.md directly from the MCP server,
eliminating the need for separate skill installation or agent config
- Set FastMCP instructions to hint the LLM to call hol_help()
- Add Agent Skills frontmatter (name/description/compatibility) to
SKILL.md per the agentskills.io specification
- Update README: tools table, skill section, acknowledgments
- Update smoke test for new tool (12 tools total)
- Update SKILL.md and TUTORIAL.md workflow sections
* mcp: default hol-mcp.toml checkpoint to noledit
Matches the code's hardcoded fallback so the shipped config and
server agree out of the box.
This looks like a typo to me, but I am not 100% sure.
Compacts the OCaml heap before taking the DMTCP snapshot. Reduces bare HOL Light checkpoint size from 511M to 306M (~40%).
…rh13#162) * mcp: faster eval, fix locking, add prove/apply_tactics tools Speed up MCP eval round-trips, fix threading issues, and add convenience tools for one-shot and batch proofs. Performance: - Queue-based sentinel signaling: replace 50ms polling loop with queue.Queue. Reader thread produces results, _wait_for_sentinel consumes via queue.get(). Near-zero latency per eval call. - Single round-trip for apply_tactic and set_goal (was 2 sequential _eval_raw calls each). - Buffer-based OCaml JSON serialization in mcp_helpers.ml, replacing O(n^2) string concatenation with O(n). Robustness: - queue.Queue eliminates race condition between _eval_raw clearing state and reader thread setting it (atomic consumption). - Dead process detection: reader thread puts error on queue at EOF, so callers get immediate feedback instead of hanging for 600s. - hol_interrupt now holds _lock, preventing races with hol_restart. New tools: - prove(goal, tactic): one-shot proof via HOL Light's prove(). - apply_tactics(tactics): batch tactic application in a single round-trip via new OCaml helper mcp_json_apply_tactics. Stops at first error or proof completion, returns step count. Docs: - Update README tools table with prove and apply_tactics. - Update SKILL.md and TUTORIAL.md workflow sections to document all 14 tools including hol_type, hol_load, hol_interrupt, and hol_help. Tests: - 35 unit tests (tool-level coverage for all 14 tools). - 25 smoke tests. * mcp: document --config, expose config path in hol_status - hol_status now includes "config" field showing the absolute path of the loaded hol-mcp.toml (or null if using defaults). - Update README to state the default config path explicitly: /path/to/hol-light/mcp/hol-mcp.toml. - Update hol-mcp.toml comments to match. - Update Kiro CLI example to show --config with absolute path. * typos
This is in effect performing multiplication in GF2[X], using the
bits of a machine word to represent polynomial coefficients in
a quite standard way (little-endian: LSB = constant term). It
has generic word sizes `word_pmul:M word->N word->P word`, so it
can be used as a target for modeling different variants supported
by CPUs or just used in other settings. There is an associated
evaluation conversion WORD_PMUL_CONV that is included in the
usual WORD_RED_CONV / WORD_REDUCE_CONV suite, as well as a
bitwise conversion BIT_WORD_PMUL_CONV. New definition:
word_pmul
new theorems:
BITVAL_BIT_WORD_PMUL
BIT_WORD_PMUL
BIT_WORD_PMUL_ALT
WORD_CLZ_USHR
WORD_CTZ_SHL
WORD_PMUL_0
WORD_PMUL_POW2
WORD_PMUL_STEP
WORD_PMUL_SYM
WORD_PMUL_XOR
WORD_PMUL_ZX
WORD_SHL_AS_USHR
WORD_USHR_AS_SHL
and conversions:
WORD_PMUL_CONV
BIT_WORD_PMUL_CONV
…ized by Claude Opus 4.6 in "100/green.ml". The proof is based on the Cauchy transform as a left inverse of the Wirtinger d-bar derivative operator. This approach, avoiding any approximation or subdivision arguments while allowing quite general path parametrization, was inspired by Kostya_I's answer here: https://mathoverflow.net/questions/307713 The technique is rooted in the Cauchy transform / dbar framework of Ahlfors, "Lectures on Quasiconformal Mappings" (1966, 2nd ed. 2006), and appears in Bonk's UCLA complex analysis lecture notes, Ch. 20: https://www.math.ucla.edu/~mbonk/complana.pdf The primary versions use complex infrastructure in the statements. More traditional (but verbose) real-analytic variants of the Green theorem and area formulas are derived as easy consequences, e.g. GREEN_THEOREM_CURL = |- f g u. g absolutely_continuous_on interval[vec 0,vec 1] /\ pathfinish g = pathstart g /\ (!z. z IN inside(path_image g) ==> winding_number(g,z) = Cx(&1)) /\ open u /\ inside(path_image g) UNION path_image g SUBSET u /\ f differentiable_on u /\ (!h:real^2. (\z. frechet_derivative f (at z) h) continuous_on u) ==> (\z. lift(frechet_derivative f (at z) (basis 1) $1 - frechet_derivative f (at z) (basis 2) $2)) integrable_on inside(path_image g) /\ (\t. lift(f(g t)$2 * vector_derivative g (at t) $1 + f(g t)$1 * vector_derivative g (at t) $2)) integrable_on interval[vec 0,vec 1] /\ integral (interval[vec 0,vec 1]) (\t. lift(f(g t)$2 * vector_derivative g (at t) $1 + f(g t)$1 * vector_derivative g (at t) $2)) = integral (inside(path_image g)) (\z. lift(frechet_derivative f (at z) (basis 1) $1 - frechet_derivative f (at z) (basis 2) $2)) Used the Green area formula from this development to replace around 1k lines of ad-hoccery in "100/isoperimetric.ml" with a simple corollary. As a side-effect, added a number of general lemmas to the Multivariate libraries, notably some results on absolutely continuous paths including the winding number integral HAS_PATH_INTEGRAL_WINDING_NUMBER_AC, a complement to HAS_PATH_INTEGRAL_WINDING_NUMBER with non-comparable hypotheses: ABSOLUTELY_CONTINUOUS_IMP_PATH ABSOLUTELY_CONTINUOUS_IMP_RECTIFIABLE_PATH ABSOLUTELY_CONTINUOUS_JOINPATHS ABSOLUTELY_CONTINUOUS_REVERSEPATH ABSOLUTELY_INTEGRABLE_VECTOR_DERIVATIVE_ABSOLUTELY_CONTINUOUS CEXP_LIPSCHITZ_BOUNDED HAS_PATH_INTEGRAL_WINDING_NUMBER_AC LEBESGUE_MEASURABLE_SING LSPACE_ALT LSPACE_SUBSET MEASURABLE_ON_CLOG MEASURABLE_ON_CPOW NEGLIGIBLE_REAL Added a smaller new example autoformalized by Claude Opus 4.6, Conway's "Doomsday Algorithm" for finding the weekday for a given (valid Gregorian) date: "Examples/doomsday.ml". The overall correctness theorem is: DOOMSDAY_ALGORITHM_CORRECT = |- !y m d. valid_date(y,m,d) ==> doomsday_algorithm y m d = day_of_week y m d Added a documentation file for the new "mapi" function introduced as part of the METIS restructuring.
…timing (jrh13#163) * mcp: structured JSON from eval/hol_load, output truncation, built-in timing eval now returns structured JSON: {success, output, output_truncated, full_output_chars, time_seconds} Large outputs are truncated to max_output_chars (default 4000, configurable in hol-mcp.toml and per-call). hol_load now returns quiet structured JSON: {success, file, time_seconds} (plus error on failure) Intermediate val bindings are suppressed. Use eval with needs for verbose output. Built-in timing on all eval/hol_load calls via _eval_raw returning (output, elapsed_seconds) tuples. Also: add hol_interrupt smoke test (all 14 tools now covered), bump all deps (mcp 1.27, starlette 1.0, cryptography 46.0.6, etc.), fix README test counts. Breaking change: eval and hol_load return types changed from raw strings to JSON. All tests and smoke tests updated. * mcp: fix smoke test hol_load to use Library/iter.ml this was a typo, and now it matches the unit test. * mcp: remove extra blank lines in test_server.py
…rk (jrh13#164) - Fix ONCE_REWRITE_TAC description: 'one pass, all topmost matches' not 'only once' - Add GEN_REWRITE_TAC examples with RAND_CONV and LAND_CONV conversionals - Note that ARITH_TAC ignores hypotheses (goal only) - Add SUBGOAL_THEN variants: MP_TAC, SUBST1_TAC, STRIP_ASSUME_TAC - Add ABBREV_TAC / EXPAND_TAC pair - Add pitfalls: SUBST1_TAC silent success, THEN vs THENL after SUBST1_TAC, ONCE_REWRITE_TAC all-matches semantics, ARITH_TAC ignoring hypotheses Co-authored-by: Kiro (Claude Opus 4.6) <kiro@amazon.com>
* mcp: add proof recording with start_recording/stop_recording tools Record e(TACTIC) and b() calls from eval, apply_tactic, and backtrack to a JSONL file. Includes paren-counting tactic extraction from eval and automatic backtrack tracking. New tools: start_recording(path), stop_recording(). * mcp: add recording_dir config for auto-recording If recording_dir is set in hol-mcp.toml or HOL_RECORDING_DIR env var, recording starts automatically at server startup without needing the LLM to call start_recording. * mcp: add replay_init and replay_prefix config for proof resumption On startup, optionally #use an ML init file then replay a JSONL tactic prefix to restore proof state. Configured via replay_init/replay_prefix in hol-mcp.toml or HOL_REPLAY_INIT/HOL_REPLAY_PREFIX env vars. Seeds the recording with replayed steps so new tactics append to the prefix. Backtracks cleanly on any failure. * mcp: add recording tests and update SKILL.md Add start_recording/stop_recording to smoke test tool list and exercise the recording round-trip. Add unit tests for recording lifecycle, backtrack removal, failed tactic skipping, parent dir creation, and the _extract_e_tactic/_is_backtrack helpers. Add the two new tools to the SKILL.md utility tools section. --------- Co-authored-by: Ceren Kocaogullar <kceren@amazon.com>
Bumps [cryptography](https://github.com/pyca/cryptography) from 46.0.5 to 46.0.7. - [Changelog](https://github.com/pyca/cryptography/blob/main/CHANGELOG.rst) - [Commits](pyca/cryptography@46.0.5...46.0.7) --- updated-dependencies: - dependency-name: cryptography dependency-version: 46.0.7 dependency-type: indirect ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
This is a proof format translator for HOL Light, converting between interactive (g/e) and structured (prove) proof styles. It is inspired by Mark Adams' Tactician tool for HOL Light: http://www.proof-technologies.com/tactician/ which provided similar functionality via a "hiproof" representation and refactoring pipeline. This is a from-scratch reimplementation by Claude Code using string-based tactic recording rather than the original promotion/demotion mechanism. Although this simpler version requires some additional user work (e.g. saving a log of the tactic invocations to a file for processing by "i2s"), it is considerably simpler and less sensitive to OCaml internals.
…ishing (jrh13#169) * mcp: rename default checkpoint from "noledit" to "base" The old name was a leftover from when the checkpoint was created without ledit. "base" is clearer and matches the README examples. * mcp: add CI workflow for unit and smoke tests Runs on PRs/pushes to master when mcp/ files change. Builds HOL Light (OCaml 4.14), installs uv, then runs: - pytest test_server.py (unit tests) - smoke_test.py (MCP integration tests) * mcp: drop unused [cli] extra from mcp dependency We only use the stdio transport (FastMCP server + client). The [cli] extra pulled in typer, rich, shellingham, etc. that we never use. Removes 7 transitive dependencies, reducing dependabot surface. * add dependabot config, limit pip alerts to direct deps The mcp SDK pulls ~30 transitive dependencies (uvicorn, starlette, cryptography, pydantic, etc.) that we don't control. Using allow-list so dependabot only opens PRs for our direct deps (mcp, pytest) and GitHub Actions versions. * mcp: fix all audit issues Docs: - Fix stale test counts in README (38→48 unit, 34→37 smoke) - Add start_recording/stop_recording to README tools table - Add recording tools to TUTORIAL.md workflow summary CI: - Add timeout-minutes: 30 to mcp.yml workflow Code: - mcp_helpers.ml: replace fragile String.sub JSON slicing in mcp_json_apply_tactics with proper buffer-based construction - server.py: make recording append-only with backtrack markers instead of rewriting the entire file on every tactic - server.py: handle nested OCaml comments (* ... *) in _extract_e_tactic paren counting - make_checkpoint.py: deduplicate opam env parsing by importing _opam_env from server.py (with inline fallback) All 48 unit tests pass. * mcp: fix 5 more audit issues - start_recording: truncate existing file instead of appending - _record_tactics_batch: capture total_goals for last tactic from the batch result instead of always recording 0 - smoke_test: use set-contains for tool list check so adding new tools doesn't break the existing assertion - .gitignore: add __pycache__/ (was only in global gitignore) - hol_restart: reset _recording_flushed so recording stays consistent after a restart All 48 unit tests pass. * fix missing trailing newline in .gitignore * mcp: rewrite make_checkpoint.py for better UX - Add argparse with --help, --name, -I flags - Validate prerequisites before launching (ocaml-hol exists, dmtcp_launch on PATH, include dirs exist) - Clear error messages instead of cryptic "EOF before loaded" - Fix LD_LIBRARY_PATH not being set (caused silent dmtcp failures) - Print checkpoint plan and size on completion - s/Bare/Base/ in README checkpoint example * mcp: fix recording duplication on replay and restart _replay_prefix() was setting _recording_flushed=0 then flushing, which re-appended all replayed entries to the file that already contained them. Fix: set _recording_flushed=len(replayed) since the entries are already on disk. Similarly, hol_restart() was setting _recording_flushed=0 without truncating the file, causing duplication on next flush. Fix: set _recording_flushed=len(_recording) to mark existing entries as already written. * mcp: fix off-by-one in _record_tactics_batch error path The OCaml side sets "step" to the count of successful tactics (incremented after e(tac) succeeds). The Python code was computing succeeded = step - 1, undercounting by 1. For example, if the first tactic succeeded and the second failed (step=1), zero tactics were recorded instead of one.
Bumps [actions/checkout](https://github.com/actions/checkout) from 2 to 6. - [Release notes](https://github.com/actions/checkout/releases) - [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md) - [Commits](actions/checkout@v2...v6) --- updated-dependencies: - dependency-name: actions/checkout dependency-version: '6' dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Bumps [astral-sh/setup-uv](https://github.com/astral-sh/setup-uv) from 4 to 7. - [Release notes](https://github.com/astral-sh/setup-uv/releases) - [Commits](astral-sh/setup-uv@v4...v7) --- updated-dependencies: - dependency-name: astral-sh/setup-uv dependency-version: '7' dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
7 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.