LSP

MCP.md

@@ -0,0 +1,153 @@
+# EasyCrypt MCP
+
+This repository includes an MCP server exposed by the EasyCrypt binary:
+
+```bash
+easycrypt mcp --stdio
+```
+
+When working from this repository without installing globally, use the built binary:
+
+```bash
+./_build/default/src/ec.exe mcp --stdio
+```
+
+The MCP server is intended to help agentic tools interact with EasyCrypt proof state and queries while editing `.ec` files.
+
+## Build
+
+Build the project first:
+
+```bash
+dune build
+```
+
+The MCP server command used below assumes the binary is:
+
+```bash
+/Users/strub/Projects/easyCrypt/vscode/_build/default/src/ec.exe
+```
+
+If your checkout lives elsewhere, adjust the path accordingly.
+
+## Codex Configuration
+
+Add the MCP server with the Codex CLI:
+
+```bash
+codex mcp add easycrypt -- /Users/strub/Projects/easyCrypt/vscode/_build/default/src/ec.exe mcp --stdio
+```
+
+Verify the configuration:
+
+```bash
+codex mcp list
+codex mcp get easycrypt --json
+```
+
+You can also configure it directly in `~/.codex/config.toml`:
+
+```toml
+[mcp_servers.easycrypt]
+command = "/Users/strub/Projects/easyCrypt/vscode/_build/default/src/ec.exe"
+args = ["mcp", "--stdio"]
+```
+
+## Claude Code Configuration
+
+Add the MCP server with the Claude Code CLI:
+
+```bash
+claude mcp add easycrypt -- /Users/strub/Projects/easyCrypt/vscode/_build/default/src/ec.exe mcp --stdio
+```
+
+You can also configure it in a project-level `.mcp.json`:
+
+```json
+{
+  "mcpServers": {
+    "easycrypt": {
+      "command": "/Users/strub/Projects/easyCrypt/vscode/_build/default/src/ec.exe",
+      "args": ["mcp", "--stdio"],
+      "env": {}
+    }
+  }
+}
+```
+
+## Recommended Agent Instructions
+
+To make agents use this MCP server reliably, add an instruction like this to your `AGENTS.md`:
+
+```md
+Always use the `easycrypt` MCP server for EasyCrypt proof work.
+
+Before proof or query operations, sync the current file into the MCP server with:
+1. `open_document` once for the file URI
+2. `apply_changes` after edits
+
+Prefer these tools:
+- `proof_next`
+- `proof_step`
+- `proof_jump_to`
+- `proof_back`
+- `proof_restart`
+- `proof_goals`
+- `query_print`
+- `query_locate`
+- `query_search`
+```
+
+## Available MCP Tools
+
+The server currently exposes these tools:
+
+- `open_document`
+- `apply_changes`
+- `close_document`
+- `proof_next`
+- `proof_step`
+- `proof_jump_to`
+- `proof_back`
+- `proof_restart`
+- `proof_goals`
+- `query_print`
+- `query_locate`
+- `query_search`
+
+## Important Usage Note
+
+The MCP server keeps its own document state. It does not automatically read the contents of your editor buffer.
+
+That means the client must:
+
+1. call `open_document` with the full text of the file
+2. call `apply_changes` after edits
+
+If the client does not do this, proof state and queries may be computed on stale text.
+
+## Typical Proof Workflow
+
+A good proof-assistant workflow is:
+
+1. `open_document` on the current `.ec` file
+2. `proof_goals` to inspect the current state
+3. `query_search` / `query_print` / `query_locate` to inspect available lemmas and objects
+4. `proof_next` to preview the next sentence
+5. `proof_step` or `proof_jump_to` to execute proof progress
+6. `apply_changes` whenever the file is edited
+
+## Example Prompt
+
+Once configured, a useful prompt is:
+
+```text
+Use the easycrypt MCP server. Open the current file, show me the current goals, inspect useful lemmas with query_search/query_print, and suggest the next proof step.
+```
+
+## References
+
+- Codex MCP configuration:
+  https://developers.openai.com/learn/docs-mcp
+- Claude Code MCP configuration:
+  https://docs.anthropic.com/en/docs/claude-code/mcp

dune-project

@@ -19,6 +19,10 @@
   dune
   dune-build-info
   dune-site
+  fmt
+  logs
+  lsp
+  lwt
   markdown
   (pcre2 (>= 8))
   (why3 (and (>= 1.8.0) (< 1.9)))

easycrypt.opam

