mcp: add CI, reduce dependabot false positives, and miscellaneous polishing#169
Merged
jrh13 merged 10 commits intojrh13:masterfrom Apr 16, 2026
Merged
mcp: add CI, reduce dependabot false positives, and miscellaneous polishing#169jrh13 merged 10 commits intojrh13:masterfrom
jrh13 merged 10 commits intojrh13:masterfrom
Conversation
The old name was a leftover from when the checkpoint was created without ledit. "base" is clearer and matches the README examples.
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)
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.
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.
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.
- 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.
- 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
_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.
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.
Owner
|
All great, thank you! I will merge. |
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
2 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.
Add CI tests: Added
.github/workflows/mcp.ymlto run unit tests and smoke tests on PRs that modify themcp/**folder.Reduce dependabot false positives: We only use the stdio transport, but the
mcpdependency pulls HTTP transport deps likecryptography. Added.github/dependabot.ymlto allow-list our direct deps. This should reduce false positive dependabot pings like #165Miscellaneous polishing: Replace fragile
String.subJSON slicing inmcp_json_apply_tacticswith more robust buffer-based construction. Rename default checkpoint from "noledit" to "base". And more.h/t @jargh for spotting bugs in an earlier version of this PR.
All 48 unit tests pass.