Repository navigation

[llm] agent-facing interfaces: interactive REPL and in-binary MCP server - #1019

Draft

strub wants to merge 57 commits into

mainfrom

llm-interactive

Draft

[llm] agent-facing interfaces: interactive REPL and in-binary MCP server#1019
strub wants to merge 57 commits into
mainfrom
llm-interactive

Commits on Oct 23, 2026
- Add LLM coding-agent REPL and goal-printing flags
  strub
  committed
  6465ea0
- [llm] add LOAD ... -trace for before/after sentence inspection
  strub
  committed
  42ffb91
- [llm] relax +strict_bullets in REPL, add TREE and focus tag
  strub
  committed
  9c72d71
- [llm] add FOCUS N and NEXT for explicit goal selection
  strub
  committed
  ee42a11
- [llm] add COMMIT to emit a +strict_bullets-friendly proof body
  strub
  committed
  48e15d9
- [llm] extract REPL into a dedicated EcLlm module
  strub
  committed
  576d333
- [llm] split REPL dispatcher into Parse and Dispatch submodules
  strub
  committed
  c4a7a87
- [llm] diagnose missing-argument REPL commands at parse time
  strub
  committed
  8cd4a51
- [llm] nested TREE and dotted-path FOCUS
  strub
  committed
  8fdfd1a
- [llm] update CLAUDE.md with current workflow status
  strub
  committed
  0b598d1
- [llm] add -eval STR for scripted one-shot invocations
  strub
  committed
  6337520
- [llm] use apply_pragma_option for loader pragmas (align with ec.ml compile path)
  strub
  committed
  c5315fa
- Add -stdlib DIR flag to override the built-in standard library
  strub
  committed
  6258477
- [llm] scripted -eval runs exit nonzero when any command errors
  strub
  committed
  487df4e
- [llm] LOAD applies the easycrypt.project of the loaded file
  strub
  committed
  e434fcb
- [llm] add golden-output regression harness for the REPL
  strub
  committed
  fdb45d0
- [llm] COMMIT keeps bullets when run after qed
  strub
  committed
  906016e
- [llm] COMMIT respects the LOAD prefix's open bullet frames
  strub
  committed
  085c183
- [llm] LOAD reports a missing file instead of an anomaly
  strub
  committed
  44cefc1
- [llm] queries no longer pollute the COMMIT transcript
  strub
  committed
  bc6cb7e
- [llm] tag GOALS / TREE / COMMIT replies with the focus indicator
  strub
  committed
  d41e460
- [llm] a -trace LOAD that cannot trace keeps the prefix state
  strub
  committed
  112b03d
- [llm] split ecLlm into an engine core and a text front-end
  strub
  committed
  4bdc39b
- [llm] core: TRY semantics via EcLlmCore.try_step
  strub
  committed
  77d7335
- [llm] add `easycrypt mcp`: an MCP server front-end over EcLlmCore
  strub
  committed
  ce2fbb1
- [llm] step runs every sentence of its input, not just the first
  strub
  committed
  5aac54d
- [llm] queries no longer spend a uuid
  strub
  committed
  e5b2cf4
- [llm] core computes `changed' for failures too
  strub
  committed
  e511838
- [llm] a golden harness for the MCP front-end
  strub
  committed
  5fc4373
- [llm] parity check: two front-ends, one core
  strub
  committed
  1b9cb5f
- [llm] real-client verification of `easycrypt mcp'
  strub
  committed
  5f7b211
- [llm] mcp: repeat the reply text inside structuredContent
  strub
  committed
  e517ed3
- [llm] document the MCP front-end
  strub
  committed
  96bf490
- [llm] wire the llm/mcp golden harnesses into check and CI
  strub
  committed
  a6a870f
- [llm] SEARCH takes a pattern, not a command stream
  strub
  committed
  5789c6b
- [llm] COMMIT emits sibling subtrees in DAG order, not typing order
  strub
  committed
  e055a6a
- [llm] escape envelope-shaped lines in REPL reply bodies
  strub
  committed
  a490bc5
- [llm] `print' renders inside the reply, not around it
  strub
  committed
  39083f8
- [mcp] repair non-UTF-8 bytes before they reach the wire
  strub
  committed
  a12ecad
- [llm] LOAD rewinds the include path instead of growing it
  strub
  committed
  f24b4b8
- [llm] ec_try restores the exact pre-call state, forward included
  strub
  committed
  7d599eb
- [llm] correct the documented meaning of FOCUS and NEXT
  strub
  committed
  ce30454
- [llm] COMMIT renders each proof of a session on its own
  strub
  committed
  280330c
- [llm] QUIT and `exit.` no longer defeat the -eval exit status
  strub
  committed
  4ef3cd4
- [llm] LOAD honours `upto` for every sentence kind, not just commands
  strub
  committed
  357e2ea
- [llm] drop the -upto/-lastgoals machinery the batch llm mode left behind
  strub
  committed
  f69f6e4
- [llm] cover ec_load's nosmt and trace options on the MCP side
  strub
  committed
  9562851
- [llm] `pragma restart.` drops the checkpoint table too
  strub
  committed
  1cb969d
- [llm] document the front-end-facing half of ecCommands' interface
  strub
  committed
  c9bf3cb
- [llm] count open goals for the focus tag instead of rendering them
  strub
  committed
  ee02a2c
- [llm] share the argument checks both front-ends were duplicating
  strub
  committed
  a28d067
- [mcp] stop naming the JSON constructors yojson 3 removed
  strub
  committed
  4acec00
- [llm] re-record the print goldens for the new locate prefix
  strub
  committed
  87e83e9
- [llm] LOAD -noproof: admit the prefix's lemmas instead of proving them
  
  authored and
  strub
  committed
  20139bb
- [llm] keep elaborated theories across a LOAD, so reloading is cheap
  
  authored and
  strub
  committed
  9b55e0f
- [llm] STRICT: stop the session at a failure instead of drifting past it
  
  authored and
  strub
  committed
  2d8eeb9
- [llm] mcp -sessions: one engine per agent behind one MCP server
  
  authored and
  strub
  committed
  5c90c47

Commits

Commits on Oct 23, 2026