@@ -7,6 +7,10 @@ depends: [
   "dune" {>= "3.13"}
   "dune-build-info"
   "dune-site"
+  "fmt"
+  "logs"
+  "lsp"
+  "lwt"
   "markdown"
   "pcre2" {>= "8"}
   "why3" {>= "1.8.0" & < "1.9"}

src/dune

@@ -16,15 +16,16 @@
  (public_name easycrypt.ecLib)
  (foreign_stubs (language c) (names eunix))
  (modules :standard \ ec)
- (libraries batteries camlp-streams dune-build-info dune-site inifiles markdown markdown.html pcre2 tyxml why3 yojson zarith)
+ (libraries batteries camlp-streams dune-build-info dune-site inifiles logs logs.fmt lsp lwt lwt.unix markdown markdown.html pcre2 tyxml why3 yojson zarith)
 )
 
 (executable
  (public_name easycrypt)
  (name ec)
  (modules ec)
  (promote (until-clean))
- (libraries batteries camlp-streams dune-build-info dune-site inifiles pcre2 why3 yojson zarith ecLib))
+ (libraries batteries ecLib)
+)
 
 (ocamllex ecLexer)
 

src/ec.ml

@@ -214,6 +214,12 @@ let main () =
   (* Execution of eager commands *)
   begin
     match options.o_command with
+    | `Lsp ->
+        EcLsp.run ();
+        exit 0
+    | `Mcp ->
+        EcMcp.run ();
+        exit 0
     | `Runtest input -> begin
         let root =
           match EcRelocate.sourceroot with
@@ -535,6 +541,12 @@ let main () =
     | `Runtest _ ->
         (* Eagerly executed *)
         assert false
+    | `Lsp ->
+        (* Eagerly executed *)
+        assert false
+    | `Mcp ->
+        (* Eagerly executed *)
+        assert false
 
     | `DocGen docopts -> begin
         let name = docopts.doco_input in

src/ecIo.ml

@@ -96,14 +96,15 @@ let from_string data =
 let finalize (ecreader : ecreader) =
   Disposable.dispose ecreader
 
+(* -------------------------------------------------------------------- *)
+let isfinal_token = function
+  | EcParser.FINAL _ -> true
+  | _ -> false
+
 (* -------------------------------------------------------------------- *)
 let lexer ?(checkpoint : _ I.checkpoint option) (ecreader : ecreader_r) =
   let lexbuf = ecreader.ecr_lexbuf in
 
-  let isfinal = function
-    | EcParser.FINAL _ -> true
-    | _ -> false in
-
   if ecreader.ecr_atstart then
     ecreader.ecr_trim <- ecreader.ecr_lexbuf.Lexing.lex_curr_p.pos_cnum;
 
@@ -134,7 +135,7 @@ let lexer ?(checkpoint : _ I.checkpoint option) (ecreader : ecreader_r) =
 
   ecreader.ecr_tokens  <- prequeue @ queue;
 
-  if isfinal token then
+  if isfinal_token token then
     ecreader.ecr_atstart <- true
   else
     ecreader.ecr_atstart <- ecreader.ecr_atstart && (
@@ -177,6 +178,42 @@ let parse (ecreader : ecreader) : EcParsetree.prog =
 
   in parse (EcParser.Incremental.prog ecreader.ecr_lexbuf.lex_curr_p)
 
+(* -------------------------------------------------------------------- *)
+let next_sentence_from (text : string) (start : int) : (string * int * int) option =
+  let len = String.length text in
+  if start < 0 || start >= len then
+    None
+  else
+    let sub = String.sub text start (len - start) in
+    let reader = from_string sub in
+    let ecr = Disposable.get reader in
+
+    let exception EOF in
+
+    Fun.protect
+      ~finally:(fun () -> finalize reader)
+      (fun () ->
+        try
+          begin
+            let exception Done in
+
+            try
+              while true do
+                match proj3_1 (lexer ecr) with
+                | EcParser.FINAL _ -> raise Done
+                | EcParser.EOF -> raise EOF
+                | _ -> ()
+              done
+            with Done -> ()
+          end;
+
+          let p = ecr.ecr_lexbuf.Lexing.lex_curr_p.pos_cnum - 1 in
+          let s = String.sub sub 0 p in
+
+          Some (s, start, start + p)
+        with
+        | EcLexer.LexicalError _ | EOF -> None)
+
 (* -------------------------------------------------------------------- *)
 let xparse (ecreader : ecreader) : string * EcParsetree.prog =
   let ecr = Disposable.get ecreader in

src/ecIo.mli

@@ -13,6 +13,7 @@ val parse    : ecreader -> EcParsetree.prog
 val parseall : ecreader -> EcParsetree.global list
 val drain    : ecreader -> unit
 val lexbuf   : ecreader -> Lexing.lexbuf
+val next_sentence_from : string -> int -> (string * int * int) option
 
 (* -------------------------------------------------------------------- *)
 val lex_single_token : string -> EcParser.token option