mcp: add CI, reduce dependabot false positives, and miscellaneous polishing

.github/dependabot.yml

@@ -0,0 +1,16 @@
+version: 2
+updates:
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    schedule:
+      interval: "weekly"
+
+  - package-ecosystem: "pip"
+    directory: "/mcp"
+    schedule:
+      interval: "weekly"
+    # Only alert on our direct dependencies, not transitive ones
+    # we can't control (pulled in by the mcp SDK).
+    allow:
+      - dependency-name: "mcp"
+      - dependency-name: "pytest"

.github/workflows/mcp.yml

@@ -0,0 +1,44 @@
+name: MCP Tests
+
+on:
+  workflow_dispatch:
+  pull_request:
+    branches: [master]
+    paths: ['mcp/**']
+  push:
+    branches: [master]
+    paths: ['mcp/**']
+
+jobs:
+  mcp-tests:
+    runs-on: ubuntu-22.04
+    timeout-minutes: 30
+    name: MCP unit & smoke tests
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Install opam & build HOL Light
+        run: |
+          sudo apt update && sudo apt install -y opam xdot
+          opam init --disable-sandboxing
+          make switch
+          eval $(opam env)
+          make
+
+      - name: Install uv
+        uses: astral-sh/setup-uv@v4
+
+      - name: Install MCP dependencies
+        run: cd mcp && uv sync
+
+      - name: Run unit tests
+        run: |
+          eval $(opam env)
+          cd mcp && uv run pytest test_server.py -v
+
+      - name: Run smoke tests
+        run: |
+          eval $(opam env)
+          cd mcp && uv run python smoke_test.py

.gitignore

@@ -27,3 +27,4 @@ unit_tests_inlined.ml
 unit_tests.byte
 unit_tests.native
 hol-*.ckpt
+__pycache__/

mcp/README.md

@@ -47,6 +47,8 @@ See [TUTORIAL.md](TUTORIAL.md) for more examples (including s2n-bignum ARM proof
 | `hol_restart` | Kill and restart the HOL Light subprocess | Status message |
 | `hol_status` | Check process health, uptime, config, checkpoint | Structured JSON |
 | `hol_help` | Return tactic reference and proof guide (SKILL.md) | Markdown text |
+| `start_recording` | Start recording proof tactics to a JSONL file | Status message |
+| `stop_recording` | Stop recording and return the file path | Status message |
 
 `eval` returns `{"success", "output", "output_truncated", "full_output_chars", "time_seconds"}`. Large outputs are truncated to `max_output_chars` (default 4000, configurable). Override per-call with `max_output_chars=N`.
 
@@ -76,7 +78,7 @@ Create named checkpoints:
 ```bash
 export LD_LIBRARY_PATH="$HOME/.local/lib:$LD_LIBRARY_PATH"
 
-# Bare HOL Light (~75s)
+# Base HOL Light (~75s)
 python3 mcp/make_checkpoint.py --name base
 
 # With s2n-bignum ARM infrastructure (~5-10min)
@@ -136,8 +138,8 @@ The server includes a built-in `hol_help` tool that returns the full tactic refe
 
 ```bash
 cd mcp
-uv run pytest test_server.py -v       # 38 unit tests
-uv run python smoke_test.py           # 34 MCP integration checks
+uv run pytest test_server.py -v       # 48 unit tests
+uv run python smoke_test.py           # 37 MCP integration checks
 ```
 
 First run includes HOL Light startup (~75s cold, ~2s with checkpoint).

mcp/TUTORIAL.md

@@ -140,7 +140,7 @@ apply_tactic  "DISJ2_TAC THEN REWRITE_TAC[EVEN_ADD] THEN ASM_REWRITE_TAC[NOT_EVE
 8. **hol_status** — check if HOL Light is alive (useful for debugging)
 9. **hol_restart** — restart HOL Light if it has died or is in a bad state
 
-**Utility tools:** **hol_type** (get term types), **hol_load** (load files), **hol_interrupt** (cancel hung tactics), **hol_help** (tactic reference)
+**Utility tools:** **hol_type** (get term types), **hol_load** (load files), **hol_interrupt** (cancel hung tactics), **hol_help** (tactic reference), **start_recording** / **stop_recording** (record tactics to JSONL for replay)
 
 ---
 

mcp/hol-mcp.toml

@@ -4,7 +4,7 @@
 
 # Which checkpoint to use (looks for hol-<name>.ckpt/ in HOL Light root).
 # Create with: python3 mcp/make_checkpoint.py --name <name> [options]
-checkpoint = "noledit"
+checkpoint = "base"
 
 # Timeout in seconds for HOL Light commands.
 timeout = 600