[llm] agent-facing interfaces: interactive REPL and in-binary MCP server - #1019
Draft
strub wants to merge 34 commits into
Draft
[llm] agent-facing interfaces: interactive REPL and in-binary MCP server#1019strub wants to merge 34 commits into
strub wants to merge 34 commits into
Conversation
strub
force-pushed
the
llm-interactive
branch
2 times, most recently
from
May 31, 2026 17:54
9f3da5b to
7f13cec
Compare
strub
force-pushed
the
llm-interactive
branch
3 times, most recently
from
July 17, 2026 06:13
a61a327 to
f409cdd
Compare
Introduce an interactive REPL for LLM coding agents driving EasyCrypt (`easycrypt llm`) using a line-oriented protocol over stdin/stdout, plus two CLI flags for goal inspection: - `-upto <pos>` compile up to a given position and print the goals - `-lastgoals` print the last unproven goals at end-of-file REPL protocol (see `doc/llm/CLAUDE.md` for the full guide): - LOAD "file.ec" [LINE[:COL]] -- compile, optionally up to a position - UNDO / REVERT <uuid|name> -- navigate proof state - GOALS / GOALS ALL -- inspect current or all subgoals - CHECKPOINT <name> -- named bookmarks for branching - SEARCH <pattern> -- lemma search - QUIET ON/OFF -- suppress goal display for bulk input - Direct EasyCrypt input (tactics, declarations, search, print, ...) Responses use a typed envelope (OK/ERROR with uuid) terminated by an `<END>` sentinel for reliable parsing. LOAD reports the last processed line in the response tag; error messages include the offending source text; only the current subgoal is shown by default with a remaining count.
Add a -trace flag to the LOAD REPL command. When set, LOAD compiles the prefix exactly as today (using the existing LINE[:COL] argument, or up to EOF if omitted), but defers the last sentence and runs it under goal capture, then returns a response body with four delimited blocks: === BEFORE: line L (col C) === <focused goal before the sentence> === TACTIC (lines L:C - L':C') === <exact source text of the sentence> === AFTER: line L (col C) === <new focused goal + any new sibling goals> === SUMMARY === open goals: N1 -> N2 Adapted from PR #1018 (-trace LINE[:COL] for batch mode): same delimiters and the same new-or-modified-head filtering for AFTER. The position is taken from LOAD's existing LINE[:COL] argument; the tag is the regular [loaded:file:LINE]. If the deferred sentence is outside a proof context, or there is no sentence to trace, the reply uses the ERROR envelope with a clear message. If the sentence fails, the BEFORE/TACTIC blocks are still delivered, AFTER carries a <sentence failed> marker, and the formatted exception is appended. Expose EcCommands.in_proof so the REPL can check the pre-execution proof status without inspecting scope internals.
Three small additions to make REPL-driven proof exploration pleasant without weakening +strict_bullets for saved scripts. 1. Bullet relaxation for REPL input. EcCommands.disable_repl_bullets is called at every REPL phrase; it drops pm_strict_bullets and clears puc_bullets on the active proof so REPL-typed tactics are not rejected for missing bullets. Files loaded via LOAD still respect their own pragma; only direct REPL input is relaxed. 2. TREE / TREE ALL meta-commands. List all open subgoals as a flat numbered enumeration with the focused goal marked. TREE shows a one-line conclusion per goal; TREE ALL shows the full goal bodies. Backed by EcCommands.pp_tree on top of EcCoreGoal.all_opened. 3. [focus: k/N] reply tag. When more than one subgoal is open, both tactic replies and the LOAD response carry [focus: 1/N] alongside any other tag, so the caller knows the next tactic targets goal #1 of N. Supporting plumbing: EcScope.set_xgoal exposes a way to swap the active proof_uc without going through the tactic engine.
The REPL relies on EC's "first open goal is the focused one"
convention. Until now the only way to work on a non-first goal was to
discharge the earlier ones; the proving agent often wants to inspect
or skip a particular sibling without that.
Add two meta-commands:
FOCUS N rotate the open-goal list so the goal at index N (from
TREE) becomes the focused one, preserving cyclic order.
NEXT shorthand for FOCUS 2 (rotate one step).
Backed by a new EcCoreGoal.rotate_focus that splits and recombines
pr_opened. Going through the tactic engine doesn't work for standalone
rotation: tcenv1_of_proof tc_down's the siblings out of view, so
Protate (the `first last` parsed form) has nothing to rotate at the
top level.
EcCommands.focus_goal wraps rotate_focus, applies it via the same
scope-mutation path disable_repl_bullets uses, and pushes a new
context so UNDO/REVERT can roll the change back.
REPL phrases are recorded with (uuid, source, parent_handle, opens),
where parent_handle is the focused goal right before the phrase ran.
COMMIT replays them against the proof DAG to recover the bullet
structure.
The DAG edge is now explicit. EcCoreGoal's proofenv carries a
pr_parent : handle ID.Map.t populated by FApi.newgoal (the single
choke-point where every child handle is created); EcCoreGoal exposes
children_of_handle / parent_of_handle on top of it. This avoids the
older approach of reading children out of g_validation, which only
worked for VIntros / VConv / VLConv / VRewrite / VExtern -- not for
VApply, whose subgoals are added to the tcenv state outside the
validation record.
Algorithm:
- For each phrase, walk the subtree rooted at its parent handle,
registering each multi-child split's children in [sibling_depth]
at the right depth. Single-child links are continuations and do
not bump depth.
- To decide whether a phrase needs a bullet, walk upward via
parent_of from its recorded parent until hitting a registered
sibling ancestor; if found, emit the bullet for that depth and
consume the registration.
Bullet tokens are chosen per depth from PR 1017's lexer order
(-, +, *, --, ++, **, ---, +++, *** ...), skipping any token already
in scope from the LOAD prefix's puc_bullets stack. The stack is
snapshotted at the moment REPL input takes over (the new return value
of disable_repl_bullets) so COMMIT can avoid token collisions with
frames opened by the prefix.
Tested patterns: simple split, nested split, case-split,
multi-tactic-per-sibling, compound first phrase (move=> hp hq;
split.), pHL seq N chain, list induction, have introducing a side
goal, [split; split.] producing 4 goals in one phrase, UNDO/REVERT
trimming, LOAD mid-proof continuation, and LOAD prefix already using
bullet tokens that COMMIT must avoid. All round-trip through
`ec.exe compile` under `pragma +strict_bullets`.
The LLM REPL accumulated ~870 lines of closures and refs inside [main]'s body, intermixed with the unrelated compile/runtest/docgen plumbing. Move it out into [src/ecLlm.ml] (with a one-line .mli exposing just [val run]). The implementation organises its closed-over state (notices buffer, transcript, prior-bullets snapshot, checkpoints, quiet flag, initialized flag) at the top of [run], then groups the helpers into nested submodules so each concern is named: - Goals goal/error formatting, focus tag, tree rendering - Wire OK/ERROR/<END> envelope and replies - Transcript transcript trimming and clearing - Commit bullet-token generator and DAG walk for COMMIT - Load LOAD parser, prefix processor, and -trace block [ec.ml] keeps the small [Llm] dispatch arm that calls [EcLlm.run ~relocdir ~boot llmopts]. Pure move, no behavioural change; smoke-tested with COMMIT, TREE, FOCUS, and -trace.
The main loop was a flat ~150-line if/else chain that mixed line parsing (substrings, int_of_string, String.starts_with checks) with the actions to take. Split into: module Parse: a [command] variant covering every accepted line shape (Quit, Help, Undo, Goals of [`One|`All], Tree of [`One|`All], Commit, Focus of int, Next, Checkpoint of string, Revert of string, Quiet of bool, Search of string, Load of string, Ec of string, Begin_multi, Done_multi, Multi_line of string, Blank), plus [of_line ~multi_active] which is a stateless string -> command, and [Parse_error] for argument-shape mistakes (e.g. "FOCUS foo"). module Dispatch: a flat pattern match on the parsed command, delegating to small handlers (do_help, do_undo, do_focus_request, do_checkpoint, do_revert, do_quiet, do_search) and to the existing Load/Commit/Goals submodules. Holds the multi-line buffer state (multi_buf/in_multi) since Parse is pure. The main loop becomes 9 lines: read a line, parse to a command, dispatch, catch Parse_error and reply ERROR. Behaviour is unchanged; manual smoke tests cover COMMIT, TREE, FOCUS (good and bad arg), CHECKPOINT/REVERT, SEARCH, multi-line input, and the prior-bullets collision case.
Before, lines like "CHECKPOINT" (no trailing argument) silently fell
through to EC input because the dispatcher used [String.starts_with
"CHECKPOINT "] -- requiring the trailing space that [String.strip]
on the input line had just removed. The user saw EC's generic "parse
error" instead of a command-specific message. Same shape applied to
LOAD, FOCUS, REVERT, and SEARCH.
Introduce a small [keyword_arg kw line] helper that accepts both
[line = kw] and [line = kw ^ " " ^ ...], returning the stripped
argument tail. Each prefix command now routes to its own parser even
when the argument is empty, and each parser produces a specific
[Parse_error] message:
FOCUS -> "FOCUS: missing argument"
CHECKPOINT -> "CHECKPOINT: missing name"
REVERT -> "REVERT: missing uuid or checkpoint name"
SEARCH -> "SEARCH: missing query"
LOAD -> "LOAD: missing filename" (Load.handle, which already
had this branch but it
was unreachable)
Introduce a frame tree derived from pr_opened + parent_of: each open
leaf's chain of multi-child ancestors (skipping single-child
continuations) becomes its path through the tree. The same data
structure backs both TREE rendering and FOCUS path lookup.
TREE now shows depth-indented entries labelled with dotted paths
matching what FOCUS accepts. Leading singleton frames are
unwrapped: when all opens share an outermost split, the rendering
starts at that split's branches, not at a redundant [1.] wrapper.
FOCUS N1.N2.N3 walks the tree following each component and focuses
the resolved leaf. A single integer (FOCUS k) still works (degree-1
path). The path must resolve to a leaf; selecting an internal frame
yields "FOCUS: path must select a leaf goal, not a frame" and
overshooting a leaf yields "FOCUS: path overshoots a leaf goal".
After [split. split. split.] on [((a /\ b) /\ c) /\ d], TREE prints:
[1.1.1] a = a <- focused
[1.1.2] b = b
[1.2] c = c
[2] d = d
and FOCUS 1.2 selects c, FOCUS 2 selects d, FOCUS 1.1.2 selects b.
NEXT semantics unchanged. Flat proofs render unindented as before.
Add two workflow sections that were missing or stale:
4. Inspect and navigate nested subgoals with TREE and FOCUS
Documents the dotted-path syntax (FOCUS 1.2.3), the [focus: k/N]
reply tag, and the fact that TREE labels are dynamic
(focus-first, not stable across focus changes).
5. Build a +strict_bullets-friendly proof with COMMIT
Documents how COMMIT replays the recorded transcript and inserts
bullets, plus the cycle (-, +, *, --, ++, **, ...) and the prior-
bullet collision avoidance.
Re-number the existing QUIET and SEARCH sections from 4/5 to 6/7.
Fix one outdated pitfall ("subgoals must be closed in order") --
FOCUS path now lets the agent address them in any order.
Reflects what's live in EcLlm; the protocol/meta-command table was
already up to date.
Add llmo_eval : string option to llm_option, wired to the -eval CLI flag. When set, EcLlm.run splits the argument on newlines and feeds each line through the same Parse/Dispatch pipeline as stdin, then exits at end of script (no QUIT required, though QUIT still works). Enables cheap scripted use without piping: easycrypt llm -eval 'LOAD "myfile.ec" 42 GOALS COMMIT' The stdin path is unchanged when -eval is not given. Docs updated.
Add ldro_stdlib : string list to ldr_options, wired to a repeatable -stdlib CLI flag. When non-empty, its entries replace Sites.theories as the roots of the System-namespace loading loop -- both the prelude add and (unless -boot) the recursive add. When empty (the default), the built-in Sites.theories list is used, preserving today's behaviour. This is stronger than -boot alone: -boot only suppresses the recursive-System add and still injects <Sites.theories>/prelude, so a caller wanting to fully sidestep the shipped stdlib currently has no clean way to do it. With -stdlib, the built-in Sites.theories is never touched. The two flags remain independent and compose: -stdlib DIR : DIR/prelude (System) + DIR (recursive System) -boot : <builtin>/prelude (System) only -boot -stdlib DIR : DIR/prelude (System) only -stdlib is also propagated to subprocess invocations of runtest so child ec calls see the same effective load path.
The REPL discovers files at run time, after option parsing, so the project-file context that the batch compiler resolves from its command-line input was never applied: LOADing a file whose project supplies include dirs, provers, timeout or pragmas failed to locate theories (and checked with default prover settings). LOAD now resolves the easycrypt.project attached to the loaded file (same parent-directory walk as the compiler), extends the load path with its idirs/rdirs, re-initializes with the project's prover options overlaid on the command-line ones, and sets the current path to the file's directory, mirroring the compile path. Note: a project scalar (e.g. timeout) now takes precedence over the same setting given on the llm command line, since the two cannot be told apart after option parsing.
17 scenarios under tests/llm (scripts + recorded goldens + fixtures), driven by scripts/testing/llm-golden and a `make test-llm` target. Each script declares its expected exit status on a `# exit: N` first line; the runner strips #-comment lines, feeds the rest to `ec llm -eval` with tests/llm as the working directory (relative fixture paths keep the [loaded:...] tags machine-independent), and diffs stdout against the golden. `--record` re-records, still checking the declared exit code. Coverage: LOAD (+ -nosmt, -trace happy/error, argument errors), GOALS/GOALS ALL, nested TREE/TREE ALL, FOCUS dotted paths and error paths, NEXT, UNDO/REVERT/CHECKPOINT (incl. errors), COMMIT (simple, nested, prior-bullets, mid-proof-LOAD continuation, after qed), SEARCH, QUIET, <BEGIN>/<DONE>, and -eval exit-code semantics. Fixtures use AllCore only and close goals without SMT so goldens are deterministic (verified over repeated runs). Goldens record CURRENT behaviour, bugs included, as the byte-identity gate for the upcoming EcLlmCore extraction. Known frozen defects, to fix separately (with deliberate golden updates): COMMIT emits a flat, bullet-less body once the proof is closed by qed (the DAG walk finds no ancestors in a discarded proof); COMMIT under a +strict_bullets prefix flattens outer-frame siblings to the inner depth; LOAD of a missing file leaks a raw Sys_error anomaly.
COMMIT reconstructed bullet structure by walking the proof DAG through EcCommands.parent_of/children_of, which read the ACTIVE proof from the scope. Once `qed.` has run there is no active proof, so both accessors answered None/[]: COMMIT registered no siblings and emitted a flat, bullet-less body -- exactly the case where the body is most useful (the proof is finished and ready to be pasted back). A [proofenv] is immutable and cumulative, so it can outlive the proof it belongs to. Add `EcCommands.current_proofenv` (Some the proofenv of the active PSCheck proof, else None), snapshot it in EcLlm's new `commit_env` ref at every recorded phrase -- keeping the last non-empty snapshot, so the phrase that closes the proof does not clear it -- and have Commit.proof_text query EcCoreGoal.parent_of_handle / children_of_handle against that snapshot, falling back to the live proof when nothing was recorded. Transcript.clear resets it along with the transcript. The snapshot is re-taken at every recorded phrase, so after UNDO plus a new phrase it is the rewound environment plus the new children; handles from undone phrases are either gone or inert (no transcript entry references them). Goldens changed: * tests/llm/expected/commit-after-qed.out -- the two `trivial.` lines now carry `- ` bullets; `qed.` stays flat, since no goal was open right before it and it therefore has no parent handle. Intended. * tests/llm/expected/multiline.out -- same, for the proof built from the multi-line lemma statement. Intended. * tests/llm/scripts/commit-after-qed.script -- comment updated: it described the old flat output as the frozen behaviour. commit-simple, commit-nested, commit-load-continuation and commit-strict-bullets are byte-identical (verified).
Under a `+strict_bullets` LOAD prefix, COMMIT seeded *every* goal that
was open when the first REPL phrase ran at depth 1 and then handed the
whole run a single freshly-picked token. Two things went wrong:
* goals still owned by different prefix frames were flattened onto one
level, so the emitted body no longer described the proof's shape;
* the prefix's own tokens were never reused, even though addressing a
frame's next sibling is spelled with exactly that frame's token --
the emitted token instead opened a brand-new nested level under the
frame that was meant to be left.
With fixtures/strict.ec (stack `[-]` with floor 1, three goals open)
the old body was three flat `+ trivial.` lines: the third goal, a
sibling of the prefix's `-`, was emitted as if it lived inside it.
New rule. Let the prefix frames be t_1..t_k, outermost first (the
stack stores the innermost frame at its head), and n = the number of
goals open at the first recorded phrase. A frame with floor f is
discharged once f goals remain, so it still owns the first (n - f)
goals of the focused-first list. A goal covered by c frames is seeded
at depth c+1. For depth d <= k the token IS t_d's own token (the
depth-to-token cache is pre-populated with those before any fresh pick
happens); deeper levels keep cycling -, +, *, --, ... skipping every
token on the stack and every token already assigned.
When the prefix left no frame, coverage is empty and every goal lands
at depth 1 exactly as before; the case of a single open goal and no
frame stays unseeded, so the REPL simply continues on the prefix's own
focus. Empty-stack scenarios are byte-identical (verified).
Manual recompilation checks (deliberately not in the harness, which
only diffs REPL stdout): for both strict fixtures I concatenated the
fixture prefix, the body COMMIT emitted and `qed.`, and compiled the
result with `ec.exe compile -no-eco`. Both succeed, and both now read
as the proof a human would have written:
split. split.
- split. - split.
+ trivial. + split.
+ trivial. * trivial.
- trivial. * trivial.
+ trivial.
- trivial.
Goldens changed:
* tests/llm/expected/commit-strict-bullets.out -- was three flat
`+ trivial.` lines, now ` + trivial.` / ` + trivial.` /
`- trivial.`: the first two goals are inside the prefix's `-` frame
(fresh `+`, indented), the third is that frame's next sibling and
reuses `-`. Intended.
Goldens added:
* tests/llm/{fixtures/strictnested.ec,scripts/commit-strict-nested.script,
expected/commit-strict-nested.out} -- new scenario with two prefix
frames (`-` then `+`) and four open goals, exercising token reuse at
two depths plus one fresh level (`*`).
`LOAD "nosuch.ec"` ran the whole LOAD preamble -- project-file lookup,
scope re-initialisation, transcript reset -- and only failed when
EcIo.from_file opened the file, surfacing as
`anomaly: Sys_error("nosuch.ec: No such file or directory")`. Besides
being an unhelpful message, the session had already been reset by the
time it was reported.
Check `Sys.file_exists` in Load.handle right after filename parsing,
before anything touches the session, and fail with
`LOAD: no such file: <filename>`. The unknown-extension error is
unchanged; it now only fires for files that exist.
Goldens changed:
* tests/llm/expected/load-errors.out -- the anomaly line becomes
`LOAD: no such file: fixtures/nosuch.ec`. Intended.
* tests/llm/scripts/load-errors.script -- the unknown-extension case
used `fixtures/simple.txt`, which does not exist and would now be
caught by the existence check first; it points at a new file that
does exist, and the two cases are ordered missing-then-extension.
Goldens added:
* tests/llm/fixtures/notec.txt -- an existing non-EasyCrypt file, so
the unknown-extension path stays covered.
* tests/llm/README.md -- layout table no longer claims fixtures are
all `.ec`.
Every successful REPL phrase was appended to the COMMIT transcript,
queries included. Looking a lemma up mid-proof with `SEARCH`, `search`,
`print` or `locate` therefore inserted the query into the proof body
COMMIT emits -- a body that no longer describes the proof, and that a
reader would have to strip by hand.
process_action now skips the transcript append (and the proofenv
snapshot) for the query actions Gprint / Gsearch / Glocate. Everything
else -- declarations, `proof.`, tactics, `qed.` -- is recorded as
before, and the engine still runs the query, so uuid behaviour and the
printed results are unchanged. The SEARCH meta-command reaches the
same code path through process_ec_input, so it is covered too.
Goldens added:
* tests/llm/{scripts/search-in-proof.script,expected/search-in-proof.out}
-- mid-proof SEARCH between two tactics; the recorded body is the
two `- trivial.` lines only.
Golden search.out is unchanged (it never ran COMMIT); verified, as is
the rest of the suite.
doc/llm/CLAUDE.md: the COMMIT section now states the exemption.
Only the replies produced by Wire.reply_ok_goals -- tactic phrases, FOCUS, NEXT, UNDO, REVERT -- and LOAD carried the `[focus: k/N]` tag. The inspection commands did not, so `GOALS`, `GOALS ALL`, `TREE`, `TREE ALL` and `COMMIT` answered with a bare `OK [uuid:N]` even with several goals open: exactly the commands an agent uses to find out how many goals there are. Dispatch now passes ~tag:(Goals.focus_tag ()) on those five arms. HELP, QUIET and CHECKPOINT do not report proof state and stay untagged. focus_tag is unchanged (empty below two open goals), so single-goal replies are unaffected. Goldens changed (each gains a tag on an otherwise identical line): * tests/llm/expected/load-goals.out -- the `GOALS` and `GOALS ALL` replies after `split.` (2 open goals) become `[focus: 1/2]`. * tests/llm/expected/tree-nested.out -- the `TREE` and `TREE ALL` replies (4 open goals) become `[focus: 1/4]`. * tests/llm/expected/focus-nav.out -- the two `TREE` replies (4 open goals) become `[focus: 1/4]`. quiet, load-nosmt and the commit-* scenarios are unchanged: they have at most one goal open when they run an inspection command. The tagged COMMIT reply is not exercised by any scenario; checked by hand (`COMMIT` after two splits replies `OK [uuid:5] [focus: 1/3]`). Also in this commit: the Commit module header still described the old "skip every stack token" policy replaced two commits ago; corrected. doc/llm/CLAUDE.md: the pitfall bullet listed no commands, which read as if only tactic replies were tagged; it now names the tagged commands and the untagged ones, and the TREE example shows its tag.
`-trace` defers the last in-prefix sentence so it can be run under goal capture. When the epilogue decided it could not trace -- no sentence pending (`trace: nothing to trace`), or the sentence sits outside any proof (`trace: target sentence is not in a proof context`) -- it failed with the deferred sentence still pending, so it was never run. The session was therefore one sentence short of a plain LOAD of the same prefix, and everything that sentence brought in was missing: `LOAD "f.ec" 3 -trace` stopping on `require import AllCore.` left a session where `b2i` did not resolve. Recovering meant reloading. Both branches now flush the deferred sentence (plainly, without trace capture) before failing, so the state matches a plain LOAD. The ERROR text is unchanged; the reply uuid now reflects the flushed sentence. A failure inside the flush propagates to the enclosing handler and is reported like any other prefix failure. `trace: nothing to trace` has nothing pending by construction, so flushing there is a no-op, kept for uniformity. Goldens changed: * tests/llm/expected/load-trace-notinproof.out -- the ERROR reply moves from `[uuid:0]` to `[uuid:1]` (the `require` ran). Intended. * tests/llm/scripts/load-trace-notinproof.script -- extended with `GOALS`, a lemma whose statement needs AllCore, and a second `GOALS`, so the golden actually demonstrates the preserved state. Before this fix that lemma failed with "no matching operator, named `b2i'". doc/llm/CLAUDE.md: the `-trace` section now states that a trace that cannot run still leaves a usable session.
Phase 0b of the `easycrypt mcp` plan: `easycrypt llm` is about to grow a
second front-end (JSON-RPC over the same engine), so the part of the REPL
that talks to EasyCrypt is extracted verbatim into a module that neither
prints nor exits.
What moved to src/ecLlmCore.ml(i):
- the session state, previously the closure refs of [run], now a
[state] record (cur_prvopts, notice buffer, initialized, projdirs,
checkpoints, transcript, commit_env, prior_bullets); [create]
performs the why3 connect / Random.self_init / relocdir addidir /
first [do_initialize] in the same order as before. The engine is a
global singleton, hence at most one [state] per process;
- the [Goals], [FrameTree], [Transcript] and [Commit] submodules and
[process_action], unchanged except for taking [state];
- one function per meta-command ([load], [step], [goals], [tree],
[focus], [undo], [revert], [checkpoint], [commit], [search]),
lifted from the [Dispatch] handlers.
Presentation state stays in src/ecLlm.ml: [quiet], the <BEGIN>/<DONE>
buffer, [had_error], HELP (a file read), the READY banner, the -help
early exit, the -eval driver, the line parser (now including the LOAD
argument-string parser) and the OK/ERROR/<END> envelope.
Reply types: an operation returns [reply] {uuid; tag; notices; body;
changed} or [failure] {uuid; message; goals; notices} rather than
printing. The front-end reconstructs today's exact bytes from those
fields; MCP will build JSON from the same records. [body] is [Goals] or
[Text] because QUIET suppression applies to precisely the replies that
used to go through [reply_ok_goals] — that choice is presentation, so
the core only says "this reply ends on the goals" and the REPL renders
them via [current_goals]. Notices are captured-and-cleared at the exact
points [Wire] used to read the buffer, so interleaving is preserved;
[failure.notices] is captured but unused by the REPL, which never
printed notices on errors. [changed] (uuid advanced?) is unused today
and exists for MCP.
De-exiting, with no observable change:
- `exit.` typed at the prompt used to call [exit 0] from inside
[process_ec_input]. [step] now returns [Quit] after finalizing the
reader, and the front-end exits — same order, same status.
- LOAD's -trace failure used a local [Trace_failed] exception plus a
[trace_prefix] ref to prepend the BEFORE/TACTIC block to the error
message; the prefix is now concatenated into [failure.message]
exactly where [reply_error] received it.
- [EcCommands.Restart] still reinitializes (and clears checkpoints in
LOAD) inside the core, and returns an ordinary [Text "Session
restarted"] reply.
- a why3 connection failure raises [Init_error] instead of exiting;
the front-end prints the same message and exits 1.
Byte-identity compromises worth knowing about for the MCP phase:
- LOAD argument errors are raised as [Parse_error] from the front-end
parser, including the bare "int_of_string" that a malformed
LINE[:COL] produces: the old code let those [Failure]s reach
[reply_error] unchanged. The parser therefore maps [Failure msg] to
[Parse_error msg] wholesale.
- the file-existence check stays in the front-end parser (it must run
before the flags parse, as it did), so [load] trusts its [file]
argument to exist. The extension check stays in the core, after the
flags parse, to keep the error ordering of `LOAD f.txt 6 7`.
- GOALS/GOALS ALL return [Text], not [Goals]: QUIET never suppressed
them.
Gate: `dune build` clean, `make test-llm` 19/19 PASS, `git diff tests/`
empty. Ten further scripts covering paths the goldens do not reach
(`exit.`, QUIT, HELP, `pragma restart.`, a failing -trace sentence, LOAD
argument errors, doc comments, checkpoint/revert/focus errors, the
multi-line block, QUIET) produce byte-identical stdout, stderr and exit
status before and after.
A failed phrase can still have advanced the engine: a compound sentence whose leading tactics went through leaves a new uuid and a transcript entry behind. [try_step] runs [step] and, on failure, restores the pre-entry uuid the way REVERT does (EcCommands.undo + Transcript.trim), then re-stamps the failure -- its uuid and goal text described a state that no longer exists. [failure] gains a [reverted] flag so a front-end can tell the caller that the rollback happened. It is false everywhere else, and the REPL front-end is untouched: it builds failures through [make_failure]. No REPL surface change; this is the primitive the MCP ec_try tool needs.
Adds a second front-end over EcLlmCore speaking the Model Context
Protocol on stdio (JSON-RPC 2.0, newline-delimited, hand-rolled over
yojson, which ecLib already depends on). Wiring mirrors `llm`: an
mcp_option record and command spec in ecOptions (so -I/-timeout/-p/
-stdlib come from the shared option groups) and a dispatch arm in
ec.ml.
Protocol: initialize with version negotiation, ping, tools/list,
tools/call, tolerance for the lifecycle notifications, and the
-32700/-32600/-32601/-32602 errors. Batch arrays are rejected: they
were removed from the spec in 2025-06-18 and have not returned. The
loop is synchronous and single-threaded on purpose: the engine is a
global mutable singleton and uuid ordering is what makes ec_revert
meaningful, so calls must run strictly in arrival order.
Spec era: the server implements the initialize-handshake era, pinned
to 2025-11-25/2025-06-18/2025-03-26. The 2026-07-28 revision removed
the handshake in favor of stateless per-request _meta fields and
server/discover; deployed clients still speak the handshake era, and
per the spec's own compatibility matrix a dual-era client that
receives -32601 for server/discover falls back to initialize.
Supporting the stateless era is future work (noted at the top of
ecMcp.ml).
stdout is reserved for the protocol at the file-descriptor level: the
wire keeps a private dup of fd 1 and the process's stdout is pointed
at stderr, so a stray print anywhere under the engine lands in the
client's log instead of corrupting the message stream.
Eleven tools route to EcLlmCore: ec_load, ec_step, ec_try, ec_goals,
ec_tree, ec_focus, ec_undo, ec_revert, ec_checkpoint, ec_commit,
ec_search. The front-end validates arguments before the engine is
touched, since the core trusts what it is handed: ec_load checks that
the file exists rather than letting a Sys_error surface downstream,
ec_focus parses the dotted path itself, and JSON typing covers the
rest. That split keeps the two error channels honest -- an unknown
tool or an argument violating the declared schema is a JSON-RPC
-32602, while a prover error is a successful response with isError
set and the error text (plus the goals at that point) as content,
which is what an agent needs in order to react to it.
Every result carries structuredContent {uuid, changed} so an agent
can address the state later with ec_revert; ec_try adds reverted on
the failure side. Each tool declares a matching outputSchema. `exit.'
answers "session terminated" and stops the process. ec_step's
description states that only the first sentence of a phrase runs --
pre-existing behavior of the shared core, inherited from the REPL.
`EcLlmCore.step` parsed one toplevel phrase and silently dropped the
rest, so `split. trivial. trivial.` ran a single `split.`. It now loops
over `EcIo.xparse` the way the LOAD prefix does, handling each item as
before and answering with one reply at the end.
The semantics are those of a file: sentences run in order, a failure
stops the run there and comes back as the reply, and everything applied
before it stays applied. `exit.` ends the session immediately, with the
sentences that preceded it applied. The reply body is decided by the
last item that did something, so a lone doc comment still answers with
an empty body rather than with goals.
Both front-ends inherit this through the core; ec_step's and ec_try's
tool descriptions and the guide's "EasyCrypt commands" section are
updated to the new truth.
Goldens: no existing scenario changes bytes (all 19 pass untouched --
none of them packed two sentences onto one line). Two new scenarios:
* multi-sentence -- `split. trivial. trivial.` closes the proof in
one line (uuid 3 -> 6) and COMMIT shows all three sentences;
* multi-sentence-error -- `split. apply nosuchlemma. trivial.` stops
at the failure with `split.` applied (uuid 4, two open goals) and
COMMIT holding `split.' alone.
`Gsearch`/`Gprint`/`Glocate` reached the engine through
`EcCommands.process`, which pushes an undo context for whatever it
runs. A query hands back the very scope it was given, so the pushed
context was a duplicate of the current one -- but it still bumped
`ct_level`, so SEARCH advanced the uuid while being advertised as
read-only, and an UNDO right after a SEARCH only undid the query.
`EcLlmCore.process_action` now pops that context back off for the three
query constructors, restoring `ct_level` and the undo stack exactly as
they were (a no-op when the query itself failed, since nothing was
pushed then). The fix sits in the llm core rather than in
`EcCommands.process` so the batch compiler and the ProofGeneral
terminal keep counting phrases the way they always have.
SEARCH / `search .` / `print .` / `locate .` now reply with the
pre-call uuid, and ec_search reports changed:false, consistent with its
readOnlyHint:true annotation.
Manual UNDO/REVERT check (tests/llm, ec.native llm -eval):
LOAD "fixtures/simple.ec" 6 -> uuid 3, goal `1 = 1 /\ 2 = 2'
split. -> uuid 4, two goals
SEARCH (b2i _) -> uuid 4 (was 5), goals unchanged
UNDO -> uuid 3, back to `1 = 1 /\ 2 = 2'
(before: landed on uuid 4, i.e. it
undid nothing but the query)
CHECKPOINT c0 / trivial. / SEARCH / REVERT c0
-> uuid 3, goal restored, COMMIT empty
Goldens re-recorded, uuid shifts only:
* search -- SEARCH reply and the following ERROR go 4 -> 3;
* search-in-proof -- the SEARCH reply goes 6 -> 5 and the three
replies after it go 7 -> 6.
`EcLlmCore.failure` gained a `changed` field, computed like the one on
`reply`: the uuid after the operation against the uuid it started from.
A failing phrase can advance the engine before failing, so the flag is
not derivable from the failure alone -- `ecMcp.ml` was recomputing it
from a `pre` it had to carry through `call_tool`, `answer` and
`Result_of`, which is exactly the engine knowledge a front-end should
not hold. That plumbing is gone; the front-end reads the field.
`try_step` re-stamps it after the rollback, so it reports the *net*
effect of the call: false for a phrase that advanced, failed and was
rolled back, since after the rollback there is nothing left to have
changed. It stays true only when the rollback cannot reach the entry
uuid -- a `pragma Reset` that dropped the engine below it. The choice
is documented on the type in ecLlmCore.mli.
The REPL ignores the field (its envelope has never reported `changed`).
No golden changes, as expected: all 21 scenarios pass untouched.
Checked over the wire (tests/llm, ec.native mcp):
ec_load -> uuid 3, changed true
ec_search "(b2i _)" -> uuid 3, changed false
ec_step "apply nosuchlemma." -> uuid 3, changed false, isError
ec_step "split. apply nosuchlemma."-> uuid 4, changed true, isError
ec_try "split. apply nosuchlemma."-> uuid 3, changed false,
reverted true, isError
`make test-mcp` mirrors `make test-llm`: each tests/mcp/scripts/*.script is a newline-delimited stream of JSON-RPC messages piped into `ec.exe mcp', and its raw stdout -- the protocol, one message per line -- is diffed against tests/mcp/expected/*.out. `#'-comment lines are stripped and the first must declare the expected exit status, exactly as in llm-golden; --record and --bin behave the same way. The runner cd's into tests/mcp so fixture paths stay relative, and the scripts load the REPL harness's fixtures through ../llm/fixtures rather than duplicating them. One field of the stream is not reproducible -- serverInfo.version is a git-describe string -- and is rewritten to "VERSION" with sed before diffing; nothing else is normalized. Twelve scenarios, covering the plan's list: initialize (handshake + notifications/initialized + ping), version-negotiation (an unsupported "2099-01-01" falls back to 2025-11-25, a supported older revision is echoed), tools-list (the whole tool table verbatim), happy-path (load, step, goals, tree, focus, multi-sentence step, commit), prover-error (isError results carrying the goal state), try-revert (a phrase that advanced before failing, rolled back, with the following ec_goals proving the restored state), protocol-errors (-32700, -32600 for both a batch array and a malformed envelope, -32601, and eight -32602 cases), revert (by uuid and by checkpoint name), load-missing (a missing file and an unknown extension are isError results, NOT -32602), notifications (known and unknown ones draw no reply), exit (`exit.' answers "session terminated" and the process stops without reading further), and eof (clean shutdown). Gate: make test-llm (21) and make test-mcp (12) both green, twice in a row.
The goldens freeze what each front-end answers; nothing yet pinned that
they answer the *same thing*. `scripts/testing/mcp-parity', run by
`make test-mcp' after the goldens, plays one representative operation
per tool family -- load, step, goals, tree, focus, undo, checkpoint,
step, revert, search, commit, and a failing phrase -- against two
sessions started from the same directory on the same fixture, one
driven with `llm -eval' and one with a JSON-RPC script, and asserts for
each step that
* the REPL's [uuid:N] envelope tag equals the MCP result's
structuredContent.uuid, and
* the REPL's reply body -- what it prints between the OK/ERROR line
and <END> -- equals the MCP result's content[0].text.
The body comparison is exact up to one trailing newline, which is the
only licensed difference: the REPL terminates a body that lacks one so
that <END> starts a line of its own, and MCP, having no sentinel, does
not. Both wires are parsed structurally (blocks closed by a lone <END>;
one JSON object per line) rather than pattern-matched, so a body
containing something envelope-shaped cannot fool the checker.
The search step is the interesting one: its payload is notices (the
lemma listing, which arrives through the notifier) followed by the goal
body, so it pins the notices/body join the two front-ends implement
separately.
Two asymmetries are structural and are documented in tests/mcp/README.md
rather than papered over: the REPL's [loaded:...] / [focus: 1/N] tags
ride on the status line and have no MCP counterpart (structuredContent
carries uuid and changed only), and the REPL has never rendered notices
on an ERROR reply while the MCP failure result does -- so the two agree
on failures only when nothing was emitted, which holds for the phrase
the check plays.
Verified the checker bites: pointing the tree step at ec_tree
{"full":true} while the REPL still says TREE makes it FAIL with both
bodies printed.
Gate: make test-llm (21) and make test-mcp (12 goldens + 12 parity)
green, twice in a row.
Neither the goldens nor the parity check involve an MCP client; they
speak the wire themselves. Two manual checks close that gap, both
documented in tests/mcp/README.md and neither wired into CI (they need
network access).
`scripts/testing/mcp-inspector-check' drives the server with the
reference client, `npx @modelcontextprotocol/inspector --cli', over
tools/list and a tools/call. Observed, against ./ec.native:
$ npx --yes @modelcontextprotocol/inspector --cli ./ec.native mcp \
--method tools/list
11 tools: ec_load, ec_step, ec_try, ec_goals, ec_tree, ec_focus,
ec_undo, ec_revert, ec_checkpoint, ec_commit, ec_search
$ ... --method tools/call --tool-name ec_load \
--tool-arg file=tests/llm/fixtures/simple.ec --tool-arg line=6
{"content":[{"type":"text","text":"Current goal\n\nType variables:
<none>\n\n------\n1 = 1 /\\ 2 = 2\n"}],
"structuredContent":{"uuid":3,"changed":true},"isError":false}
`tests/mcp/claude-code.mcp.json' is a ready-to-paste project config.
Claude Code 2.1.238, registered at local scope (a project-scoped
.mcp.json needs interactive approval), reports
easycrypt: /.../ec.native mcp - ✔ Connected
and a headless `claude -p' saw all eleven tools and drove a session:
ec_load -> uuid 3, ec_step "split. trivial. trivial." -> uuid 6 (the
multi-sentence step of the first commit, over a real client), ec_commit
-> uuid 6. Connection + tools listing: gate met.
FINDING, and it is the reason this gate exists. The same headless run
shows the payload never reaches the agent:
> Call ec_load ... Then quote the ENTIRE raw tool result, verbatim.
{"uuid":3,"changed":true}
That's the complete content -- no additional human-readable text
accompanied it.
Isolated against a throwaway probe server returning identical text
under four result shapes, Claude Code's rule is: when a tools/call
result carries structuredContent, the model is handed that object and
`content' is dropped -- with or without an outputSchema. `content'
alone arrives; text placed *inside* structuredContent arrives. So it
is the presence of structuredContent, not of outputSchema, that
suppresses the payload, and the Inspector passes because it displays
both.
Our shape puts metadata in structuredContent and the goal state, search
results and proof body in `content', so `easycrypt mcp' is fully usable
from the Inspector and blind from Claude Code. The fix is a change of
result shape -- move the payload into structuredContent beside uuid and
changed, or drop structuredContent and fold the metadata into the text
-- which is a design decision this commit does not take. The evidence
and both options are recorded in tests/mcp/README.md.
Gate: make test-llm (21) and make test-mcp (12 + 12) green.
Claude Code, the client this server is primarily for, hands the model a tools/call result's `structuredContent' alone and drops `content' entirely whenever both are present -- with or without an outputSchema. The probe matrix behind that statement is in the message of e3dce85: four result shapes, identical text, and only the two that put the text somewhere other than a `content' shadowed by `structuredContent' reach the model. Our shape put the metadata in `structuredContent' and the payload -- goal state, commit body, search results -- in `content', so an agent driving `easycrypt mcp' through Claude Code saw `{"uuid":3,"changed":true}' and nothing else, while the Inspector, which displays both halves, showed nothing wrong. Each result now carries the text twice: `content' is unchanged, and `structuredContent' gains a `text' field holding exactly the string already in content[0].text -- one `~text' argument written into both halves by Result_of.make, so the copies cannot drift. Every tool's outputSchema declares `text' (string) required alongside `uuid' and `changed'; ec_try keeps `reverted' optional. The duplication is deliberate rather than a migration step. Dropping `content' would break spec-abiding clients that read it, and the parity check compares the REPL body against content[0].text; keeping both costs one repeated string per reply and serves either kind of client. Goldens: seven of twelve scenarios change, all in the same way -- structuredContent gains `text', and content[0].text, uuid, changed, reverted and isError are byte-identical to before (verified field by field against the recorded goldens); tools-list picks up the schema change. The five untouched scenarios play no tools/call. mcp-parity is unmodified and still green. tests/mcp/README.md: the "Known gap" section becomes "Result shape", which states the duplication, keeps the probe matrix as the reason, and turns the Claude Code check from "is it connected" into "can the agent quote the goal". Re-verified against the real client, Claude Code 2.1.238, the binary registered at local scope and removed afterwards: $ claude -p 'Call ec_load ... line=6. Then call ec_goals. Then quote the ENTIRE raw result object you received from ec_goals.' {"text":"Current goal\n\nType variables: <none>\n\n-----...-----\n 1 = 1 /\\ 2 = 2\n","uuid":3,"changed":false} Recap: the open goal is `1 = 1 /\ 2 = 2' ... The agent quotes the goal, which is the whole point; note that the object it received is still `structuredContent' alone, confirming the client rule rather than working around it. Gates: dune build clean; make test-llm (21) green; make test-mcp (12 goldens + 12 parity) green twice.
Adds a "Using the MCP mode" section to the agent guide: how to launch, the eleven tools, the uuid/state model (shared with the REPL section), the JSON-RPC-error / isError split, the result shape and why the reply text is duplicated, the ec_step and ec_try contracts, and a ready-to-paste client configuration. `mcp -help` now prints that section, as `llm -help` prints the whole guide: it reads the same file and cuts from the heading to the next one at the same level, falling back to the whole guide if the heading is gone. That is why `EcLlm.llm_guide_path` becomes public. README gains a paragraph on the LLM-agent interface, pointing at the guide.
strub
changed the title
`make check` now runs test-llm and test-mcp alongside unit, stdlib
and examples, and the CI library-check matrix gains both targets.
Both harnesses need only the built binary (their fixtures avoid SMT),
so they run in the same docker job as the existing targets.
Closes the last open item of PLAN-easycrypt-mcp.md Phase 2 ("wire
both into the existing test harness/CI").
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
1 participant
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.
Adds two front-ends over one shared proof-engine core, designed for
LLM proving agents:
easycrypt llm— an interactive REPL with a machine-friendlyprotocol (
OK/ERROR+<END>envelopes, monotonic state uuids).Meta-commands: LOAD (with
-nosmt,-trace), GOALS, TREE (nested,dotted-path labels), FOCUS (dotted paths), NEXT, UNDO, REVERT,
CHECKPOINT, COMMIT, SEARCH, QUIET, multi-line input,
-evalforscripted one-shot runs (nonzero exit on error).
easycrypt mcp— a Model Context Protocol server (stdio, JSON-RPC2.0, hand-rolled over the existing yojson dependency). Eleven tools
(
ec_load…ec_search, plusec_trywith an auto-revertcontract). Verified against the MCP Inspector and a live Claude
Code session.
Highlights:
+strict_bullets-ready proof body from the recordedinteractive session, reconstructing bullet structure from the proof
DAG (a new
pr_parentedge recorded inEcCoreGoalat goalcreation) and reusing the bullet tokens of frames the loaded prefix
left open.
pragma +strict_bulletsdoes not apply to REPL-typed phrases: theagent is the focus mechanism interactively; bullets are emitted at
COMMIT time.
structuredContent.text—empirically, Claude Code drops
contentwheneverstructuredContentis present (probe matrix in the git history).(2025-11-25 and earlier); the 2026-07-28 stateless revision is
documented future work.
-stdlib DIR(replace the built-in standard libraryroot),
llm -eval STR.Testing: two golden harnesses (
make test-llm, 21 scenarios;make test-mcp, 12 protocol goldens + 12 REPL/MCP parity checkspinning the two-front-ends-one-core invariant), all green.
Docs:
doc/llm/CLAUDE.mdcovers both modes and is printed byllm -help/mcp -help; ready-to-paste.mcp.jsonandclaude mcp addconfiguration included.