From 3a6b7b0858204aa6799ac5e167322dae96f71cae Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 26 May 2026 21:07:24 +0200 Subject: [PATCH 01/10] Add LLM coding-agent REPL and goal-printing flags 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 ` 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 -- navigate proof state - GOALS / GOALS ALL -- inspect current or all subgoals - CHECKPOINT -- named bookmarks for branching - SEARCH -- 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 `` 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. --- doc/llm/CLAUDE.md | 272 +++++++++++++++++++++---- src/ec.ml | 493 +++++++++++++++++++++++++++++++++++++++++++--- src/ecOptions.ml | 48 ++--- src/ecOptions.mli | 4 +- 4 files changed, 708 insertions(+), 109 deletions(-) diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index 0cc20c5a3..c33dc1825 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -6,59 +6,246 @@ computations, program logics (Hoare logic, probabilistic Hoare logic, probabilistic relational Hoare logic), and ambient mathematical reasoning. -## Using the `llm` command +## Using the `llm` interactive mode -The `llm` subcommand is designed for non-interactive, LLM-friendly -batch compilation. It produces no progress bar and no `.eco` cache -files. +The `llm` subcommand provides an interactive REPL with a +machine-friendly protocol designed for LLM agents. The LLM sends +commands over stdin and receives structured responses on stdout. ``` -easycrypt llm [OPTIONS] FILE.ec +easycrypt llm [OPTIONS] ``` -### Options +Standard loader and prover options (`-I`, `-timeout`, `-p`, etc.) are +available. Use `-help` to print this guide and exit: -- `-upto LINE` or `-upto LINE:COL` — Compile up to (but not - including) the given location, then print the current goal state to - stdout and exit with code 0. Use this to inspect the proof state at - a specific point in a file. +``` +easycrypt llm -help +``` -- `-lastgoals` — On failure, print the goal state (as it was just - before the failing command) to stdout, then print the error to - stderr, and exit with code 1. Use this to understand what the - failing tactic was supposed to prove. +### Protocol -Standard loader and prover options (`-I`, `-timeout`, `-p`, etc.) are -also available. +**Startup.** EasyCrypt prints a `READY` message and waits for input: + +``` +READY [uuid:0] + +``` + +**Responses.** Every response has a typed envelope and an `` +sentinel: + +``` +OK [uuid:N] + + +``` + +``` +ERROR [uuid:N] + + +``` + +The `uuid` is a monotonically increasing integer identifying the proof +engine state. It increments with each successful command. + +### Meta-commands -### Output conventions +These are protocol-level commands, not EasyCrypt syntax: -- **Goals** are printed to **stdout**. -- **Errors** are printed to **stderr**. -- **Exit code 0** means success (or `-upto` reached its target). -- **Exit code 1** means a command failed. -- If there is no active proof at the point where goals are requested, - stdout will contain: `No active proof.` +| Command | Description | +|---------|-------------| +| `LOAD "file.ec" [LINE[:COL]] [-nosmt]` | Reset state, compile file (optionally skip SMT) | +| `UNDO` | Undo the last proof step | +| `REVERT ` | Revert to a specific state (by uuid or checkpoint name) | +| `GOALS` | Print the current goal (first subgoal only, with remaining count) | +| `GOALS ALL` | Print all subgoals | +| `CHECKPOINT ` | Save current uuid under a name for later `REVERT` | +| `SEARCH ` | Search for lemmas matching a pattern | +| `QUIET ON` / `QUIET OFF` | Suppress/enable automatic goal display after tactics | +| `` / `` | Delimit multi-line EasyCrypt input | +| `HELP` | Print this guide | +| `QUIT` | Exit | -### Workflow for writing and debugging proofs +### EasyCrypt commands -1. Try to write a pen-and-paper proof first. +Any line that is not a meta-command is parsed as EasyCrypt input. +This covers tactics, declarations, `search`, `print`, `require`, +etc. The line must be a complete EasyCrypt statement ending with `.` -2. Write the `.ec` file with your proof attempt. For a large proof, - write down skeleton and `admit` subgoals first, and then detail - the proof. +``` +smt(). +rewrite H1 H2. +search (%/). +print mulzK. +``` + +For multi-line statements, wrap with `` and ``: + +``` + +lemma test : + 0 <= n => + 0 < n + 1. + +``` + +### Workflow + +**1. Load a file up to the proof point:** -3. Run `easycrypt llm -lastgoals FILE.ec` to check the full file. - - If it succeeds (exit 0), you are done. - - If it fails (exit 1), read the error from stderr and the goal - state from stdout to understand what went wrong. +``` +LOAD "myfile.ec" 42 +``` + +This compiles the file through line 42 (processing any command whose +end is on or before that line). The response includes where it +stopped: + +``` +OK [uuid:15] [loaded:myfile.ec:42] +Current goal +... + +``` -4. Use `-upto LINE` to inspect the proof state at a specific point - without running the rest of the file. This is useful for - incremental proof development. +For large files, use `-nosmt` to skip SMT calls during prefix +compilation (safe when the prefix was already verified): -5. Fix the proof and repeat from step 2. The ultimate proof should - not contain `admit` or `admitted`. +``` +LOAD "myfile.ec" 436 -nosmt +``` + +**2. Try tactics, using REVERT to restart:** + +The uuid returned by LOAD is a revertible state. Use `REVERT` to +return to it after failed experiments — this is instant, unlike +re-doing LOAD which recompiles the prefix. + +``` +LOAD "myfile.ec" 42 +→ OK [uuid:15] [loaded:myfile.ec:42] + +smt(). ← fails, state unchanged +rewrite H1. smt(). ← succeeds (uuid:17) +rewrite H2. ← wrong direction +REVERT 17 ← back to after the successful smt() +``` + +To restart the proof from scratch, revert to the LOAD uuid: + +``` +REVERT 15 ← back to the state right after LOAD +``` + +Always note the LOAD uuid so you can return to it. + +**3. Use checkpoints for branching exploration:** + +``` +CHECKPOINT before_split +split. +smt(). ← fails +REVERT before_split +apply H. ← try a different approach +``` + +**4. Use QUIET mode to save tokens during bulk tactic application:** + +``` +QUIET ON +rewrite H1. +rewrite H2. +rewrite H3. +QUIET OFF +GOALS +``` + +**5. Search for lemmas using patterns:** + +EasyCrypt `search` uses pattern syntax, not keywords. Use `_` as +wildcard: + +``` +search (fdom _). ← lemmas involving fdom +search (_ %/ _). ← integer division lemmas +search (card (_ `|` _)). ← card of union +search (mu _ _) (_ <= _). ← mu lemmas with inequalities +``` + +The SEARCH meta-command is a shorthand that adds `search`/`.`: + +``` +SEARCH (fdom _) +SEARCH (_ %/ _) +``` + +## EasyCrypt proof strategy + +### General approach + +- Start with a pen-and-paper proof plan before writing tactics. +- Use `smt()` aggressively. Try it first — if it fails, add hints: + `smt(lemma1 lemma2)`. +- Build proofs with `have` assertions. Establish intermediate facts + as named hypotheses, then combine with `smt()`. Avoid long rewrite + chains. +- Case split early: `case (n = 0) => [->|hn0].` Base cases often + close by computation. +- Provide specific instances of lemmas to smt: + `have h := lemma arg1 arg2.` SMT works much better with ground + instances than with universally quantified axioms. + +### Integer division (`%/`) + +- `divzK`: `d %| m => m %/ d * d = m` — recovering from exact + division +- `mulzK`: `d <> 0 => m * d %/ d = m` — canceling a known factor +- `divzMpl`: `0 < p => p * m %/ (p * d) = m %/ d` — simplifying + common factors +- To prove `a %/ d = x`, establish `a = x * d` (with `d %| a`), + then use `mulzK`. +- Don't try to rewrite inside `%/` expressions directly. Instead, + prove the equality as a `have` and use it. + +### What works, what doesn't + +- `ring` solves polynomial equalities over integers but treats + abstract ops (like `fact`) as opaque. It **cannot** simplify + `fact(n-1+1)` to `fact(n)`. +- `smt()` can do linear arithmetic and combine hypotheses, but + struggles with nonlinear integer division. Pre-compute key facts + with `have` and `divzK`/`mulzK`, then let smt combine them. +- `rewrite {k}h` rewrites the k-th occurrence only. Essential when a + term appears on both sides of an equation. +- For induction on naturals: `elim/natind: n` gives base (`n ≤ 0`) + and step (`0 ≤ n → P n → P (n+1)`). + +### SMT usage + +`smt()` and `/#` are equivalent — both call external SMT solvers. + +- Use `smt()` **only** on goals that are pure arithmetic or pure + propositional logic. If the goal contains abstract operators, + FMap terms, or `if-then-else`, reduce it first with `rewrite`, + `case`, or `have` before calling `smt()`. +- If `smt()` takes more than 1 second, the goal is too complex. + Simplify with interactive tactics instead of increasing the + timeout. + +### Common pitfalls + +- `rewrite (factS n) //` generates a side goal `0 <= n`. Use + `first smt()` or provide the precondition explicitly. +- `by` closes **all** remaining subgoals. If it fails, the error + refers to the first unclosed goal, which may not be the intended + one. +- When a tactic generates multiple subgoals, each subgoal must be + closed in order. Use `GOALS ALL` to see them all. +- `rewrite lemma in H` modifies hypothesis `H` in place (it does + not consume it). If you need to preserve the original, copy it + first: `have H' := H; rewrite lemma in H'`. ## EasyCrypt language overview @@ -91,8 +278,6 @@ proof. by ring. qed. ### Common tactics - - - `trivial` — solve trivial goals - `smt` / `smt(lemmas...)` — call SMT solvers, optionally with hints - `auto` — automatic reasoning @@ -141,9 +326,10 @@ proof. by ring. qed. ### Guidelines -* Use SMT solver only in direct mode (smt() or /#) on simple goals (arithmetic goals, pure logical goals). +* Use SMT solver only in direct mode (smt() or /#) on simple goals + (arithmetic goals, pure logical goals). * Refrain from unfolding operator definitions unless necessary. - If you need more properties on an operator, state this property in a dedicated lemma, - but avoid unfolding definitions in higher level proofs. - + If you need more properties on an operator, state this property + in a dedicated lemma, but avoid unfolding definitions in higher + level proofs. diff --git a/src/ec.ml b/src/ec.ml index 2b8b6f7d1..73845495d 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -404,6 +404,469 @@ let main () = (* Register user messages printers *) begin let open EcUserMessages in register () end; + (* -------------------------------------------------------------------- *) + (* LLM interactive mode *) + (* -------------------------------------------------------------------- *) + + let llm_guide_path () = + let (module Sites) = EcRelocate.sites in + match EcRelocate.sourceroot with + | Some root -> + Filename.concat (Filename.concat root "doc/llm") "CLAUDE.md" + | None -> + Filename.concat Sites.doc "llm-guide.md" + in + + let print_llm_guide () = + let path = llm_guide_path () in + try + let ic = open_in path in + begin try while true do + print_char (input_char ic) + done with End_of_file -> () end; + close_in ic + with Sys_error e -> + Printf.eprintf "cannot read LLM guide: %s\n%!" e + in + + let run_llm_repl (llmopts : llm_option) = + if llmopts.llmo_help then begin + print_llm_guide (); + exit 0 + end; + + let prvopts = llmopts.llmo_provers in + (* Initialize PRNG *) + Random.self_init (); + + (* Connect to external Why3 server if requested *) + prvopts.prvo_why3server |> oiter (fun server -> + try + Why3.Prove_client.connect_external server + with Why3.Prove_client.ConnectionError e -> + Format.eprintf + "cannot connect to Why3 server `%s': %s" server e; + exit 1); + + (* Add current directory to load path *) + (match relocdir with + | None -> EcCommands.addidir Filename.current_dir_name + | Some pwd -> EcCommands.addidir pwd); + + (* Proof engine configuration *) + let checkmode = { + EcCommands.cm_checkall = prvopts.prvo_checkall; + EcCommands.cm_timeout = odfl 3 prvopts.prvo_timeout; + EcCommands.cm_cpufactor = odfl 1 prvopts.prvo_cpufactor; + EcCommands.cm_nprovers = odfl 4 prvopts.prvo_maxjobs; + EcCommands.cm_provers = prvopts.prvo_provers; + EcCommands.cm_quorum = prvopts.prvo_quorum; + EcCommands.cm_profile = prvopts.prvo_profile; + } in + + (* Notice buffer: collects messages during command processing *) + let notices = Buffer.create 256 in + + let notifier (_ : EcGState.loglevel) (lazy msg) = + Buffer.add_string notices msg; + Buffer.add_char notices '\n' + in + + let initialized = ref false in + + let do_initialize () = + EcCommands.initialize + ~restart:!initialized ~undo:true + ~boot:ldropts.ldro_boot ~checkmode ~checkproof:true; + initialized := true; + (try + List.iter EcCommands.apply_pragma prvopts.prvo_pragmas + with EcCommands.InvalidPragma x -> + EcScope.hierror "invalid pragma: `%s'\n%!" x); + EcCommands.addnotifier notifier; + oiter (fun ppwidth -> + let gs = EcEnv.gstate (EcScope.env (EcCommands.current ())) in + EcGState.setvalue "PP:width" (`Int ppwidth) gs) + prvopts.prvo_ppwidth + in + + (* Error formatting *) + let format_error ?(src="") e = + let base = match e with + | EcScope.TopError (loc, e) -> + let msg = String.strip (EcPException.tostring e) in + if loc = EcLocation._dummy then msg + else Format.asprintf "%s: %s" (EcLocation.tostring loc) msg + | e -> + String.strip (EcPException.tostring e) + in + if src = "" then base + else Printf.sprintf "%s\nsource: %s" base src + in + + (* Output helpers *) + let goals_to_string ?(all=false) () = + let buf = Buffer.create 256 in + let fmt = Format.formatter_of_buffer buf in + EcCommands.pp_current_goal_or_noproof ~all fmt; + Format.pp_print_flush fmt (); + Buffer.contents buf + in + + let quiet = ref false in + + let checkpoints : (string, int) Hashtbl.t = Hashtbl.create 16 in + + let reply_ok ?(tag="") body = + let n = Buffer.contents notices in + Printf.printf "OK [uuid:%d]%s\n" (EcCommands.uuid ()) tag; + if n <> "" then print_string n; + if body <> "" then begin + print_string body; + let len = String.length body in + if len > 0 && body.[len - 1] <> '\n' then + print_char '\n' + end; + Printf.printf "\n%!"; + Buffer.clear notices + in + + let reply_ok_goals ?(all=false) () = + if !quiet then reply_ok "" + else reply_ok (goals_to_string ~all ()) + in + + let reply_error msg = + let goals = goals_to_string () in + Printf.printf "ERROR [uuid:%d]\n%s\n" (EcCommands.uuid ()) msg; + if goals <> "" then begin + print_string goals; + let len = String.length goals in + if len > 0 && goals.[len - 1] <> '\n' then + print_char '\n' + end; + Printf.printf "\n%!"; + Buffer.clear notices + in + + (* Process a single EasyCrypt command, respecting gl_fail *) + let process_action ~src (p : EP.global) = + let loc = p.EP.gl_action.EcLocation.pl_loc in + let succeeded = ref false in + begin try + ignore (EcCommands.process ~src p.EP.gl_action : float option); + succeeded := true + with + | EcCommands.Restart -> raise EcCommands.Restart + | _ when p.EP.gl_fail -> () + | e -> raise (EcScope.toperror_of_exn ~gloc:loc e) + end; + if !succeeded && p.EP.gl_fail then + raise (EcScope.toperror_of_exn ~gloc:loc + (EcScope.HiScopeError (None, + "this command is expected to fail"))) + in + + (* Process EasyCrypt input from a string (one parsed program) *) + let process_ec_input input = + Buffer.clear notices; + let reader = EcIo.from_string input in + let last_src = ref "" in + begin try + let (src, prog) = EcIo.xparse reader in + let src = String.strip src in + last_src := src; + begin match EcLocation.unloc prog with + | EP.P_Prog (commands, _) -> + List.iter (process_action ~src) commands; + reply_ok_goals () + | EP.P_Undo i -> + EcCommands.undo i; + reply_ok_goals () + | EP.P_Exit -> + EcIo.finalize reader; exit 0 + | EP.P_DocComment doc -> + EcCommands.doc_comment doc; + reply_ok "" + end + with + | EcCommands.Restart -> + do_initialize (); + reply_ok "Session restarted" + | e -> + reply_error (format_error ~src:!last_src e) + end; + EcIo.finalize reader + in + + (* Handle LOAD "file.ec" [LINE[:COL]] *) + let handle_load args = + Buffer.clear notices; + let args = String.strip args in + let last_src = ref "" in + + try + (* Parse quoted or unquoted filename *) + let filename, rest = + if String.length args > 0 && args.[0] = '"' then + let close = + try String.index_from args 1 '"' + with Not_found -> + failwith "LOAD: unterminated filename" + in + let fn = String.sub args 1 (close - 1) in + let rest = String.strip ( + String.sub args (close + 1) + (String.length args - close - 1)) in + (fn, rest) + else + match String.split_on_char ' ' args with + | [] -> failwith "LOAD: missing filename" + | [f] -> (f, "") + | f :: rest -> (f, String.concat " " rest) + in + + (* Parse optional LINE[:COL] and flags (-nosmt) *) + let upto, nosmt = + if rest = "" then (None, false) + else + let words = String.split_on_char ' ' rest in + let words = List.filter (fun s -> s <> "") words in + let nosmt = List.mem "-nosmt" words in + let words = List.filter (fun s -> s <> "-nosmt") words in + let upto = match words with + | [] -> None + | [w] -> + begin match String.split_on_char ':' w with + | [line] -> + Some (int_of_string line, None) + | [line; col] -> + Some (int_of_string line, Some (int_of_string col)) + | _ -> failwith "LOAD: invalid LINE[:COL] format" + end + | _ -> failwith "LOAD: unexpected arguments" + in + (upto, nosmt) + in + + (* Validate file extension *) + begin try + ignore (EcLoader.getkind + (Filename.extension filename) : EcLoader.kind) + with EcLoader.BadExtension ext -> + failwith (Format.sprintf + "unknown file extension: %s" ext) + end; + + (* Reset proof engine and process file *) + do_initialize (); + Hashtbl.clear checkpoints; + EcCommands.addidir (Filename.dirname filename); + + let reader = EcIo.from_file filename in + + let past_upto (loc : EcLocation.t) = + match upto with + | None -> false + | Some (line, col) -> + let (el, ec) = loc.loc_end in + el > line || (el = line && match col with + | None -> false + | Some c -> ec > c) + in + + let last_loc = ref None in + + (* In -nosmt mode, admit all SMT calls during prefix loading *) + if nosmt then EcCommands.pragma_check `WeakCheck; + + begin try while true do + let (src, prog) = EcIo.xparse reader in + let src = String.strip src in + last_src := src; + match EcLocation.unloc prog with + | EP.P_Prog (commands, locterm) -> + List.iter (fun p -> + let loc = p.EP.gl_action.EcLocation.pl_loc in + if past_upto loc then raise Exit; + process_action ~src p; + last_loc := Some loc + ) commands; + if locterm then raise Exit + | EP.P_Undo i -> + EcCommands.undo i + | EP.P_Exit -> + raise Exit + | EP.P_DocComment doc -> + EcCommands.doc_comment doc + done with + | Exit | End_of_file -> () + | e -> + EcIo.finalize reader; + if nosmt then EcCommands.pragma_check `Check; + raise e + end; + + EcIo.finalize reader; + + (* Restore full SMT checking for interactive tactics *) + if nosmt then EcCommands.pragma_check `Check; + + let tag = + match !last_loc with + | None -> "" + | Some loc -> + let (el, _) = loc.EcLocation.loc_end in + Printf.sprintf " [loaded:%s:%d]" filename el + in + reply_ok ~tag (goals_to_string ()) + + with + | EcCommands.Restart -> + do_initialize (); + Hashtbl.clear checkpoints; + reply_ok "Session restarted" + | Failure s -> + reply_error s + | e -> + reply_error (format_error ~src:!last_src e) + in + + (* Initialize proof engine *) + do_initialize (); + + (* Signal ready *) + Printf.printf "READY [uuid:%d]\n\n%!" + (EcCommands.uuid ()); + + (* Main REPL loop *) + let multi_buf = Buffer.create 256 in + let in_multi = ref false in + + begin try while true do + let line = input_line stdin in + let line = String.strip line in + + (* Multi-line input: starts, flushes *) + if line = "" then begin + Buffer.clear multi_buf; + in_multi := true + end + else if line = "" && !in_multi then begin + let input = Buffer.contents multi_buf in + Buffer.clear multi_buf; + in_multi := false; + if input <> "" then process_ec_input input + end + else if !in_multi then begin + if Buffer.length multi_buf > 0 then + Buffer.add_char multi_buf ' '; + Buffer.add_string multi_buf line + end + + else if line = "" then + () + else if line = "QUIT" then + exit 0 + else if line = "HELP" then begin + Buffer.clear notices; + let buf = Buffer.create 4096 in + let path = llm_guide_path () in + begin try + let ic = open_in path in + begin try while true do + Buffer.add_char buf (input_char ic) + done with End_of_file -> () end; + close_in ic; + reply_ok (Buffer.contents buf) + with Sys_error e -> + reply_error (Printf.sprintf "cannot read guide: %s" e) + end + end + else if line = "UNDO" then begin + Buffer.clear notices; + let uuid = EcCommands.uuid () in + if uuid > 0 then begin + EcCommands.undo (uuid - 1); + reply_ok_goals () + end else + reply_error "nothing to undo" + end + else if line = "GOALS ALL" then begin + Buffer.clear notices; + reply_ok (goals_to_string ~all:true ()) + end + else if line = "GOALS" then begin + Buffer.clear notices; + reply_ok (goals_to_string ()) + end + else if String.starts_with line "CHECKPOINT " then begin + Buffer.clear notices; + let name = String.strip ( + String.sub line 11 (String.length line - 11)) in + if name = "" then + reply_error "CHECKPOINT: missing name" + else begin + Hashtbl.replace checkpoints name (EcCommands.uuid ()); + reply_ok (Printf.sprintf + "checkpoint '%s' set at uuid %d" name (EcCommands.uuid ())) + end + end + else if String.starts_with line "REVERT " then begin + Buffer.clear notices; + let n = String.strip ( + String.sub line 7 (String.length line - 7)) in + let target = + try Some (int_of_string n) + with Failure _ -> Hashtbl.find_opt checkpoints n + in + begin match target with + | None -> + reply_error (Printf.sprintf + "REVERT: '%s' is not a valid uuid or checkpoint name" n) + | Some target -> + let uuid = EcCommands.uuid () in + if target < 0 || target > uuid then + reply_error (Printf.sprintf + "REVERT: uuid %d out of range [0, %d]" target uuid) + else begin + EcCommands.undo target; + reply_ok_goals () + end + end + end + else if line = "QUIET ON" then begin + Buffer.clear notices; + quiet := true; + reply_ok "" + end + else if line = "QUIET OFF" then begin + Buffer.clear notices; + quiet := false; + reply_ok "" + end + else if String.starts_with line "SEARCH " then begin + let query = String.strip ( + String.sub line 7 (String.length line - 7)) in + let query = + if String.ends_with query "." + then String.sub query 0 (String.length query - 1) + else query + in + process_ec_input (Printf.sprintf "search %s." query) + end + else if String.starts_with line "LOAD " then + handle_load (String.sub line 5 (String.length line - 5)) + else + (* Treat as EasyCrypt input *) + process_ec_input line + done with + | End_of_file -> () + end; + + exit 0 + in + (* Initialize I/O + interaction module *) let module State = struct type t = { @@ -535,34 +998,8 @@ let main () = end - | `Llm llmopts -> begin - let name = llmopts.llmo_input in - - begin try - let ext = Filename.extension name in - ignore (EcLoader.getkind ext : EcLoader.kind) - with EcLoader.BadExtension ext -> - Format.eprintf "do not know what to do with %s@." ext; - exit 1 - end; - - let lastgoals = llmopts.llmo_lastgoals in - let terminal = - lazy (T.from_channel ~name ~progress:`Silent ~lastgoals (open_in name)) - in - - { prvopts = llmopts.llmo_provers - ; input = Some name - ; terminal = terminal - ; interactive = false - ; eco = true - ; gccompact = None - ; docgen = false - ; outdirp = None - ; upto = llmopts.llmo_upto - ; trace = None } - - end + | `Llm llmopts -> + run_llm_repl llmopts | `Runtest _ -> (* Eagerly executed *) diff --git a/src/ecOptions.ml b/src/ecOptions.ml index bd21a69aa..3e6dc5c5c 100644 --- a/src/ecOptions.ml +++ b/src/ecOptions.ml @@ -49,10 +49,8 @@ and doc_option = { } and llm_option = { - llmo_input : string; llmo_provers : prv_options; - llmo_lastgoals : bool; - llmo_upto : (int * int option) option; + llmo_help : bool; } and prv_options = { @@ -370,11 +368,10 @@ let specs = { `Spec ("trace" , `Flag , "Save all goals & messages in .eco"); `Spec ("compact", `Int , "")]); - ("llm", "LLM-friendly batch compilation", [ + ("llm", "LLM-friendly interactive mode", [ `Group "loader"; `Group "provers"; - `Spec ("lastgoals" , `Flag , "Print last unproved goals on failure"); - `Spec ("upto" , `String, "Compile up to LINE or LINE:COL and print goals")]); + `Spec ("help", `Flag, "Print the LLM agent guide and exit")]); ("cli", "Run EasyCrypt top-level", [ `Group "loader"; @@ -562,26 +559,9 @@ let doc_options_of_values values input = { doco_input = input; doco_outdirp = get_string "outdir" values; } -let parse_upto values = - get_string "upto" values |> Option.map (fun s -> - let invalid () = - raise (Arg.Bad (Printf.sprintf - "invalid -upto format: expected LINE or LINE:COL, got %S" s)) in - match String.split_on_char ':' s with - | [line] -> - let line = try int_of_string line with Failure _ -> invalid () in - (line, None) - | [line; col] -> - let line = try int_of_string line with Failure _ -> invalid () in - let col = try int_of_string col with Failure _ -> invalid () in - (line, Some col) - | _ -> invalid ()) - -let llm_options_of_values ini values input = - { llmo_input = input; - llmo_provers = prv_options_of_values ini values; - llmo_lastgoals = get_flag "lastgoals" values; - llmo_upto = parse_upto values; } +let llm_options_of_values ini values = + { llmo_provers = prv_options_of_values ini values; + llmo_help = get_flag "help" values; } (* -------------------------------------------------------------------- *) let parse getini argv = @@ -654,16 +634,14 @@ let parse getini argv = raise (Arg.Bad "this command takes a single input file as argument") end - | "llm" -> begin - match anons with - | [input] -> - let ini = getini (Some input) in - let cmd = `Llm (llm_options_of_values ini values input) in - (cmd, ini, true) + | "llm" -> + if not (List.is_empty anons) then + raise (Arg.Bad "this command does not take arguments"); - | _ -> - raise (Arg.Bad "this command takes a single argument") - end + let ini = getini None in + let cmd = `Llm (llm_options_of_values ini values) in + + (cmd, ini, true) | _ -> assert false diff --git a/src/ecOptions.mli b/src/ecOptions.mli index a5c09b11d..f00aef075 100644 --- a/src/ecOptions.mli +++ b/src/ecOptions.mli @@ -45,10 +45,8 @@ and doc_option = { } and llm_option = { - llmo_input : string; llmo_provers : prv_options; - llmo_lastgoals : bool; - llmo_upto : (int * int option) option; + llmo_help : bool; } and prv_options = { From 1dec301e4b0ebfbba2c715d4e915959ccdaadd61 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 27 May 2026 05:01:33 +0200 Subject: [PATCH 02/10] [llm] add LOAD ... -trace for before/after sentence inspection 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) === === TACTIC (lines L:C - L':C') === === AFTER: line L (col C) === === 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 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. --- doc/llm/CLAUDE.md | 23 +++++- src/ec.ml | 188 ++++++++++++++++++++++++++++++++++++++------- src/ecCommands.ml | 5 +- src/ecCommands.mli | 1 + 4 files changed, 186 insertions(+), 31 deletions(-) diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index c33dc1825..7918f21fe 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -56,7 +56,7 @@ These are protocol-level commands, not EasyCrypt syntax: | Command | Description | |---------|-------------| -| `LOAD "file.ec" [LINE[:COL]] [-nosmt]` | Reset state, compile file (optionally skip SMT) | +| `LOAD "file.ec" [LINE[:COL]] [-nosmt] [-trace]` | Reset state, compile file (optionally skip SMT or trace last sentence) | | `UNDO` | Undo the last proof step | | `REVERT ` | Revert to a specific state (by uuid or checkpoint name) | | `GOALS` | Print the current goal (first subgoal only, with remaining count) | @@ -117,6 +117,27 @@ compilation (safe when the prefix was already verified): LOAD "myfile.ec" 436 -nosmt ``` +Add `-trace` to a LOAD to inspect the proof state around the last +loaded sentence. The reply body contains four delimited blocks: + +``` +LOAD "myfile.ec" 42 -trace + +=== BEFORE: line 42 (col 0) === + +=== TACTIC (lines 42:0 - 42:10) === + +=== AFTER: line 42 (col 0) === + +=== SUMMARY === +open goals: N1 -> N2 +``` + +The position comes from the existing `LINE[:COL]` argument; omit it to +trace the file's last sentence. On tactic failure the reply uses the +`ERROR` envelope and still includes the BEFORE/TACTIC blocks plus an +`` marker in the AFTER block. + **2. Try tactics, using REVERT to restart:** The uuid returned by LOAD is a revertible state. Use `REVERT` to diff --git a/src/ec.ml b/src/ec.ml index 73845495d..3e57da5be 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -604,6 +604,8 @@ let main () = Buffer.clear notices; let args = String.strip args in let last_src = ref "" in + let trace_prefix = ref "" in + let exception Trace_failed of exn in try (* Parse quoted or unquoted filename *) @@ -626,27 +628,32 @@ let main () = | f :: rest -> (f, String.concat " " rest) in - (* Parse optional LINE[:COL] and flags (-nosmt) *) - let upto, nosmt = - if rest = "" then (None, false) - else - let words = String.split_on_char ' ' rest in - let words = List.filter (fun s -> s <> "") words in - let nosmt = List.mem "-nosmt" words in - let words = List.filter (fun s -> s <> "-nosmt") words in - let upto = match words with - | [] -> None - | [w] -> - begin match String.split_on_char ':' w with - | [line] -> - Some (int_of_string line, None) - | [line; col] -> - Some (int_of_string line, Some (int_of_string col)) - | _ -> failwith "LOAD: invalid LINE[:COL] format" - end - | _ -> failwith "LOAD: unexpected arguments" - in - (upto, nosmt) + (* Parse optional LINE[:COL] and flags (-nosmt, -trace) *) + let upto, nosmt, trace = + let words = + String.split_on_char ' ' rest + |> List.filter (fun s -> s <> "") + in + let nosmt = List.mem "-nosmt" words in + let trace = List.mem "-trace" words in + let words = + List.filter + (fun s -> s <> "-nosmt" && s <> "-trace") + words + in + let upto = match words with + | [] -> None + | [w] -> + begin match String.split_on_char ':' w with + | [line] -> + Some (int_of_string line, None) + | [line; col] -> + Some (int_of_string line, Some (int_of_string col)) + | _ -> failwith "LOAD: invalid LINE[:COL] format" + end + | _ -> failwith "LOAD: unexpected arguments" + in + (upto, nosmt, trace) in (* Validate file extension *) @@ -677,27 +684,65 @@ let main () = let last_loc = ref None in + (* For -trace: lazy whole-file bytes, used to slice the exact + source text of a sentence by byte offsets. *) + let input_bytes = lazy ( + let ic = open_in_bin filename in + let n = in_channel_length ic in + let b = Bytes.create n in + really_input ic b 0 n; + close_in ic; + Bytes.unsafe_to_string b) + in + let sentence_source (loc : EcLocation.t) = + let s = Lazy.force input_bytes in + let lo = max 0 loc.EcLocation.loc_bchar in + let hi = min (String.length s) loc.EcLocation.loc_echar in + if hi <= lo then "" else String.sub s lo (hi - lo) + in + + (* For -trace: defer execution of the last sentence within the + prefix so we can capture goals before and after it. *) + let pending : (string * EP.global) option ref = ref None in + let flush_pending () = + match !pending with + | None -> () + | Some (src, p) -> + last_src := src; + process_action ~src p; + last_loc := Some p.EP.gl_action.EcLocation.pl_loc; + pending := None + in + let step src p = + let loc = p.EP.gl_action.EcLocation.pl_loc in + if past_upto loc then raise Exit; + if trace then begin + flush_pending (); + pending := Some (src, p) + end else begin + last_src := src; + process_action ~src p; + last_loc := Some loc + end + in + (* In -nosmt mode, admit all SMT calls during prefix loading *) if nosmt then EcCommands.pragma_check `WeakCheck; begin try while true do let (src, prog) = EcIo.xparse reader in let src = String.strip src in - last_src := src; match EcLocation.unloc prog with | EP.P_Prog (commands, locterm) -> - List.iter (fun p -> - let loc = p.EP.gl_action.EcLocation.pl_loc in - if past_upto loc then raise Exit; - process_action ~src p; - last_loc := Some loc - ) commands; + List.iter (step src) commands; if locterm then raise Exit | EP.P_Undo i -> + last_src := src; EcCommands.undo i | EP.P_Exit -> raise Exit | EP.P_DocComment doc -> + last_src := src; EcCommands.doc_comment doc done with | Exit | End_of_file -> () @@ -712,6 +757,88 @@ let main () = (* Restore full SMT checking for interactive tactics *) if nosmt then EcCommands.pragma_check `Check; + (* If -trace is set, the last in-prefix sentence is still + pending. Run it with goal capture before and after, and + build the BEFORE/TACTIC/AFTER/SUMMARY response body. *) + let body = + if not trace then + goals_to_string () + else + let pre_state = + match !pending with + | None -> `Nothing + | Some _ when not (EcCommands.in_proof ()) -> `NotInProof + | Some (src, p) -> `Ready (src, p) + in + match pre_state with + | `Nothing -> failwith "trace: nothing to trace" + | `NotInProof -> + failwith + "trace: target sentence is not in a proof context" + | `Ready (src, p) -> + let loc = p.EP.gl_action.EcLocation.pl_loc in + let (sl, sc) = loc.EcLocation.loc_start in + let (el, ec) = loc.EcLocation.loc_end in + let before_goals = EcCommands.pp_all_goals () in + let n1 = List.length before_goals in + let buf = Buffer.create 1024 in + let fmt = Format.formatter_of_buffer buf in + Format.fprintf fmt + "=== BEFORE: line %d (col %d) ===@\n" sl sc; + EcCommands.pp_current_goal_or_noproof ~all:false fmt; + Format.fprintf fmt + "@\n=== TACTIC (lines %d:%d - %d:%d) ===@\n%s@\n@\n" + sl sc el ec (sentence_source loc); + last_src := src; + begin + try + process_action ~src p; + last_loc := Some loc; + pending := None; + let after_goals = EcCommands.pp_all_goals () in + let n2 = List.length after_goals in + Format.fprintf fmt + "=== AFTER: line %d (col %d) ===@\n" sl sc; + let before_set = + List.fold_left + (fun s g -> EcMaps.Sstr.add g s) + EcMaps.Sstr.empty before_goals + in + (* The new focused goal always counts as "modified" + (its focus status changed even if its text matches + an old sibling); the rest are printed only if + they didn't appear in BEFORE. *) + let to_print = + match after_goals with + | [] -> [] + | head :: tl -> + head :: + List.filter + (fun g -> not (EcMaps.Sstr.mem g before_set)) + tl + in + begin match to_print with + | [] -> Format.fprintf fmt "(no open goals)@\n" + | _ -> + List.iteri (fun i g -> + if i > 0 then Format.fprintf fmt "@\n"; + Format.fprintf fmt "%s@\n" g) + to_print + end; + Format.fprintf fmt + "@\n=== SUMMARY ===@\nopen goals: %d -> %d@\n" n1 n2; + Format.pp_print_flush fmt (); + Buffer.contents buf + with e -> + Format.fprintf fmt + "=== AFTER: line %d (col %d) ===@\n@\n" + sl sc; + Format.pp_print_flush fmt (); + trace_prefix := Buffer.contents buf; + raise (Trace_failed e) + end + in + let tag = match !last_loc with | None -> "" @@ -719,13 +846,16 @@ let main () = let (el, _) = loc.EcLocation.loc_end in Printf.sprintf " [loaded:%s:%d]" filename el in - reply_ok ~tag (goals_to_string ()) + reply_ok ~tag body with | EcCommands.Restart -> do_initialize (); Hashtbl.clear checkpoints; reply_ok "Session restarted" + | Trace_failed e -> + let msg = format_error ~src:!last_src e in + reply_error (!trace_prefix ^ msg) | Failure s -> reply_error s | e -> diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 8cdbf561e..2a5b75fa7 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -1127,8 +1127,11 @@ let pp_current_goal ?(all = false) stream = end (* -------------------------------------------------------------------- *) +let in_proof () = + Option.is_some (S.xgoal (current ())) + let pp_current_goal_or_noproof ?(all = false) stream = - if Option.is_some (S.xgoal (current ())) then + if in_proof () then pp_current_goal ~all stream else Format.fprintf stream "No active proof.@\n%!" diff --git a/src/ecCommands.mli b/src/ecCommands.mli index 8a1220ae0..88c119efb 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -64,6 +64,7 @@ val pp_current_goal : ?all:bool -> Format.formatter -> unit val pp_current_goal_or_noproof : ?all:bool -> Format.formatter -> unit val pp_maybe_current_goal : Format.formatter -> unit val pp_all_goals : unit -> string list +val in_proof : unit -> bool (* -------------------------------------------------------------------- *) val pragma_verbose : bool -> unit From 2f1c51528e203de9fb9b3c2821fc68eeead8299b Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 30 May 2026 06:58:45 +0200 Subject: [PATCH 03/10] [llm] relax +strict_bullets in REPL, add TREE and focus tag 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. --- doc/llm/CLAUDE.md | 11 +++++++- src/ec.ml | 66 +++++++++++++++++++++++++++++++++++++++++----- src/ecCommands.ml | 53 +++++++++++++++++++++++++++++++++++++ src/ecCommands.mli | 2 ++ src/ecScope.ml | 4 +++ src/ecScope.mli | 1 + 6 files changed, 129 insertions(+), 8 deletions(-) diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index 7918f21fe..1b7a3b066 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -61,6 +61,8 @@ These are protocol-level commands, not EasyCrypt syntax: | `REVERT ` | Revert to a specific state (by uuid or checkpoint name) | | `GOALS` | Print the current goal (first subgoal only, with remaining count) | | `GOALS ALL` | Print all subgoals | +| `TREE` | List open subgoals as `[N] `, marking the focused one | +| `TREE ALL` | Same as `TREE`, but with full goal bodies | | `CHECKPOINT ` | Save current uuid under a name for later `REVERT` | | `SEARCH ` | Search for lemmas matching a pattern | | `QUIET ON` / `QUIET OFF` | Suppress/enable automatic goal display after tactics | @@ -263,7 +265,14 @@ SEARCH (_ %/ _) refers to the first unclosed goal, which may not be the intended one. - When a tactic generates multiple subgoals, each subgoal must be - closed in order. Use `GOALS ALL` to see them all. + closed in order. Use `GOALS ALL` or `TREE` to see them all. +- When more than one subgoal is open, replies carry a + `[focus: k/N]` tag (e.g. `OK [uuid:42] [focus: 1/3]`) so you know + which one the next tactic will hit. +- `pragma +strict_bullets` does **not** apply to REPL input. Files + loaded via `LOAD` still respect their own pragmas, but tactics typed + at the REPL prompt are never rejected for missing bullets — the + REPL is the focus mechanism. - `rewrite lemma in H` modifies hypothesis `H` in place (it does not consume it). If you need to preserve the original, copy it first: `have H' := H; rewrite lemma in H'`. diff --git a/src/ec.ml b/src/ec.ml index 3e57da5be..592157fe7 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -513,6 +513,38 @@ let main () = Buffer.contents buf in + (* Render the focus-tree of open subgoals. [all=false] gives a + one-line digest per goal (conclusion truncated); [all=true] + gives the full goal body for each. *) + let tree_to_string ?(all=false) () = + let entries = EcCommands.pp_tree ~all () in + match entries with + | [] -> "No active proof.\n" + | _ -> + let buf = Buffer.create 256 in + let one_line s = + let s = + match String.index_opt s '\n' with + | None -> s + | Some k -> String.sub s 0 k + in + let limit = 80 in + if String.length s > limit + then String.sub s 0 (limit - 1) ^ "…" + else s + in + List.iter (fun (i, focused, text) -> + let marker = if focused then " <- focused" else "" in + if all then + Buffer.add_string buf + (Printf.sprintf "[%d]%s\n%s\n" i marker text) + else + Buffer.add_string buf + (Printf.sprintf "[%d] %s%s\n" i (one_line text) marker) + ) entries; + Buffer.contents buf + in + let quiet = ref false in let checkpoints : (string, int) Hashtbl.t = Hashtbl.create 16 in @@ -531,9 +563,17 @@ let main () = Buffer.clear notices in + let focus_tag () = + match EcCommands.pp_tree () with + | _ :: _ :: _ as entries -> + Printf.sprintf " [focus: 1/%d]" (List.length entries) + | _ -> "" + in + let reply_ok_goals ?(all=false) () = - if !quiet then reply_ok "" - else reply_ok (goals_to_string ~all ()) + let tag = focus_tag () in + if !quiet then reply_ok ~tag "" + else reply_ok ~tag (goals_to_string ~all ()) in let reply_error msg = @@ -570,6 +610,7 @@ let main () = (* Process EasyCrypt input from a string (one parsed program) *) let process_ec_input input = Buffer.clear notices; + EcCommands.disable_repl_bullets (); let reader = EcIo.from_string input in let last_src = ref "" in begin try @@ -840,11 +881,14 @@ let main () = in let tag = - match !last_loc with - | None -> "" - | Some loc -> - let (el, _) = loc.EcLocation.loc_end in - Printf.sprintf " [loaded:%s:%d]" filename el + let loaded = + match !last_loc with + | None -> "" + | Some loc -> + let (el, _) = loc.EcLocation.loc_end in + Printf.sprintf " [loaded:%s:%d]" filename el + in + loaded ^ focus_tag () in reply_ok ~tag body @@ -930,6 +974,14 @@ let main () = Buffer.clear notices; reply_ok (goals_to_string ()) end + else if line = "TREE ALL" then begin + Buffer.clear notices; + reply_ok (tree_to_string ~all:true ()) + end + else if line = "TREE" then begin + Buffer.clear notices; + reply_ok (tree_to_string ()) + end else if String.starts_with line "CHECKPOINT " then begin Buffer.clear notices; let name = String.strip ( diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 2a5b75fa7..f1da34df3 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -987,6 +987,28 @@ let push_context scope context = ct_stack = context.ct_stack |> omap (fun st -> context.ct_current :: st); } +(* -------------------------------------------------------------------- *) +(* Disable bullet enforcement for REPL-driven phrases. Drops the global + pragma so newly-opened proofs have no bullet stack, and clears the + stack on any currently active proof so REPL phrases are not checked + against it. Idempotent. Does not advance the undo level. *) +let disable_repl_bullets () = + pragma_strict_bullets false; + match !context with + | None -> () + | Some ctxt -> + match EcScope.xgoal ctxt.ct_current with + | None -> () + | Some puc -> + match puc.EcScope.puc_active with + | None -> () + | Some (pac, _) when pac.EcScope.puc_bullets = None -> () + | Some (pac, pct) -> + let pac = { pac with EcScope.puc_bullets = None } in + let puc = { puc with EcScope.puc_active = Some (pac, pct) } in + let scope = EcScope.set_xgoal ctxt.ct_current puc in + context := Some { ctxt with ct_current = scope } + (* -------------------------------------------------------------------- *) let initialize ~restart ~undo ~boot ~checkmode ~checkproof = assert (restart || EcUtils.is_none !context); @@ -1169,3 +1191,34 @@ let pp_all_goals () = end | _ -> [] + +(* -------------------------------------------------------------------- *) +(* Render the open-subgoals tree. Each entry is (index, is_focused, + text). [index] is 1-based, [is_focused] marks the focused goal + (always at index 1 with EC's current focus model), and [text] is + either a one-line conclusion digest (when [~all = false]) or the + full goal body (when [~all = true]). *) +let pp_tree ?(all = false) () : (int * bool * string) list = + let scope = current () in + match S.xgoal scope with + | Some { S.puc_active = Some ({ puc_jdg = S.PSCheck pf }, _) } -> begin + match EcCoreGoal.opened pf with + | None -> [] + | Some _ -> + let ppe = EcPrinting.PPEnv.ofenv (S.env scope) in + let goals = EcCoreGoal.all_opened pf in + List.mapi (fun i { EcCoreGoal.g_hyps; EcCoreGoal.g_concl } -> + let text = + if all then + let buf = Buffer.create 256 in + let hc = (EcEnv.LDecl.tohyps g_hyps, g_concl) in + Format.fprintf + (Format.formatter_of_buffer buf) + "%a@?" (EcPrinting.pp_goal1 ppe) hc; + Buffer.contents buf + else + Format.asprintf "%a" (EcPrinting.pp_form ppe) g_concl + in + (i + 1, i = 0, text)) goals + end + | _ -> [] diff --git a/src/ecCommands.mli b/src/ecCommands.mli index 88c119efb..1e744cb5f 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -65,6 +65,8 @@ val pp_current_goal_or_noproof : ?all:bool -> Format.formatter -> unit val pp_maybe_current_goal : Format.formatter -> unit val pp_all_goals : unit -> string list val in_proof : unit -> bool +val disable_repl_bullets : unit -> unit +val pp_tree : ?all:bool -> unit -> (int * bool * string) list (* -------------------------------------------------------------------- *) val pragma_verbose : bool -> unit diff --git a/src/ecScope.ml b/src/ecScope.ml index 19cddec23..f7509a3ac 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -489,6 +489,10 @@ let goal (scope : scope) = let xgoal (scope : scope) = scope.sc_pr_uc +(* -------------------------------------------------------------------- *) +let set_xgoal (scope : scope) (puc : proof_uc) = + { scope with sc_pr_uc = Some puc } + (* -------------------------------------------------------------------- *) let dump_why3 (scope : scope) (filename : string) = try EcSmt.dump_why3 (env scope) filename diff --git a/src/ecScope.mli b/src/ecScope.mli index d73ed66d7..5aeae3e3b 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -87,6 +87,7 @@ val env : scope -> EcEnv.env val attop : scope -> bool val goal : scope -> proof_auc option val xgoal : scope -> proof_uc option +val set_xgoal : scope -> proof_uc -> scope (* Creates a scope that is identical to the supplied one except * that the environment and required theories are reset to the ones From f94711eb59e09da7b2bd355a483cba2e9f0f8aaf Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 30 May 2026 07:11:13 +0200 Subject: [PATCH 04/10] [llm] add FOCUS N and NEXT for explicit goal selection 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. --- doc/llm/CLAUDE.md | 2 ++ src/ec.ml | 27 +++++++++++++++++++++++++++ src/ecCommands.ml | 34 ++++++++++++++++++++++++++++++++++ src/ecCommands.mli | 1 + src/ecCoreGoal.ml | 10 ++++++++++ src/ecCoreGoal.mli | 6 ++++++ 6 files changed, 80 insertions(+) diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index 1b7a3b066..28c8d049a 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -63,6 +63,8 @@ These are protocol-level commands, not EasyCrypt syntax: | `GOALS ALL` | Print all subgoals | | `TREE` | List open subgoals as `[N] `, marking the focused one | | `TREE ALL` | Same as `TREE`, but with full goal bodies | +| `FOCUS N` | Rotate focus so subgoal `[N]` (from `TREE`) becomes the focused goal | +| `NEXT` | Rotate focus to the next subgoal (equivalent to `FOCUS 2`) | | `CHECKPOINT ` | Save current uuid under a name for later `REVERT` | | `SEARCH ` | Search for lemmas matching a pattern | | `QUIET ON` / `QUIET OFF` | Suppress/enable automatic goal display after tactics | diff --git a/src/ec.ml b/src/ec.ml index 592157fe7..e49f8a208 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -982,6 +982,33 @@ let main () = Buffer.clear notices; reply_ok (tree_to_string ()) end + else if String.starts_with line "FOCUS " || line = "NEXT" then begin + Buffer.clear notices; + let request = + if line = "NEXT" then `Next + else + let arg = String.strip ( + String.sub line 6 (String.length line - 6)) in + try `At (int_of_string arg) + with Failure _ -> `Bad arg + in + match request with + | `Bad arg -> + reply_error (Printf.sprintf "FOCUS: not an integer: %s" arg) + | _ -> + let entries = EcCommands.pp_tree () in + let n = List.length entries in + let target = + match request with + | `Next -> if n <= 1 then 1 else 2 + | `At k -> k + | `Bad _ -> 1 + in + begin match EcCommands.focus_goal target with + | Ok _ -> reply_ok_goals () + | Error msg -> reply_error msg + end + end else if String.starts_with line "CHECKPOINT " then begin Buffer.clear notices; let name = String.strip ( diff --git a/src/ecCommands.ml b/src/ecCommands.ml index f1da34df3..3878499d4 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -988,6 +988,40 @@ let push_context scope context = |> omap (fun st -> context.ct_current :: st); } (* -------------------------------------------------------------------- *) +(* Rotate the focus of the currently active proof so that the goal at + 1-based index [k] becomes the focused one. The change is persisted + in the context with a new uuid so UNDO/REVERT can roll it back. + Returns the new number of open goals on success, or an error + message on failure. *) +let focus_goal (k : int) : (int, string) result = + match !context with + | None -> Error "no active context" + | Some ctxt -> + match EcScope.xgoal ctxt.ct_current with + | None -> Error "no active proof" + | Some puc -> + match puc.EcScope.puc_active with + | None -> Error "no active proof" + | Some (pac, pct) -> + match pac.EcScope.puc_jdg with + | EcScope.PSNoCheck -> Error "proof is in no-check mode" + | EcScope.PSCheck pf -> + let n = List.length (EcCoreGoal.all_hd_opened pf) in + if n = 0 then Error "no open goals" + else if k < 1 || k > n then + Error (Printf.sprintf + "focus: index %d out of range (1..%d)" k n) + else if k = 1 then Ok n + else begin + let pf = EcCoreGoal.rotate_focus k pf in + let pac = { pac with EcScope.puc_jdg = EcScope.PSCheck pf } in + let puc = + { puc with EcScope.puc_active = Some (pac, pct) } in + let scope = EcScope.set_xgoal ctxt.ct_current puc in + context := Some (push_context scope ctxt); + Ok n + end + (* Disable bullet enforcement for REPL-driven phrases. Drops the global pragma so newly-opened proofs have no bullet stack, and clears the stack on any currently active proof so REPL phrases are not checked diff --git a/src/ecCommands.mli b/src/ecCommands.mli index 1e744cb5f..5248ef8b9 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -67,6 +67,7 @@ val pp_all_goals : unit -> string list val in_proof : unit -> bool val disable_repl_bullets : unit -> unit val pp_tree : ?all:bool -> unit -> (int * bool * string) list +val focus_goal : int -> (int, string) result (* -------------------------------------------------------------------- *) val pragma_verbose : bool -> unit diff --git a/src/ecCoreGoal.ml b/src/ecCoreGoal.ml index 19291f3f7..306269681 100644 --- a/src/ecCoreGoal.ml +++ b/src/ecCoreGoal.ml @@ -1016,6 +1016,16 @@ let all_opened (pf : proof) = (* -------------------------------------------------------------------- *) let closed (pf : proof) = List.is_empty pf.pr_opened +(* -------------------------------------------------------------------- *) +let rotate_focus (k : int) (pf : proof) = + let n = List.length pf.pr_opened in + if k < 1 || k > n then + invalid_arg "EcCoreGoal.rotate_focus"; + if k = 1 then pf + else + let pre, post = List.split_at (k - 1) pf.pr_opened in + { pf with pr_opened = post @ pre } + (* -------------------------------------------------------------------- *) module Exn = struct let recast pe _hyps f x = diff --git a/src/ecCoreGoal.mli b/src/ecCoreGoal.mli index d045b8f93..3bb100d2f 100644 --- a/src/ecCoreGoal.mli +++ b/src/ecCoreGoal.mli @@ -206,6 +206,12 @@ val all_opened : proof -> pregoal list (* Check if a proof is done *) val closed : proof -> bool +(* Rotate the list of opened goals at the top level. [rotate_focus k pf] + makes the goal currently at 1-based index [k] the new focused goal, + preserving the cyclic order of the others. Raises [Invalid_argument] + if [k] is out of range. *) +val rotate_focus : int -> proof -> proof + (* -------------------------------------------------------------------- *) val tc_error : proofenv -> ?catchable:bool -> ?loc:EcLocation.t -> ?who:string From 9bef372288fefac1532f595acc75d790bce02bb4 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 30 May 2026 07:39:17 +0200 Subject: [PATCH 05/10] [llm] add COMMIT to emit a +strict_bullets-friendly proof body 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`. --- doc/llm/CLAUDE.md | 1 + src/ec.ml | 206 +++++++++++++++++++++++++++++++++++++++++++-- src/ecCommands.ml | 55 +++++++++--- src/ecCommands.mli | 5 +- src/ecCoreGoal.ml | 47 +++++++++-- src/ecCoreGoal.mli | 6 ++ 6 files changed, 295 insertions(+), 25 deletions(-) diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index 28c8d049a..a06725467 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -65,6 +65,7 @@ These are protocol-level commands, not EasyCrypt syntax: | `TREE ALL` | Same as `TREE`, but with full goal bodies | | `FOCUS N` | Rotate focus so subgoal `[N]` (from `TREE`) becomes the focused goal | | `NEXT` | Rotate focus to the next subgoal (equivalent to `FOCUS 2`) | +| `COMMIT` | Emit recorded REPL phrases as a bulleted proof body (works under `+strict_bullets`) | | `CHECKPOINT ` | Save current uuid under a name for later `REVERT` | | `SEARCH ` | Search for lemmas matching a pattern | | `QUIET ON` / `QUIET OFF` | Suppress/enable automatic goal display after tactics | diff --git a/src/ec.ml b/src/ec.ml index e49f8a208..b4d3dc0c6 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -549,6 +549,170 @@ let main () = let checkpoints : (string, int) Hashtbl.t = Hashtbl.create 16 in + (* Transcript of REPL-typed phrases that succeeded. Each entry is + (uuid_before, src, parent, opens_at_entry), where: + - [parent] is the handle that was focused right before the + phrase ran ([None] iff outside a proof); + - [opens_at_entry] is the full open-handle list at entry time + (focused-first), used by COMMIT to seed the sibling map for + continuations whose first phrase already starts inside a + frame opened by the LOAD prefix. + Trimmed by UNDO/REVERT; cleared on LOAD/Restart. *) + let transcript : + (int * string * EcCoreGoal.handle option + * EcCoreGoal.handle list) list ref = ref [] in + + (* The bullet stack of the active proof at the moment REPL input + took over. Captured the first time [disable_repl_bullets] + actually clears a non-empty stack; subsequent (idempotent) + calls return [None] and leave this snapshot unchanged. Used by + [COMMIT] to pick bullet characters that don't collide with + tokens already in scope from the LOAD prefix. Cleared on + LOAD/Restart along with the transcript. *) + let prior_bullets : EcBullets.stack option ref = ref None in + + let transcript_trim target = + transcript := + List.filter + (fun (uuid_before, _, _, _) -> uuid_before < target) + !transcript + in + + (* Render the recorded transcript as a +strict_bullets-friendly + proof body. The algorithm reads the proof DAG via + [EcCommands.children_of]/[parent_of] (backed by [pr_parent], + which records the parent handle of every child at + [FApi.newgoal] time). Strategy: + - For each phrase, walk the subtree rooted at its parent + handle, finding every multi-child split, and register each + such child in [sibling_depth] at the corresponding depth. + Single-child links are continuations and don't 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, skipping any token + already in the LOAD prefix's [puc_bullets] stack (snapshotted + at the moment REPL input took over) so we never collide. *) + (* Token order matches PR 1017's lexer: -, +, *, --, ++, **, + ---, +++, *** ... *) + let token_at_index i = + let chars = [| "-"; "+"; "*" |] in + let rep = i / 3 + 1 in + let chr = chars.(i mod 3) in + String.concat "" (List.init rep (fun _ -> chr)) + in + + let commit_proof_text () = + let entries = List.rev !transcript in + let buf = Buffer.create 1024 in + let emit_indent depth = + for _ = 1 to depth do Buffer.add_string buf " " done + in + let module Hmap = + Map.Make (struct + type t = EcCoreGoal.handle + let compare = compare + end) + in + let sibling_depth : int Hmap.t ref = ref Hmap.empty in + let current_depth = ref 0 in + (* Pick a bullet token for each depth, skipping tokens already + in scope from the LOAD prefix's bullet stack (so we never + collide with frames the prefix opened). State is per-COMMIT + so each invocation starts from a clean slate. *) + let in_use_tokens = + match !prior_bullets with + | None -> [] + | Some stack -> + List.map (fun (f : EcBullets.frame) -> f.bf_token) stack + in + let depth_cache : (int, string) Hashtbl.t = Hashtbl.create 8 in + let next_tok_idx = ref 0 in + let assigned_tokens = ref [] in + let bullet_for_depth d = + match Hashtbl.find_opt depth_cache d with + | Some t -> t + | None -> + let rec pick () = + let t = token_at_index !next_tok_idx in + incr next_tok_idx; + if List.mem t in_use_tokens || List.mem t !assigned_tokens + then pick () + else t + in + let t = pick () in + assigned_tokens := t :: !assigned_tokens; + Hashtbl.add depth_cache d t; + t + in + (* Seed: if the first recorded phrase entered a state with + multiple open goals, the LOAD prefix opened a frame whose + siblings are still pending. Register all of them as depth-1 + pending siblings so the first phrase's parent gets a bullet. *) + (match entries with + | (_, _, Some _, (_ :: _ :: _ as opens)) :: _ -> + List.iter + (fun h -> sibling_depth := Hmap.add h 1 !sibling_depth) + opens + | _ -> ()); + List.iter (fun (_uuid, src, parent_opt, _opens) -> + match parent_opt with + | None -> + Buffer.add_string buf src; + Buffer.add_char buf '\n' + | Some parent -> + (* Walk upward through pr_parent until we find a registered + sibling ancestor, or run out. If found, emit a bullet at + that depth and consume the registration. *) + let rec find_ancestor h = + match Hmap.find_opt h !sibling_depth with + | Some d -> Some (h, d) + | None -> + match EcCommands.parent_of h with + | Some p -> find_ancestor p + | None -> None + in + (match find_ancestor parent with + | Some (h, d) -> + emit_indent (d - 1); + Buffer.add_string buf (bullet_for_depth d); + Buffer.add_char buf ' '; + current_depth := d; + sibling_depth := Hmap.remove h !sibling_depth + | None -> + emit_indent !current_depth); + Buffer.add_string buf src; + Buffer.add_char buf '\n'; + (* A phrase can chain multiple sub-validations internally + (e.g. [move=> hp hq; split.] is VIntros -> VApply(split) + on a single recorded phrase). Walk single-child + validations until we hit a real split (>=2 children) or + an open leaf. *) + (* Walk the entire subtree rooted at [parent], finding every + multi-child node, and register its children at the + corresponding nesting depth. A compound phrase like + [split; split.] can produce nested splits within a single + phrase; both levels of children need to be registered. + Single-child links don't bump the depth (continuations); + multi-child links do. *) + let rec walk h d = + match EcCommands.children_of h with + | [c] -> walk c d + | (_ :: _ :: _) as cs -> + List.iter + (fun c -> + sibling_depth := + Hmap.add c d !sibling_depth; + walk c (d + 1)) + cs + | [] -> () + in + walk parent (!current_depth + 1) + ) entries; + Buffer.contents buf + in + let reply_ok ?(tag="") body = let n = Buffer.contents notices in Printf.printf "OK [uuid:%d]%s\n" (EcCommands.uuid ()) tag; @@ -589,9 +753,20 @@ let main () = Buffer.clear notices in - (* Process a single EasyCrypt command, respecting gl_fail *) - let process_action ~src (p : EP.global) = + (* Process a single EasyCrypt command, respecting gl_fail. When + [~record:true], capture the parent handle (the focused goal + before the phrase ran) and append a transcript entry on + success. COMMIT will use [EcCommands.children_of] on each + parent to walk the proof DAG and recover bullet structure. *) + let process_action ?(record=false) ~src (p : EP.global) = let loc = p.EP.gl_action.EcLocation.pl_loc in + let pre_uuid = EcCommands.uuid () in + let opens_pre = + if record then EcCommands.open_handles () else [] + in + let parent = + match opens_pre with h :: _ -> Some h | [] -> None + in let succeeded = ref false in begin try ignore (EcCommands.process ~src p.EP.gl_action : float option); @@ -604,13 +779,21 @@ let main () = if !succeeded && p.EP.gl_fail then raise (EcScope.toperror_of_exn ~gloc:loc (EcScope.HiScopeError (None, - "this command is expected to fail"))) + "this command is expected to fail"))); + if record && !succeeded && not p.EP.gl_fail then + transcript := (pre_uuid, src, parent, opens_pre) :: !transcript in (* Process EasyCrypt input from a string (one parsed program) *) let process_ec_input input = Buffer.clear notices; - EcCommands.disable_repl_bullets (); + (* On the first REPL phrase of each proof, capture the bullet + stack that the LOAD prefix left so COMMIT can avoid token + collisions with it. Subsequent calls return [None] and don't + clobber the snapshot. *) + (match EcCommands.disable_repl_bullets () with + | None -> () + | Some _ as snapshot -> prior_bullets := snapshot); let reader = EcIo.from_string input in let last_src = ref "" in begin try @@ -619,10 +802,11 @@ let main () = last_src := src; begin match EcLocation.unloc prog with | EP.P_Prog (commands, _) -> - List.iter (process_action ~src) commands; + List.iter (process_action ~record:true ~src) commands; reply_ok_goals () | EP.P_Undo i -> EcCommands.undo i; + transcript_trim i; reply_ok_goals () | EP.P_Exit -> EcIo.finalize reader; exit 0 @@ -633,6 +817,8 @@ let main () = with | EcCommands.Restart -> do_initialize (); + transcript := []; + prior_bullets := None; reply_ok "Session restarted" | e -> reply_error (format_error ~src:!last_src e) @@ -709,6 +895,8 @@ let main () = (* Reset proof engine and process file *) do_initialize (); Hashtbl.clear checkpoints; + transcript := []; + prior_bullets := None; EcCommands.addidir (Filename.dirname filename); let reader = EcIo.from_file filename in @@ -896,6 +1084,8 @@ let main () = | EcCommands.Restart -> do_initialize (); Hashtbl.clear checkpoints; + transcript := []; + prior_bullets := None; reply_ok "Session restarted" | Trace_failed e -> let msg = format_error ~src:!last_src e in @@ -962,6 +1152,7 @@ let main () = let uuid = EcCommands.uuid () in if uuid > 0 then begin EcCommands.undo (uuid - 1); + transcript_trim (uuid - 1); reply_ok_goals () end else reply_error "nothing to undo" @@ -982,6 +1173,10 @@ let main () = Buffer.clear notices; reply_ok (tree_to_string ()) end + else if line = "COMMIT" then begin + Buffer.clear notices; + reply_ok (commit_proof_text ()) + end else if String.starts_with line "FOCUS " || line = "NEXT" then begin Buffer.clear notices; let request = @@ -1040,6 +1235,7 @@ let main () = "REVERT: uuid %d out of range [0, %d]" target uuid) else begin EcCommands.undo target; + transcript_trim target; reply_ok_goals () end end diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 3878499d4..fb03df2ae 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -1025,23 +1025,30 @@ let focus_goal (k : int) : (int, string) result = (* Disable bullet enforcement for REPL-driven phrases. Drops the global pragma so newly-opened proofs have no bullet stack, and clears the stack on any currently active proof so REPL phrases are not checked - against it. Idempotent. Does not advance the undo level. *) -let disable_repl_bullets () = + against it. Idempotent. Does not advance the undo level. Returns + the stack that was in place (if any) at the moment the active + proof's bullets were first cleared; returns [None] on idempotent + calls (where the stack is already gone). Callers use the returned + stack to drive bullet-character selection in [COMMIT]. *) +let disable_repl_bullets () : EcBullets.stack option = pragma_strict_bullets false; match !context with - | None -> () + | None -> None | Some ctxt -> match EcScope.xgoal ctxt.ct_current with - | None -> () + | None -> None | Some puc -> match puc.EcScope.puc_active with - | None -> () - | Some (pac, _) when pac.EcScope.puc_bullets = None -> () + | None -> None | Some (pac, pct) -> - let pac = { pac with EcScope.puc_bullets = None } in - let puc = { puc with EcScope.puc_active = Some (pac, pct) } in - let scope = EcScope.set_xgoal ctxt.ct_current puc in - context := Some { ctxt with ct_current = scope } + match pac.EcScope.puc_bullets with + | None -> None + | Some _ as prior -> + let pac = { pac with EcScope.puc_bullets = None } in + let puc = { puc with EcScope.puc_active = Some (pac, pct) } in + let scope = EcScope.set_xgoal ctxt.ct_current puc in + context := Some { ctxt with ct_current = scope }; + prior (* -------------------------------------------------------------------- *) let initialize ~restart ~undo ~boot ~checkmode ~checkproof = @@ -1186,6 +1193,34 @@ let pp_current_goal ?(all = false) stream = let in_proof () = Option.is_some (S.xgoal (current ())) +(* Return the list of open-goal handles at the top level of the active + proof, focused-first, or [] if no proof is active. *) +let open_handles () : EcCoreGoal.handle list = + match S.xgoal (current ()) with + | Some { S.puc_active = + Some ({ S.puc_jdg = S.PSCheck pf }, _) } -> + EcCoreGoal.all_hd_opened pf + | _ -> [] + +(* Direct DAG children of [h] in the active proof. [] if no proof. *) +let children_of (h : EcCoreGoal.handle) : EcCoreGoal.handle list = + match S.xgoal (current ()) with + | Some { S.puc_active = + Some ({ S.puc_jdg = S.PSCheck pf }, _) } -> + EcCoreGoal.children_of_handle + (EcCoreGoal.proofenv_of_proof pf) h + | _ -> [] + +(* Parent of [h] in the active proof's DAG, or [None] if [h] is the + root or no proof is active. *) +let parent_of (h : EcCoreGoal.handle) : EcCoreGoal.handle option = + match S.xgoal (current ()) with + | Some { S.puc_active = + Some ({ S.puc_jdg = S.PSCheck pf }, _) } -> + EcCoreGoal.parent_of_handle + (EcCoreGoal.proofenv_of_proof pf) h + | _ -> None + let pp_current_goal_or_noproof ?(all = false) stream = if in_proof () then pp_current_goal ~all stream diff --git a/src/ecCommands.mli b/src/ecCommands.mli index 5248ef8b9..320aed1d6 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -65,9 +65,12 @@ val pp_current_goal_or_noproof : ?all:bool -> Format.formatter -> unit val pp_maybe_current_goal : Format.formatter -> unit val pp_all_goals : unit -> string list val in_proof : unit -> bool -val disable_repl_bullets : unit -> unit +val disable_repl_bullets : unit -> EcBullets.stack option val pp_tree : ?all:bool -> unit -> (int * bool * string) list val focus_goal : int -> (int, string) result +val open_handles : unit -> EcCoreGoal.handle list +val children_of : EcCoreGoal.handle -> EcCoreGoal.handle list +val parent_of : EcCoreGoal.handle -> EcCoreGoal.handle option (* -------------------------------------------------------------------- *) val pragma_verbose : bool -> unit diff --git a/src/ecCoreGoal.ml b/src/ecCoreGoal.ml index 306269681..b0b09aebf 100644 --- a/src/ecCoreGoal.ml +++ b/src/ecCoreGoal.ml @@ -132,9 +132,13 @@ type proof = { } and proofenv = { - pr_uid : ID.id; (* unique ID for this proof *) - pr_main : ID.id; (* top goal, contains the final result *) - pr_goals : goal ID.Map.t; (* set of all goals, closed and opened *) + pr_uid : ID.id; (* unique ID for this proof *) + pr_main : ID.id; (* top goal, contains the final result *) + pr_goals : goal ID.Map.t; (* set of all goals, closed and opened *) + pr_parent : handle ID.Map.t; + (* For each non-root handle, the parent in the proof DAG: i.e. + the handle that was being worked on when this one was created + via [FApi.newgoal]. The root [pr_main] is absent. *) } and pregoal = { @@ -459,17 +463,24 @@ module FApi = struct tcenv (* ------------------------------------------------------------------ *) - let pf_newgoal (pe : proofenv) ?vx hyps concl = + let pf_newgoal (pe : proofenv) ?parent ?vx hyps concl = let hid = ID.gen () in let pregoal = { g_uid = hid; g_hyps = hyps; g_concl = concl; } in let goal = { g_goal = pregoal; g_validation = vx; } in - let pe = { pe with pr_goals = ID.Map.add pregoal.g_uid goal pe.pr_goals; } in + let pr_goals = ID.Map.add pregoal.g_uid goal pe.pr_goals in + let pr_parent = + match parent with + | None -> pe.pr_parent + | Some p -> ID.Map.add pregoal.g_uid p pe.pr_parent + in + let pe = { pe with pr_goals; pr_parent } in (pe, pregoal) (* ------------------------------------------------------------------ *) let newgoal (tc : tcenv) ?(hyps : LDecl.hyps option) (concl : form) = let hyps = ofdfl (fun () -> tc_hyps tc) hyps in - let (pe, pg) = pf_newgoal (tc_penv tc) hyps concl in + let parent = tc.tce_tcenv.tce_goal |> Option.map (fun g -> g.g_uid) in + let (pe, pg) = pf_newgoal (tc_penv tc) ?parent hyps concl in let tc = tc_update_tcenv (fun te -> { te with tce_penv = pe }) tc in let tc = { tc with tce_goals = tc.tce_goals @ [pg.g_uid] } in @@ -992,9 +1003,10 @@ let start (hyps : LDecl.hyps) (goal : form) = let goal = { g_uid = hid; g_hyps = hyps; g_concl = goal; } in let goal = { g_goal = goal; g_validation = None; } in - let env = { pr_uid = uid; - pr_main = hid; - pr_goals = ID.Map.singleton hid goal; } in + let env = { pr_uid = uid; + pr_main = hid; + pr_goals = ID.Map.singleton hid goal; + pr_parent = ID.Map.empty; } in { pr_env = env; pr_opened = [hid]; } @@ -1016,6 +1028,23 @@ let all_opened (pf : proof) = (* -------------------------------------------------------------------- *) let closed (pf : proof) = List.is_empty pf.pr_opened +(* -------------------------------------------------------------------- *) +(* Direct children of [h] in the proof DAG, in creation order. This is + driven by [pr_parent], the explicit parent edge recorded by + [FApi.newgoal] at the moment each child handle is allocated. The + iteration order matches creation order because handles are + generated by a monotonic counter and [ID.Map] iterates by key. *) +let children_of_handle (pe : proofenv) (h : handle) : handle list = + ID.Map.fold + (fun child parent acc -> + if eq_handle parent h then child :: acc else acc) + pe.pr_parent [] + |> List.rev + +(* Parent of [h] in the proof DAG, or [None] if [h] is the root. *) +let parent_of_handle (pe : proofenv) (h : handle) : handle option = + ID.Map.find_opt h pe.pr_parent + (* -------------------------------------------------------------------- *) let rotate_focus (k : int) (pf : proof) = let n = List.length pf.pr_opened in diff --git a/src/ecCoreGoal.mli b/src/ecCoreGoal.mli index 3bb100d2f..c82fcac11 100644 --- a/src/ecCoreGoal.mli +++ b/src/ecCoreGoal.mli @@ -206,6 +206,12 @@ val all_opened : proof -> pregoal list (* Check if a proof is done *) val closed : proof -> bool +(* Direct children of [h] in the proof DAG, in creation order. *) +val children_of_handle : proofenv -> handle -> handle list + +(* Parent of [h] in the proof DAG, or [None] if [h] is the root. *) +val parent_of_handle : proofenv -> handle -> handle option + (* Rotate the list of opened goals at the top level. [rotate_focus k pf] makes the goal currently at 1-based index [k] the new focused goal, preserving the cyclic order of the others. Raises [Invalid_argument] From 3ac6aa8b5063c42004867d9fb983746cfcf13612 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 30 May 2026 10:54:50 +0200 Subject: [PATCH 06/10] [llm] extract REPL into a dedicated EcLlm module 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/ 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. --- src/ec.ml | 870 +------------------------------------------------ src/ecLlm.ml | 873 ++++++++++++++++++++++++++++++++++++++++++++++++++ src/ecLlm.mli | 11 + 3 files changed, 885 insertions(+), 869 deletions(-) create mode 100644 src/ecLlm.ml create mode 100644 src/ecLlm.mli diff --git a/src/ec.ml b/src/ec.ml index b4d3dc0c6..07913c4a4 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -404,874 +404,6 @@ let main () = (* Register user messages printers *) begin let open EcUserMessages in register () end; - (* -------------------------------------------------------------------- *) - (* LLM interactive mode *) - (* -------------------------------------------------------------------- *) - - let llm_guide_path () = - let (module Sites) = EcRelocate.sites in - match EcRelocate.sourceroot with - | Some root -> - Filename.concat (Filename.concat root "doc/llm") "CLAUDE.md" - | None -> - Filename.concat Sites.doc "llm-guide.md" - in - - let print_llm_guide () = - let path = llm_guide_path () in - try - let ic = open_in path in - begin try while true do - print_char (input_char ic) - done with End_of_file -> () end; - close_in ic - with Sys_error e -> - Printf.eprintf "cannot read LLM guide: %s\n%!" e - in - - let run_llm_repl (llmopts : llm_option) = - if llmopts.llmo_help then begin - print_llm_guide (); - exit 0 - end; - - let prvopts = llmopts.llmo_provers in - (* Initialize PRNG *) - Random.self_init (); - - (* Connect to external Why3 server if requested *) - prvopts.prvo_why3server |> oiter (fun server -> - try - Why3.Prove_client.connect_external server - with Why3.Prove_client.ConnectionError e -> - Format.eprintf - "cannot connect to Why3 server `%s': %s" server e; - exit 1); - - (* Add current directory to load path *) - (match relocdir with - | None -> EcCommands.addidir Filename.current_dir_name - | Some pwd -> EcCommands.addidir pwd); - - (* Proof engine configuration *) - let checkmode = { - EcCommands.cm_checkall = prvopts.prvo_checkall; - EcCommands.cm_timeout = odfl 3 prvopts.prvo_timeout; - EcCommands.cm_cpufactor = odfl 1 prvopts.prvo_cpufactor; - EcCommands.cm_nprovers = odfl 4 prvopts.prvo_maxjobs; - EcCommands.cm_provers = prvopts.prvo_provers; - EcCommands.cm_quorum = prvopts.prvo_quorum; - EcCommands.cm_profile = prvopts.prvo_profile; - } in - - (* Notice buffer: collects messages during command processing *) - let notices = Buffer.create 256 in - - let notifier (_ : EcGState.loglevel) (lazy msg) = - Buffer.add_string notices msg; - Buffer.add_char notices '\n' - in - - let initialized = ref false in - - let do_initialize () = - EcCommands.initialize - ~restart:!initialized ~undo:true - ~boot:ldropts.ldro_boot ~checkmode ~checkproof:true; - initialized := true; - (try - List.iter EcCommands.apply_pragma prvopts.prvo_pragmas - with EcCommands.InvalidPragma x -> - EcScope.hierror "invalid pragma: `%s'\n%!" x); - EcCommands.addnotifier notifier; - oiter (fun ppwidth -> - let gs = EcEnv.gstate (EcScope.env (EcCommands.current ())) in - EcGState.setvalue "PP:width" (`Int ppwidth) gs) - prvopts.prvo_ppwidth - in - - (* Error formatting *) - let format_error ?(src="") e = - let base = match e with - | EcScope.TopError (loc, e) -> - let msg = String.strip (EcPException.tostring e) in - if loc = EcLocation._dummy then msg - else Format.asprintf "%s: %s" (EcLocation.tostring loc) msg - | e -> - String.strip (EcPException.tostring e) - in - if src = "" then base - else Printf.sprintf "%s\nsource: %s" base src - in - - (* Output helpers *) - let goals_to_string ?(all=false) () = - let buf = Buffer.create 256 in - let fmt = Format.formatter_of_buffer buf in - EcCommands.pp_current_goal_or_noproof ~all fmt; - Format.pp_print_flush fmt (); - Buffer.contents buf - in - - (* Render the focus-tree of open subgoals. [all=false] gives a - one-line digest per goal (conclusion truncated); [all=true] - gives the full goal body for each. *) - let tree_to_string ?(all=false) () = - let entries = EcCommands.pp_tree ~all () in - match entries with - | [] -> "No active proof.\n" - | _ -> - let buf = Buffer.create 256 in - let one_line s = - let s = - match String.index_opt s '\n' with - | None -> s - | Some k -> String.sub s 0 k - in - let limit = 80 in - if String.length s > limit - then String.sub s 0 (limit - 1) ^ "…" - else s - in - List.iter (fun (i, focused, text) -> - let marker = if focused then " <- focused" else "" in - if all then - Buffer.add_string buf - (Printf.sprintf "[%d]%s\n%s\n" i marker text) - else - Buffer.add_string buf - (Printf.sprintf "[%d] %s%s\n" i (one_line text) marker) - ) entries; - Buffer.contents buf - in - - let quiet = ref false in - - let checkpoints : (string, int) Hashtbl.t = Hashtbl.create 16 in - - (* Transcript of REPL-typed phrases that succeeded. Each entry is - (uuid_before, src, parent, opens_at_entry), where: - - [parent] is the handle that was focused right before the - phrase ran ([None] iff outside a proof); - - [opens_at_entry] is the full open-handle list at entry time - (focused-first), used by COMMIT to seed the sibling map for - continuations whose first phrase already starts inside a - frame opened by the LOAD prefix. - Trimmed by UNDO/REVERT; cleared on LOAD/Restart. *) - let transcript : - (int * string * EcCoreGoal.handle option - * EcCoreGoal.handle list) list ref = ref [] in - - (* The bullet stack of the active proof at the moment REPL input - took over. Captured the first time [disable_repl_bullets] - actually clears a non-empty stack; subsequent (idempotent) - calls return [None] and leave this snapshot unchanged. Used by - [COMMIT] to pick bullet characters that don't collide with - tokens already in scope from the LOAD prefix. Cleared on - LOAD/Restart along with the transcript. *) - let prior_bullets : EcBullets.stack option ref = ref None in - - let transcript_trim target = - transcript := - List.filter - (fun (uuid_before, _, _, _) -> uuid_before < target) - !transcript - in - - (* Render the recorded transcript as a +strict_bullets-friendly - proof body. The algorithm reads the proof DAG via - [EcCommands.children_of]/[parent_of] (backed by [pr_parent], - which records the parent handle of every child at - [FApi.newgoal] time). Strategy: - - For each phrase, walk the subtree rooted at its parent - handle, finding every multi-child split, and register each - such child in [sibling_depth] at the corresponding depth. - Single-child links are continuations and don't 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, skipping any token - already in the LOAD prefix's [puc_bullets] stack (snapshotted - at the moment REPL input took over) so we never collide. *) - (* Token order matches PR 1017's lexer: -, +, *, --, ++, **, - ---, +++, *** ... *) - let token_at_index i = - let chars = [| "-"; "+"; "*" |] in - let rep = i / 3 + 1 in - let chr = chars.(i mod 3) in - String.concat "" (List.init rep (fun _ -> chr)) - in - - let commit_proof_text () = - let entries = List.rev !transcript in - let buf = Buffer.create 1024 in - let emit_indent depth = - for _ = 1 to depth do Buffer.add_string buf " " done - in - let module Hmap = - Map.Make (struct - type t = EcCoreGoal.handle - let compare = compare - end) - in - let sibling_depth : int Hmap.t ref = ref Hmap.empty in - let current_depth = ref 0 in - (* Pick a bullet token for each depth, skipping tokens already - in scope from the LOAD prefix's bullet stack (so we never - collide with frames the prefix opened). State is per-COMMIT - so each invocation starts from a clean slate. *) - let in_use_tokens = - match !prior_bullets with - | None -> [] - | Some stack -> - List.map (fun (f : EcBullets.frame) -> f.bf_token) stack - in - let depth_cache : (int, string) Hashtbl.t = Hashtbl.create 8 in - let next_tok_idx = ref 0 in - let assigned_tokens = ref [] in - let bullet_for_depth d = - match Hashtbl.find_opt depth_cache d with - | Some t -> t - | None -> - let rec pick () = - let t = token_at_index !next_tok_idx in - incr next_tok_idx; - if List.mem t in_use_tokens || List.mem t !assigned_tokens - then pick () - else t - in - let t = pick () in - assigned_tokens := t :: !assigned_tokens; - Hashtbl.add depth_cache d t; - t - in - (* Seed: if the first recorded phrase entered a state with - multiple open goals, the LOAD prefix opened a frame whose - siblings are still pending. Register all of them as depth-1 - pending siblings so the first phrase's parent gets a bullet. *) - (match entries with - | (_, _, Some _, (_ :: _ :: _ as opens)) :: _ -> - List.iter - (fun h -> sibling_depth := Hmap.add h 1 !sibling_depth) - opens - | _ -> ()); - List.iter (fun (_uuid, src, parent_opt, _opens) -> - match parent_opt with - | None -> - Buffer.add_string buf src; - Buffer.add_char buf '\n' - | Some parent -> - (* Walk upward through pr_parent until we find a registered - sibling ancestor, or run out. If found, emit a bullet at - that depth and consume the registration. *) - let rec find_ancestor h = - match Hmap.find_opt h !sibling_depth with - | Some d -> Some (h, d) - | None -> - match EcCommands.parent_of h with - | Some p -> find_ancestor p - | None -> None - in - (match find_ancestor parent with - | Some (h, d) -> - emit_indent (d - 1); - Buffer.add_string buf (bullet_for_depth d); - Buffer.add_char buf ' '; - current_depth := d; - sibling_depth := Hmap.remove h !sibling_depth - | None -> - emit_indent !current_depth); - Buffer.add_string buf src; - Buffer.add_char buf '\n'; - (* A phrase can chain multiple sub-validations internally - (e.g. [move=> hp hq; split.] is VIntros -> VApply(split) - on a single recorded phrase). Walk single-child - validations until we hit a real split (>=2 children) or - an open leaf. *) - (* Walk the entire subtree rooted at [parent], finding every - multi-child node, and register its children at the - corresponding nesting depth. A compound phrase like - [split; split.] can produce nested splits within a single - phrase; both levels of children need to be registered. - Single-child links don't bump the depth (continuations); - multi-child links do. *) - let rec walk h d = - match EcCommands.children_of h with - | [c] -> walk c d - | (_ :: _ :: _) as cs -> - List.iter - (fun c -> - sibling_depth := - Hmap.add c d !sibling_depth; - walk c (d + 1)) - cs - | [] -> () - in - walk parent (!current_depth + 1) - ) entries; - Buffer.contents buf - in - - let reply_ok ?(tag="") body = - let n = Buffer.contents notices in - Printf.printf "OK [uuid:%d]%s\n" (EcCommands.uuid ()) tag; - if n <> "" then print_string n; - if body <> "" then begin - print_string body; - let len = String.length body in - if len > 0 && body.[len - 1] <> '\n' then - print_char '\n' - end; - Printf.printf "\n%!"; - Buffer.clear notices - in - - let focus_tag () = - match EcCommands.pp_tree () with - | _ :: _ :: _ as entries -> - Printf.sprintf " [focus: 1/%d]" (List.length entries) - | _ -> "" - in - - let reply_ok_goals ?(all=false) () = - let tag = focus_tag () in - if !quiet then reply_ok ~tag "" - else reply_ok ~tag (goals_to_string ~all ()) - in - - let reply_error msg = - let goals = goals_to_string () in - Printf.printf "ERROR [uuid:%d]\n%s\n" (EcCommands.uuid ()) msg; - if goals <> "" then begin - print_string goals; - let len = String.length goals in - if len > 0 && goals.[len - 1] <> '\n' then - print_char '\n' - end; - Printf.printf "\n%!"; - Buffer.clear notices - in - - (* Process a single EasyCrypt command, respecting gl_fail. When - [~record:true], capture the parent handle (the focused goal - before the phrase ran) and append a transcript entry on - success. COMMIT will use [EcCommands.children_of] on each - parent to walk the proof DAG and recover bullet structure. *) - let process_action ?(record=false) ~src (p : EP.global) = - let loc = p.EP.gl_action.EcLocation.pl_loc in - let pre_uuid = EcCommands.uuid () in - let opens_pre = - if record then EcCommands.open_handles () else [] - in - let parent = - match opens_pre with h :: _ -> Some h | [] -> None - in - let succeeded = ref false in - begin try - ignore (EcCommands.process ~src p.EP.gl_action : float option); - succeeded := true - with - | EcCommands.Restart -> raise EcCommands.Restart - | _ when p.EP.gl_fail -> () - | e -> raise (EcScope.toperror_of_exn ~gloc:loc e) - end; - if !succeeded && p.EP.gl_fail then - raise (EcScope.toperror_of_exn ~gloc:loc - (EcScope.HiScopeError (None, - "this command is expected to fail"))); - if record && !succeeded && not p.EP.gl_fail then - transcript := (pre_uuid, src, parent, opens_pre) :: !transcript - in - - (* Process EasyCrypt input from a string (one parsed program) *) - let process_ec_input input = - Buffer.clear notices; - (* On the first REPL phrase of each proof, capture the bullet - stack that the LOAD prefix left so COMMIT can avoid token - collisions with it. Subsequent calls return [None] and don't - clobber the snapshot. *) - (match EcCommands.disable_repl_bullets () with - | None -> () - | Some _ as snapshot -> prior_bullets := snapshot); - let reader = EcIo.from_string input in - let last_src = ref "" in - begin try - let (src, prog) = EcIo.xparse reader in - let src = String.strip src in - last_src := src; - begin match EcLocation.unloc prog with - | EP.P_Prog (commands, _) -> - List.iter (process_action ~record:true ~src) commands; - reply_ok_goals () - | EP.P_Undo i -> - EcCommands.undo i; - transcript_trim i; - reply_ok_goals () - | EP.P_Exit -> - EcIo.finalize reader; exit 0 - | EP.P_DocComment doc -> - EcCommands.doc_comment doc; - reply_ok "" - end - with - | EcCommands.Restart -> - do_initialize (); - transcript := []; - prior_bullets := None; - reply_ok "Session restarted" - | e -> - reply_error (format_error ~src:!last_src e) - end; - EcIo.finalize reader - in - - (* Handle LOAD "file.ec" [LINE[:COL]] *) - let handle_load args = - Buffer.clear notices; - let args = String.strip args in - let last_src = ref "" in - let trace_prefix = ref "" in - let exception Trace_failed of exn in - - try - (* Parse quoted or unquoted filename *) - let filename, rest = - if String.length args > 0 && args.[0] = '"' then - let close = - try String.index_from args 1 '"' - with Not_found -> - failwith "LOAD: unterminated filename" - in - let fn = String.sub args 1 (close - 1) in - let rest = String.strip ( - String.sub args (close + 1) - (String.length args - close - 1)) in - (fn, rest) - else - match String.split_on_char ' ' args with - | [] -> failwith "LOAD: missing filename" - | [f] -> (f, "") - | f :: rest -> (f, String.concat " " rest) - in - - (* Parse optional LINE[:COL] and flags (-nosmt, -trace) *) - let upto, nosmt, trace = - let words = - String.split_on_char ' ' rest - |> List.filter (fun s -> s <> "") - in - let nosmt = List.mem "-nosmt" words in - let trace = List.mem "-trace" words in - let words = - List.filter - (fun s -> s <> "-nosmt" && s <> "-trace") - words - in - let upto = match words with - | [] -> None - | [w] -> - begin match String.split_on_char ':' w with - | [line] -> - Some (int_of_string line, None) - | [line; col] -> - Some (int_of_string line, Some (int_of_string col)) - | _ -> failwith "LOAD: invalid LINE[:COL] format" - end - | _ -> failwith "LOAD: unexpected arguments" - in - (upto, nosmt, trace) - in - - (* Validate file extension *) - begin try - ignore (EcLoader.getkind - (Filename.extension filename) : EcLoader.kind) - with EcLoader.BadExtension ext -> - failwith (Format.sprintf - "unknown file extension: %s" ext) - end; - - (* Reset proof engine and process file *) - do_initialize (); - Hashtbl.clear checkpoints; - transcript := []; - prior_bullets := None; - EcCommands.addidir (Filename.dirname filename); - - let reader = EcIo.from_file filename in - - let past_upto (loc : EcLocation.t) = - match upto with - | None -> false - | Some (line, col) -> - let (el, ec) = loc.loc_end in - el > line || (el = line && match col with - | None -> false - | Some c -> ec > c) - in - - let last_loc = ref None in - - (* For -trace: lazy whole-file bytes, used to slice the exact - source text of a sentence by byte offsets. *) - let input_bytes = lazy ( - let ic = open_in_bin filename in - let n = in_channel_length ic in - let b = Bytes.create n in - really_input ic b 0 n; - close_in ic; - Bytes.unsafe_to_string b) - in - let sentence_source (loc : EcLocation.t) = - let s = Lazy.force input_bytes in - let lo = max 0 loc.EcLocation.loc_bchar in - let hi = min (String.length s) loc.EcLocation.loc_echar in - if hi <= lo then "" else String.sub s lo (hi - lo) - in - - (* For -trace: defer execution of the last sentence within the - prefix so we can capture goals before and after it. *) - let pending : (string * EP.global) option ref = ref None in - let flush_pending () = - match !pending with - | None -> () - | Some (src, p) -> - last_src := src; - process_action ~src p; - last_loc := Some p.EP.gl_action.EcLocation.pl_loc; - pending := None - in - let step src p = - let loc = p.EP.gl_action.EcLocation.pl_loc in - if past_upto loc then raise Exit; - if trace then begin - flush_pending (); - pending := Some (src, p) - end else begin - last_src := src; - process_action ~src p; - last_loc := Some loc - end - in - - (* In -nosmt mode, admit all SMT calls during prefix loading *) - if nosmt then EcCommands.pragma_check `WeakCheck; - - begin try while true do - let (src, prog) = EcIo.xparse reader in - let src = String.strip src in - match EcLocation.unloc prog with - | EP.P_Prog (commands, locterm) -> - List.iter (step src) commands; - if locterm then raise Exit - | EP.P_Undo i -> - last_src := src; - EcCommands.undo i - | EP.P_Exit -> - raise Exit - | EP.P_DocComment doc -> - last_src := src; - EcCommands.doc_comment doc - done with - | Exit | End_of_file -> () - | e -> - EcIo.finalize reader; - if nosmt then EcCommands.pragma_check `Check; - raise e - end; - - EcIo.finalize reader; - - (* Restore full SMT checking for interactive tactics *) - if nosmt then EcCommands.pragma_check `Check; - - (* If -trace is set, the last in-prefix sentence is still - pending. Run it with goal capture before and after, and - build the BEFORE/TACTIC/AFTER/SUMMARY response body. *) - let body = - if not trace then - goals_to_string () - else - let pre_state = - match !pending with - | None -> `Nothing - | Some _ when not (EcCommands.in_proof ()) -> `NotInProof - | Some (src, p) -> `Ready (src, p) - in - match pre_state with - | `Nothing -> failwith "trace: nothing to trace" - | `NotInProof -> - failwith - "trace: target sentence is not in a proof context" - | `Ready (src, p) -> - let loc = p.EP.gl_action.EcLocation.pl_loc in - let (sl, sc) = loc.EcLocation.loc_start in - let (el, ec) = loc.EcLocation.loc_end in - let before_goals = EcCommands.pp_all_goals () in - let n1 = List.length before_goals in - let buf = Buffer.create 1024 in - let fmt = Format.formatter_of_buffer buf in - Format.fprintf fmt - "=== BEFORE: line %d (col %d) ===@\n" sl sc; - EcCommands.pp_current_goal_or_noproof ~all:false fmt; - Format.fprintf fmt - "@\n=== TACTIC (lines %d:%d - %d:%d) ===@\n%s@\n@\n" - sl sc el ec (sentence_source loc); - last_src := src; - begin - try - process_action ~src p; - last_loc := Some loc; - pending := None; - let after_goals = EcCommands.pp_all_goals () in - let n2 = List.length after_goals in - Format.fprintf fmt - "=== AFTER: line %d (col %d) ===@\n" sl sc; - let before_set = - List.fold_left - (fun s g -> EcMaps.Sstr.add g s) - EcMaps.Sstr.empty before_goals - in - (* The new focused goal always counts as "modified" - (its focus status changed even if its text matches - an old sibling); the rest are printed only if - they didn't appear in BEFORE. *) - let to_print = - match after_goals with - | [] -> [] - | head :: tl -> - head :: - List.filter - (fun g -> not (EcMaps.Sstr.mem g before_set)) - tl - in - begin match to_print with - | [] -> Format.fprintf fmt "(no open goals)@\n" - | _ -> - List.iteri (fun i g -> - if i > 0 then Format.fprintf fmt "@\n"; - Format.fprintf fmt "%s@\n" g) - to_print - end; - Format.fprintf fmt - "@\n=== SUMMARY ===@\nopen goals: %d -> %d@\n" n1 n2; - Format.pp_print_flush fmt (); - Buffer.contents buf - with e -> - Format.fprintf fmt - "=== AFTER: line %d (col %d) ===@\n@\n" - sl sc; - Format.pp_print_flush fmt (); - trace_prefix := Buffer.contents buf; - raise (Trace_failed e) - end - in - - let tag = - let loaded = - match !last_loc with - | None -> "" - | Some loc -> - let (el, _) = loc.EcLocation.loc_end in - Printf.sprintf " [loaded:%s:%d]" filename el - in - loaded ^ focus_tag () - in - reply_ok ~tag body - - with - | EcCommands.Restart -> - do_initialize (); - Hashtbl.clear checkpoints; - transcript := []; - prior_bullets := None; - reply_ok "Session restarted" - | Trace_failed e -> - let msg = format_error ~src:!last_src e in - reply_error (!trace_prefix ^ msg) - | Failure s -> - reply_error s - | e -> - reply_error (format_error ~src:!last_src e) - in - - (* Initialize proof engine *) - do_initialize (); - - (* Signal ready *) - Printf.printf "READY [uuid:%d]\n\n%!" - (EcCommands.uuid ()); - - (* Main REPL loop *) - let multi_buf = Buffer.create 256 in - let in_multi = ref false in - - begin try while true do - let line = input_line stdin in - let line = String.strip line in - - (* Multi-line input: starts, flushes *) - if line = "" then begin - Buffer.clear multi_buf; - in_multi := true - end - else if line = "" && !in_multi then begin - let input = Buffer.contents multi_buf in - Buffer.clear multi_buf; - in_multi := false; - if input <> "" then process_ec_input input - end - else if !in_multi then begin - if Buffer.length multi_buf > 0 then - Buffer.add_char multi_buf ' '; - Buffer.add_string multi_buf line - end - - else if line = "" then - () - else if line = "QUIT" then - exit 0 - else if line = "HELP" then begin - Buffer.clear notices; - let buf = Buffer.create 4096 in - let path = llm_guide_path () in - begin try - let ic = open_in path in - begin try while true do - Buffer.add_char buf (input_char ic) - done with End_of_file -> () end; - close_in ic; - reply_ok (Buffer.contents buf) - with Sys_error e -> - reply_error (Printf.sprintf "cannot read guide: %s" e) - end - end - else if line = "UNDO" then begin - Buffer.clear notices; - let uuid = EcCommands.uuid () in - if uuid > 0 then begin - EcCommands.undo (uuid - 1); - transcript_trim (uuid - 1); - reply_ok_goals () - end else - reply_error "nothing to undo" - end - else if line = "GOALS ALL" then begin - Buffer.clear notices; - reply_ok (goals_to_string ~all:true ()) - end - else if line = "GOALS" then begin - Buffer.clear notices; - reply_ok (goals_to_string ()) - end - else if line = "TREE ALL" then begin - Buffer.clear notices; - reply_ok (tree_to_string ~all:true ()) - end - else if line = "TREE" then begin - Buffer.clear notices; - reply_ok (tree_to_string ()) - end - else if line = "COMMIT" then begin - Buffer.clear notices; - reply_ok (commit_proof_text ()) - end - else if String.starts_with line "FOCUS " || line = "NEXT" then begin - Buffer.clear notices; - let request = - if line = "NEXT" then `Next - else - let arg = String.strip ( - String.sub line 6 (String.length line - 6)) in - try `At (int_of_string arg) - with Failure _ -> `Bad arg - in - match request with - | `Bad arg -> - reply_error (Printf.sprintf "FOCUS: not an integer: %s" arg) - | _ -> - let entries = EcCommands.pp_tree () in - let n = List.length entries in - let target = - match request with - | `Next -> if n <= 1 then 1 else 2 - | `At k -> k - | `Bad _ -> 1 - in - begin match EcCommands.focus_goal target with - | Ok _ -> reply_ok_goals () - | Error msg -> reply_error msg - end - end - else if String.starts_with line "CHECKPOINT " then begin - Buffer.clear notices; - let name = String.strip ( - String.sub line 11 (String.length line - 11)) in - if name = "" then - reply_error "CHECKPOINT: missing name" - else begin - Hashtbl.replace checkpoints name (EcCommands.uuid ()); - reply_ok (Printf.sprintf - "checkpoint '%s' set at uuid %d" name (EcCommands.uuid ())) - end - end - else if String.starts_with line "REVERT " then begin - Buffer.clear notices; - let n = String.strip ( - String.sub line 7 (String.length line - 7)) in - let target = - try Some (int_of_string n) - with Failure _ -> Hashtbl.find_opt checkpoints n - in - begin match target with - | None -> - reply_error (Printf.sprintf - "REVERT: '%s' is not a valid uuid or checkpoint name" n) - | Some target -> - let uuid = EcCommands.uuid () in - if target < 0 || target > uuid then - reply_error (Printf.sprintf - "REVERT: uuid %d out of range [0, %d]" target uuid) - else begin - EcCommands.undo target; - transcript_trim target; - reply_ok_goals () - end - end - end - else if line = "QUIET ON" then begin - Buffer.clear notices; - quiet := true; - reply_ok "" - end - else if line = "QUIET OFF" then begin - Buffer.clear notices; - quiet := false; - reply_ok "" - end - else if String.starts_with line "SEARCH " then begin - let query = String.strip ( - String.sub line 7 (String.length line - 7)) in - let query = - if String.ends_with query "." - then String.sub query 0 (String.length query - 1) - else query - in - process_ec_input (Printf.sprintf "search %s." query) - end - else if String.starts_with line "LOAD " then - handle_load (String.sub line 5 (String.length line - 5)) - else - (* Treat as EasyCrypt input *) - process_ec_input line - done with - | End_of_file -> () - end; - - exit 0 - in - (* Initialize I/O + interaction module *) let module State = struct type t = { @@ -1404,7 +536,7 @@ let main () = end | `Llm llmopts -> - run_llm_repl llmopts + EcLlm.run ~relocdir ~boot:ldropts.ldro_boot llmopts | `Runtest _ -> (* Eagerly executed *) diff --git a/src/ecLlm.ml b/src/ecLlm.ml new file mode 100644 index 000000000..7d2cbdde6 --- /dev/null +++ b/src/ecLlm.ml @@ -0,0 +1,873 @@ +(* -------------------------------------------------------------------- *) +(* The LLM coding-agent REPL. See [ecLlm.mli] for the entry point. + + Implementation note: the REPL holds a large amount of mutable state + (notice buffer, transcript, checkpoints, ...). To keep that state + sharable across the various helpers without resorting to a big + record, [run] is a single closure that opens nested [module] blocks + for grouping. The submodules are read-only views over the closed- + over refs. *) + +open EcUtils + +module EP = EcParsetree + +(* -------------------------------------------------------------------- *) +(* Path to the bundled LLM-agent guide. *) +let llm_guide_path () = + let (module Sites) = EcRelocate.sites in + match EcRelocate.sourceroot with + | Some root -> + Filename.concat (Filename.concat root "doc/llm") "CLAUDE.md" + | None -> + Filename.concat Sites.doc "llm-guide.md" + +(* Print the bundled guide to stdout. Used by [-help]. *) +let print_llm_guide () = + let path = llm_guide_path () in + try + let ic = open_in path in + begin try while true do + print_char (input_char ic) + done with End_of_file -> () end; + close_in ic + with Sys_error e -> + Printf.eprintf "cannot read LLM guide: %s\n%!" e + +(* -------------------------------------------------------------------- *) +let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = + if llmopts.llmo_help then begin + print_llm_guide (); + exit 0 + end; + + let prvopts = llmopts.llmo_provers in + Random.self_init (); + + prvopts.prvo_why3server |> oiter (fun server -> + try + Why3.Prove_client.connect_external server + with Why3.Prove_client.ConnectionError e -> + Format.eprintf + "cannot connect to Why3 server `%s': %s" server e; + exit 1); + + (match relocdir with + | None -> EcCommands.addidir Filename.current_dir_name + | Some pwd -> EcCommands.addidir pwd); + + let checkmode = { + EcCommands.cm_checkall = prvopts.prvo_checkall; + EcCommands.cm_timeout = odfl 3 prvopts.prvo_timeout; + EcCommands.cm_cpufactor = odfl 1 prvopts.prvo_cpufactor; + EcCommands.cm_nprovers = odfl 4 prvopts.prvo_maxjobs; + EcCommands.cm_provers = prvopts.prvo_provers; + EcCommands.cm_quorum = prvopts.prvo_quorum; + EcCommands.cm_profile = prvopts.prvo_profile; + } in + + (* ------------------------------------------------------------------ *) + (* State. *) + + (* Messages emitted by the engine during a phrase; flushed into the + next OK/ERROR reply. *) + let notices = Buffer.create 256 in + + (* Has [EcCommands.initialize] been called? Subsequent calls pass + [~restart:true]. *) + let initialized = ref false in + + (* True iff replies should suppress goal bodies. Toggled by QUIET. *) + let quiet = ref false in + + (* CHECKPOINT name -> uuid. *) + let checkpoints : (string, int) Hashtbl.t = Hashtbl.create 16 in + + (* Transcript of REPL-typed phrases that succeeded. Each entry is + [(uuid_before, src, parent, opens_at_entry)]: + - [parent]: focused handle right before the phrase ([None] iff + outside a proof); + - [opens_at_entry]: full open-handle list (focused first), used + by [Commit] to seed the sibling map when the first recorded + phrase already sits inside a frame opened by the LOAD prefix. + Trimmed by UNDO/REVERT; cleared on LOAD/Restart. *) + let transcript : + (int * string * EcCoreGoal.handle option + * EcCoreGoal.handle list) list ref = ref [] in + + (* The bullet stack of the active proof at the moment REPL input + took over. Captured the first time [disable_repl_bullets] clears + a non-empty stack. Used by [Commit] to pick bullet characters + that don't collide with frames opened by the LOAD prefix. + Cleared with the transcript on LOAD/Restart. *) + let prior_bullets : EcBullets.stack option ref = ref None in + + let notifier (_ : EcGState.loglevel) (lazy msg) = + Buffer.add_string notices msg; + Buffer.add_char notices '\n' + in + + let do_initialize () = + EcCommands.initialize + ~restart:!initialized ~undo:true + ~boot ~checkmode ~checkproof:true; + initialized := true; + (try + List.iter EcCommands.apply_pragma prvopts.prvo_pragmas + with EcCommands.InvalidPragma x -> + EcScope.hierror "invalid pragma: `%s'\n%!" x); + EcCommands.addnotifier notifier; + oiter (fun ppwidth -> + let gs = EcEnv.gstate (EcScope.env (EcCommands.current ())) in + EcGState.setvalue "PP:width" (`Int ppwidth) gs) + prvopts.prvo_ppwidth + in + + (* ------------------------------------------------------------------ *) + (* Goal/error formatting: shared between the wire layer and the + -trace block. *) + let module Goals = struct + let format_error ?(src="") e = + let base = match e with + | EcScope.TopError (loc, e) -> + let msg = String.strip (EcPException.tostring e) in + if loc = EcLocation._dummy then msg + else Format.asprintf "%s: %s" (EcLocation.tostring loc) msg + | e -> + String.strip (EcPException.tostring e) + in + if src = "" then base + else Printf.sprintf "%s\nsource: %s" base src + + let goals_to_string ?(all=false) () = + let buf = Buffer.create 256 in + let fmt = Format.formatter_of_buffer buf in + EcCommands.pp_current_goal_or_noproof ~all fmt; + Format.pp_print_flush fmt (); + Buffer.contents buf + + (* Render the focus-tree of open subgoals. [all=false] gives a + one-line digest per goal; [all=true] gives the full goal body. *) + let tree_to_string ?(all=false) () = + let entries = EcCommands.pp_tree ~all () in + match entries with + | [] -> "No active proof.\n" + | _ -> + let buf = Buffer.create 256 in + let one_line s = + let s = + match String.index_opt s '\n' with + | None -> s + | Some k -> String.sub s 0 k + in + let limit = 80 in + if String.length s > limit + then String.sub s 0 (limit - 1) ^ "…" + else s + in + List.iter (fun (i, focused, text) -> + let marker = if focused then " <- focused" else "" in + if all then + Buffer.add_string buf + (Printf.sprintf "[%d]%s\n%s\n" i marker text) + else + Buffer.add_string buf + (Printf.sprintf "[%d] %s%s\n" i (one_line text) marker) + ) entries; + Buffer.contents buf + + (* Inline focus annotation ([focus: 1/N]) appended to reply tags + whenever the active proof has >=2 open subgoals. *) + let focus_tag () = + match EcCommands.pp_tree () with + | _ :: _ :: _ as entries -> + Printf.sprintf " [focus: 1/%d]" (List.length entries) + | _ -> "" + end in + + (* ------------------------------------------------------------------ *) + (* OK/ERROR/ wire envelope. *) + let module Wire = struct + let reply_ok ?(tag="") body = + let n = Buffer.contents notices in + Printf.printf "OK [uuid:%d]%s\n" (EcCommands.uuid ()) tag; + if n <> "" then print_string n; + if body <> "" then begin + print_string body; + let len = String.length body in + if len > 0 && body.[len - 1] <> '\n' then + print_char '\n' + end; + Printf.printf "\n%!"; + Buffer.clear notices + + let reply_ok_goals ?(all=false) () = + let tag = Goals.focus_tag () in + if !quiet then reply_ok ~tag "" + else reply_ok ~tag (Goals.goals_to_string ~all ()) + + let reply_error msg = + let goals = Goals.goals_to_string () in + Printf.printf "ERROR [uuid:%d]\n%s\n" (EcCommands.uuid ()) msg; + if goals <> "" then begin + print_string goals; + let len = String.length goals in + if len > 0 && goals.[len - 1] <> '\n' then + print_char '\n' + end; + Printf.printf "\n%!"; + Buffer.clear notices + end in + + (* ------------------------------------------------------------------ *) + (* Transcript manipulation. *) + let module Transcript = struct + let trim target = + transcript := + List.filter + (fun (uuid_before, _, _, _) -> uuid_before < target) + !transcript + + let clear () = + transcript := []; + prior_bullets := None + end in + + (* ------------------------------------------------------------------ *) + (* Process a single EasyCrypt command, respecting [gl_fail]. When + [~record:true], append a transcript entry on success: the parent + handle (focused goal before the phrase) and the open-handle list, + which together let [Commit] reconstruct bullet structure. *) + let process_action ?(record=false) ~src (p : EP.global) = + let loc = p.EP.gl_action.EcLocation.pl_loc in + let pre_uuid = EcCommands.uuid () in + let opens_pre = + if record then EcCommands.open_handles () else [] + in + let parent = + match opens_pre with h :: _ -> Some h | [] -> None + in + let succeeded = ref false in + begin try + ignore (EcCommands.process ~src p.EP.gl_action : float option); + succeeded := true + with + | EcCommands.Restart -> raise EcCommands.Restart + | _ when p.EP.gl_fail -> () + | e -> raise (EcScope.toperror_of_exn ~gloc:loc e) + end; + if !succeeded && p.EP.gl_fail then + raise (EcScope.toperror_of_exn ~gloc:loc + (EcScope.HiScopeError (None, + "this command is expected to fail"))); + if record && !succeeded && not p.EP.gl_fail then + transcript := (pre_uuid, src, parent, opens_pre) :: !transcript + in + + (* ------------------------------------------------------------------ *) + (* COMMIT: replay the transcript against the proof DAG (parent_of / + children_of, backed by [EcCoreGoal.pr_parent]), inserting bullets + at multi-child splits. Bullet tokens skip any character already on + the LOAD prefix's [puc_bullets] stack so emitted bullets cannot + collide with frames opened by the prefix. *) + let module Commit = struct + (* Token order matches PR 1017's lexer: -, +, *, --, ++, **, + ---, +++, *** ... *) + let token_at_index i = + let chars = [| "-"; "+"; "*" |] in + let rep = i / 3 + 1 in + let chr = chars.(i mod 3) in + String.concat "" (List.init rep (fun _ -> chr)) + + let proof_text () = + let entries = List.rev !transcript in + let buf = Buffer.create 1024 in + let emit_indent depth = + for _ = 1 to depth do Buffer.add_string buf " " done + in + let module Hmap = + Map.Make (struct + type t = EcCoreGoal.handle + let compare = compare + end) + in + let sibling_depth : int Hmap.t ref = ref Hmap.empty in + let current_depth = ref 0 in + (* Pick a bullet token for each depth, skipping tokens already + in scope from the LOAD prefix's bullet stack. *) + let bullet_to_string (b : EcParsetree.bullet) = + let ch = + match b.b_kind with + | `Minus -> "-" + | `Plus -> "+" + | `Star -> "*" + in + String.concat "" (List.init b.b_count (fun _ -> ch)) + in + let in_use_tokens = + match !prior_bullets with + | None -> [] + | Some stack -> + List.map + (fun (f : EcBullets.frame) -> bullet_to_string f.bf_bullet) + stack + in + let depth_cache : (int, string) Hashtbl.t = Hashtbl.create 8 in + let next_tok_idx = ref 0 in + let assigned_tokens = ref [] in + let bullet_for_depth d = + match Hashtbl.find_opt depth_cache d with + | Some t -> t + | None -> + let rec pick () = + let t = token_at_index !next_tok_idx in + incr next_tok_idx; + if List.mem t in_use_tokens || List.mem t !assigned_tokens + then pick () + else t + in + let t = pick () in + assigned_tokens := t :: !assigned_tokens; + Hashtbl.add depth_cache d t; + t + in + (* Seed: if the first recorded phrase entered a state with + multiple open goals, the LOAD prefix opened a frame whose + siblings are still pending. Register all of them at depth 1 + so the first phrase's parent gets a bullet. *) + (match entries with + | (_, _, Some _, (_ :: _ :: _ as opens)) :: _ -> + List.iter + (fun h -> sibling_depth := Hmap.add h 1 !sibling_depth) + opens + | _ -> ()); + List.iter (fun (_uuid, src, parent_opt, _opens) -> + match parent_opt with + | None -> + Buffer.add_string buf src; + Buffer.add_char buf '\n' + | Some parent -> + (* Walk upward via pr_parent until we hit a registered + sibling ancestor. If found, emit its bullet and consume + the registration. *) + let rec find_ancestor h = + match Hmap.find_opt h !sibling_depth with + | Some d -> Some (h, d) + | None -> + match EcCommands.parent_of h with + | Some p -> find_ancestor p + | None -> None + in + (match find_ancestor parent with + | Some (h, d) -> + emit_indent (d - 1); + Buffer.add_string buf (bullet_for_depth d); + Buffer.add_char buf ' '; + current_depth := d; + sibling_depth := Hmap.remove h !sibling_depth + | None -> + emit_indent !current_depth); + Buffer.add_string buf src; + Buffer.add_char buf '\n'; + (* Register fresh siblings: walk the subtree rooted at + [parent], finding every multi-child split, and register + each such child at the right depth. Single-child links + are continuations and don't bump depth; multi-child + links do. A compound phrase like [split; split.] can + produce nested splits within one phrase. *) + let rec walk h d = + match EcCommands.children_of h with + | [c] -> walk c d + | (_ :: _ :: _) as cs -> + List.iter + (fun c -> + sibling_depth := + Hmap.add c d !sibling_depth; + walk c (d + 1)) + cs + | [] -> () + in + walk parent (!current_depth + 1) + ) entries; + Buffer.contents buf + end in + + (* ------------------------------------------------------------------ *) + (* Process EasyCrypt input typed at the REPL prompt (single phrase + or a line ending with a "."). *) + let process_ec_input input = + Buffer.clear notices; + (* On the first REPL phrase of each proof, capture the bullet stack + the LOAD prefix left so COMMIT can avoid token collisions with + it. Subsequent calls return [None] and don't clobber the snapshot. *) + (match EcCommands.disable_repl_bullets () with + | None -> () + | Some _ as snapshot -> prior_bullets := snapshot); + let reader = EcIo.from_string input in + let last_src = ref "" in + begin try + let (src, prog) = EcIo.xparse reader in + let src = String.strip src in + last_src := src; + begin match EcLocation.unloc prog with + | EP.P_Prog (commands, _) -> + List.iter (process_action ~record:true ~src) commands; + Wire.reply_ok_goals () + | EP.P_Undo i -> + EcCommands.undo i; + Transcript.trim i; + Wire.reply_ok_goals () + | EP.P_Exit -> + EcIo.finalize reader; exit 0 + | EP.P_DocComment doc -> + EcCommands.doc_comment doc; + Wire.reply_ok "" + end + with + | EcCommands.Restart -> + do_initialize (); + Transcript.clear (); + Wire.reply_ok "Session restarted" + | e -> + Wire.reply_error (Goals.format_error ~src:!last_src e) + end; + EcIo.finalize reader + in + + (* ------------------------------------------------------------------ *) + (* LOAD "file.ec" [LINE[:COL]] [-nosmt] [-trace]. *) + let module Load = struct + let handle args = + Buffer.clear notices; + let args = String.strip args in + let last_src = ref "" in + let trace_prefix = ref "" in + let exception Trace_failed of exn in + + try + (* Parse quoted or unquoted filename. *) + let filename, rest = + if String.length args > 0 && args.[0] = '"' then + let close = + try String.index_from args 1 '"' + with Not_found -> + failwith "LOAD: unterminated filename" + in + let fn = String.sub args 1 (close - 1) in + let rest = String.strip ( + String.sub args (close + 1) + (String.length args - close - 1)) in + (fn, rest) + else + match String.split_on_char ' ' args with + | [] -> failwith "LOAD: missing filename" + | [f] -> (f, "") + | f :: rest -> (f, String.concat " " rest) + in + + (* Parse optional LINE[:COL] and flags (-nosmt, -trace). *) + let upto, nosmt, trace = + let words = + String.split_on_char ' ' rest + |> List.filter (fun s -> s <> "") + in + let nosmt = List.mem "-nosmt" words in + let trace = List.mem "-trace" words in + let words = + List.filter + (fun s -> s <> "-nosmt" && s <> "-trace") + words + in + let upto = match words with + | [] -> None + | [w] -> + begin match String.split_on_char ':' w with + | [line] -> + Some (int_of_string line, None) + | [line; col] -> + Some (int_of_string line, Some (int_of_string col)) + | _ -> failwith "LOAD: invalid LINE[:COL] format" + end + | _ -> failwith "LOAD: unexpected arguments" + in + (upto, nosmt, trace) + in + + begin try + ignore (EcLoader.getkind + (Filename.extension filename) : EcLoader.kind) + with EcLoader.BadExtension ext -> + failwith (Format.sprintf + "unknown file extension: %s" ext) + end; + + do_initialize (); + Hashtbl.clear checkpoints; + Transcript.clear (); + EcCommands.addidir (Filename.dirname filename); + + let reader = EcIo.from_file filename in + + let past_upto (loc : EcLocation.t) = + match upto with + | None -> false + | Some (line, col) -> + let (el, ec) = loc.loc_end in + el > line || (el = line && match col with + | None -> false + | Some c -> ec > c) + in + + let last_loc = ref None in + + (* For -trace: lazy whole-file bytes, used to slice the exact + source text of a sentence by byte offsets. *) + let input_bytes = lazy ( + let ic = open_in_bin filename in + let n = in_channel_length ic in + let b = Bytes.create n in + really_input ic b 0 n; + close_in ic; + Bytes.unsafe_to_string b) + in + let sentence_source (loc : EcLocation.t) = + let s = Lazy.force input_bytes in + let lo = max 0 loc.EcLocation.loc_bchar in + let hi = min (String.length s) loc.EcLocation.loc_echar in + if hi <= lo then "" else String.sub s lo (hi - lo) + in + + (* For -trace: defer execution of the last sentence within the + prefix so we can capture goals before and after it. *) + let pending : (string * EP.global) option ref = ref None in + let flush_pending () = + match !pending with + | None -> () + | Some (src, p) -> + last_src := src; + process_action ~src p; + last_loc := Some p.EP.gl_action.EcLocation.pl_loc; + pending := None + in + let step src p = + let loc = p.EP.gl_action.EcLocation.pl_loc in + if past_upto loc then raise Exit; + if trace then begin + flush_pending (); + pending := Some (src, p) + end else begin + last_src := src; + process_action ~src p; + last_loc := Some loc + end + in + + if nosmt then EcCommands.pragma_check `WeakCheck; + + begin try while true do + let (src, prog) = EcIo.xparse reader in + let src = String.strip src in + match EcLocation.unloc prog with + | EP.P_Prog (commands, locterm) -> + List.iter (step src) commands; + if locterm then raise Exit + | EP.P_Undo i -> + last_src := src; + EcCommands.undo i + | EP.P_Exit -> + raise Exit + | EP.P_DocComment doc -> + last_src := src; + EcCommands.doc_comment doc + done with + | Exit | End_of_file -> () + | e -> + EcIo.finalize reader; + if nosmt then EcCommands.pragma_check `Check; + raise e + end; + + EcIo.finalize reader; + + if nosmt then EcCommands.pragma_check `Check; + + (* If -trace is set, the last in-prefix sentence is still + pending. Run it under goal capture and build the + BEFORE/TACTIC/AFTER/SUMMARY response body. *) + let body = + if not trace then + Goals.goals_to_string () + else + let pre_state = + match !pending with + | None -> `Nothing + | Some _ when not (EcCommands.in_proof ()) -> `NotInProof + | Some (src, p) -> `Ready (src, p) + in + match pre_state with + | `Nothing -> failwith "trace: nothing to trace" + | `NotInProof -> + failwith + "trace: target sentence is not in a proof context" + | `Ready (src, p) -> + let loc = p.EP.gl_action.EcLocation.pl_loc in + let (sl, sc) = loc.EcLocation.loc_start in + let (el, ec) = loc.EcLocation.loc_end in + let before_goals = EcCommands.pp_all_goals () in + let n1 = List.length before_goals in + let buf = Buffer.create 1024 in + let fmt = Format.formatter_of_buffer buf in + Format.fprintf fmt + "=== BEFORE: line %d (col %d) ===@\n" sl sc; + EcCommands.pp_current_goal_or_noproof ~all:false fmt; + Format.fprintf fmt + "@\n=== TACTIC (lines %d:%d - %d:%d) ===@\n%s@\n@\n" + sl sc el ec (sentence_source loc); + last_src := src; + begin + try + process_action ~src p; + last_loc := Some loc; + pending := None; + let after_goals = EcCommands.pp_all_goals () in + let n2 = List.length after_goals in + Format.fprintf fmt + "=== AFTER: line %d (col %d) ===@\n" sl sc; + let before_set = + List.fold_left + (fun s g -> EcMaps.Sstr.add g s) + EcMaps.Sstr.empty before_goals + in + (* The new focused goal always counts as "modified" + (its focus status changed even if its text matches + an old sibling); the rest are printed only if they + didn't appear in BEFORE. *) + let to_print = + match after_goals with + | [] -> [] + | head :: tl -> + head :: + List.filter + (fun g -> not (EcMaps.Sstr.mem g before_set)) + tl + in + begin match to_print with + | [] -> Format.fprintf fmt "(no open goals)@\n" + | _ -> + List.iteri (fun i g -> + if i > 0 then Format.fprintf fmt "@\n"; + Format.fprintf fmt "%s@\n" g) + to_print + end; + Format.fprintf fmt + "@\n=== SUMMARY ===@\nopen goals: %d -> %d@\n" n1 n2; + Format.pp_print_flush fmt (); + Buffer.contents buf + with e -> + Format.fprintf fmt + "=== AFTER: line %d (col %d) ===@\n@\n" + sl sc; + Format.pp_print_flush fmt (); + trace_prefix := Buffer.contents buf; + raise (Trace_failed e) + end + in + + let tag = + let loaded = + match !last_loc with + | None -> "" + | Some loc -> + let (el, _) = loc.EcLocation.loc_end in + Printf.sprintf " [loaded:%s:%d]" filename el + in + loaded ^ Goals.focus_tag () + in + Wire.reply_ok ~tag body + + with + | EcCommands.Restart -> + do_initialize (); + Hashtbl.clear checkpoints; + Transcript.clear (); + Wire.reply_ok "Session restarted" + | Trace_failed e -> + let msg = Goals.format_error ~src:!last_src e in + Wire.reply_error (!trace_prefix ^ msg) + | Failure s -> + Wire.reply_error s + | e -> + Wire.reply_error (Goals.format_error ~src:!last_src e) + end in + + (* ------------------------------------------------------------------ *) + (* Main loop: line-by-line dispatcher. *) + + do_initialize (); + + Printf.printf "READY [uuid:%d]\n\n%!" (EcCommands.uuid ()); + + let multi_buf = Buffer.create 256 in + let in_multi = ref false in + + begin try while true do + let line = input_line stdin in + let line = String.strip line in + + if line = "" then begin + Buffer.clear multi_buf; + in_multi := true + end + else if line = "" && !in_multi then begin + let input = Buffer.contents multi_buf in + Buffer.clear multi_buf; + in_multi := false; + if input <> "" then process_ec_input input + end + else if !in_multi then begin + if Buffer.length multi_buf > 0 then + Buffer.add_char multi_buf ' '; + Buffer.add_string multi_buf line + end + + else if line = "" then + () + else if line = "QUIT" then + exit 0 + else if line = "HELP" then begin + Buffer.clear notices; + let buf = Buffer.create 4096 in + let path = llm_guide_path () in + begin try + let ic = open_in path in + begin try while true do + Buffer.add_char buf (input_char ic) + done with End_of_file -> () end; + close_in ic; + Wire.reply_ok (Buffer.contents buf) + with Sys_error e -> + Wire.reply_error (Printf.sprintf "cannot read guide: %s" e) + end + end + else if line = "UNDO" then begin + Buffer.clear notices; + let uuid = EcCommands.uuid () in + if uuid > 0 then begin + EcCommands.undo (uuid - 1); + Transcript.trim (uuid - 1); + Wire.reply_ok_goals () + end else + Wire.reply_error "nothing to undo" + end + else if line = "GOALS ALL" then begin + Buffer.clear notices; + Wire.reply_ok (Goals.goals_to_string ~all:true ()) + end + else if line = "GOALS" then begin + Buffer.clear notices; + Wire.reply_ok (Goals.goals_to_string ()) + end + else if line = "TREE ALL" then begin + Buffer.clear notices; + Wire.reply_ok (Goals.tree_to_string ~all:true ()) + end + else if line = "TREE" then begin + Buffer.clear notices; + Wire.reply_ok (Goals.tree_to_string ()) + end + else if line = "COMMIT" then begin + Buffer.clear notices; + Wire.reply_ok (Commit.proof_text ()) + end + else if String.starts_with line "FOCUS " || line = "NEXT" then begin + Buffer.clear notices; + let request = + if line = "NEXT" then `Next + else + let arg = String.strip ( + String.sub line 6 (String.length line - 6)) in + try `At (int_of_string arg) + with Failure _ -> `Bad arg + in + match request with + | `Bad arg -> + Wire.reply_error (Printf.sprintf "FOCUS: not an integer: %s" arg) + | _ -> + let entries = EcCommands.pp_tree () in + let n = List.length entries in + let target = + match request with + | `Next -> if n <= 1 then 1 else 2 + | `At k -> k + | `Bad _ -> 1 + in + begin match EcCommands.focus_goal target with + | Ok _ -> Wire.reply_ok_goals () + | Error msg -> Wire.reply_error msg + end + end + else if String.starts_with line "CHECKPOINT " then begin + Buffer.clear notices; + let name = String.strip ( + String.sub line 11 (String.length line - 11)) in + if name = "" then + Wire.reply_error "CHECKPOINT: missing name" + else begin + Hashtbl.replace checkpoints name (EcCommands.uuid ()); + Wire.reply_ok (Printf.sprintf + "checkpoint '%s' set at uuid %d" name (EcCommands.uuid ())) + end + end + else if String.starts_with line "REVERT " then begin + Buffer.clear notices; + let n = String.strip ( + String.sub line 7 (String.length line - 7)) in + let target = + try Some (int_of_string n) + with Failure _ -> Hashtbl.find_opt checkpoints n + in + begin match target with + | None -> + Wire.reply_error (Printf.sprintf + "REVERT: '%s' is not a valid uuid or checkpoint name" n) + | Some target -> + let uuid = EcCommands.uuid () in + if target < 0 || target > uuid then + Wire.reply_error (Printf.sprintf + "REVERT: uuid %d out of range [0, %d]" target uuid) + else begin + EcCommands.undo target; + Transcript.trim target; + Wire.reply_ok_goals () + end + end + end + else if line = "QUIET ON" then begin + Buffer.clear notices; + quiet := true; + Wire.reply_ok "" + end + else if line = "QUIET OFF" then begin + Buffer.clear notices; + quiet := false; + Wire.reply_ok "" + end + else if String.starts_with line "SEARCH " then begin + let query = String.strip ( + String.sub line 7 (String.length line - 7)) in + let query = + if String.ends_with query "." + then String.sub query 0 (String.length query - 1) + else query + in + process_ec_input (Printf.sprintf "search %s." query) + end + else if String.starts_with line "LOAD " then + Load.handle (String.sub line 5 (String.length line - 5)) + else + process_ec_input line + done with + | End_of_file -> () + end; + + exit 0 diff --git a/src/ecLlm.mli b/src/ecLlm.mli new file mode 100644 index 000000000..b12dde1ef --- /dev/null +++ b/src/ecLlm.mli @@ -0,0 +1,11 @@ +(* -------------------------------------------------------------------- *) +(* The LLM coding-agent REPL: an interactive proof-development protocol + over stdin/stdout. Driven via the [easycrypt llm] command. *) + +(* Run the REPL until [QUIT] or EOF, then exit the process. Never + returns. *) +val run : + relocdir:string option + -> boot:bool + -> EcOptions.llm_option + -> 'a From 09c4408f74547a04e88e811f35fdc6d001734446 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 30 May 2026 11:01:59 +0200 Subject: [PATCH 07/10] [llm] split REPL dispatcher into Parse and Dispatch submodules 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. --- src/ecLlm.ml | 301 +++++++++++++++++++++++++++++++-------------------- 1 file changed, 184 insertions(+), 117 deletions(-) diff --git a/src/ecLlm.ml b/src/ecLlm.ml index 7d2cbdde6..dc89c2a12 100644 --- a/src/ecLlm.ml +++ b/src/ecLlm.ml @@ -703,38 +703,99 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = (* ------------------------------------------------------------------ *) (* Main loop: line-by-line dispatcher. *) - do_initialize (); + (* ------------------------------------------------------------------ *) + (* Surface command vocabulary. Parsing turns each stdin line into one + of these, and dispatch is a flat pattern-match. Argument + parsing/validation lives in [Parse]; commands that interact with + mutable state (checkpoints table, multi-line buffer) carry only + the raw user-supplied data and let [Dispatch] do the lookup. *) + let module Parse = struct + type command = + | Quit + | Help + | Undo + | Goals of [`One | `All] + | Tree of [`One | `All] + | Commit + | Focus of int + | Next + | Checkpoint of string + | Revert of string (* uuid-or-name; Dispatch resolves *) + | Quiet of bool + | Search of string (* trailing "." already stripped *) + | Load of string (* raw arg tail; Load.handle parses *) + | Ec of string (* fall-through: raw EasyCrypt input *) + | Begin_multi + | Done_multi + | Multi_line of string + | Blank + + exception Parse_error of string + + let rest n line = + String.strip (String.sub line n (String.length line - n)) + + let parse_focus arg = + try Focus (int_of_string arg) + with Failure _ -> + raise (Parse_error + (Printf.sprintf "FOCUS: not an integer: %s" arg)) + + let parse_checkpoint name = + if name = "" then + raise (Parse_error "CHECKPOINT: missing name"); + Checkpoint name - Printf.printf "READY [uuid:%d]\n\n%!" (EcCommands.uuid ()); + let parse_search query = + let query = + if String.ends_with query "." + then String.sub query 0 (String.length query - 1) + else query + in + Search query + + let of_line ~multi_active (raw : string) : command = + let line = String.strip raw in + if multi_active then + if line = "" then Done_multi + else Multi_line line + else + match line with + | "" -> Begin_multi + | "" -> Blank + | "QUIT" -> Quit + | "HELP" -> Help + | "UNDO" -> Undo + | "GOALS" -> Goals `One + | "GOALS ALL" -> Goals `All + | "TREE" -> Tree `One + | "TREE ALL" -> Tree `All + | "COMMIT" -> Commit + | "NEXT" -> Next + | "QUIET ON" -> Quiet true + | "QUIET OFF" -> Quiet false + | _ when String.starts_with line "FOCUS " -> + parse_focus (rest 6 line) + | _ when String.starts_with line "CHECKPOINT " -> + parse_checkpoint (rest 11 line) + | _ when String.starts_with line "REVERT " -> + Revert (rest 7 line) + | _ when String.starts_with line "SEARCH " -> + parse_search (rest 7 line) + | _ when String.starts_with line "LOAD " -> + Load (rest 5 line) + | _ -> Ec line + end in + (* ------------------------------------------------------------------ *) + (* Command handlers. Each takes (already-parsed) data and produces a + wire reply via [Wire] (or exits the process). Multi-line state is + held here so [Parse] can stay pure. *) let multi_buf = Buffer.create 256 in - let in_multi = ref false in - - begin try while true do - let line = input_line stdin in - let line = String.strip line in + let in_multi = ref false in - if line = "" then begin - Buffer.clear multi_buf; - in_multi := true - end - else if line = "" && !in_multi then begin - let input = Buffer.contents multi_buf in - Buffer.clear multi_buf; - in_multi := false; - if input <> "" then process_ec_input input - end - else if !in_multi then begin - if Buffer.length multi_buf > 0 then - Buffer.add_char multi_buf ' '; - Buffer.add_string multi_buf line - end - - else if line = "" then - () - else if line = "QUIT" then - exit 0 - else if line = "HELP" then begin + let module Dispatch = struct + let do_help () = Buffer.clear notices; let buf = Buffer.create 4096 in let path = llm_guide_path () in @@ -748,8 +809,8 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = with Sys_error e -> Wire.reply_error (Printf.sprintf "cannot read guide: %s" e) end - end - else if line = "UNDO" then begin + + let do_undo () = Buffer.clear notices; let uuid = EcCommands.uuid () in if uuid > 0 then begin @@ -758,78 +819,38 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = Wire.reply_ok_goals () end else Wire.reply_error "nothing to undo" - end - else if line = "GOALS ALL" then begin - Buffer.clear notices; - Wire.reply_ok (Goals.goals_to_string ~all:true ()) - end - else if line = "GOALS" then begin - Buffer.clear notices; - Wire.reply_ok (Goals.goals_to_string ()) - end - else if line = "TREE ALL" then begin - Buffer.clear notices; - Wire.reply_ok (Goals.tree_to_string ~all:true ()) - end - else if line = "TREE" then begin - Buffer.clear notices; - Wire.reply_ok (Goals.tree_to_string ()) - end - else if line = "COMMIT" then begin - Buffer.clear notices; - Wire.reply_ok (Commit.proof_text ()) - end - else if String.starts_with line "FOCUS " || line = "NEXT" then begin + + let do_focus_request request = + (* [request] is the user's intent normalized; [`Next] is "second + sibling unless only one open". *) Buffer.clear notices; - let request = - if line = "NEXT" then `Next - else - let arg = String.strip ( - String.sub line 6 (String.length line - 6)) in - try `At (int_of_string arg) - with Failure _ -> `Bad arg + let entries = EcCommands.pp_tree () in + let n = List.length entries in + let target = + match request with + | `Next -> if n <= 1 then 1 else 2 + | `At k -> k in - match request with - | `Bad arg -> - Wire.reply_error (Printf.sprintf "FOCUS: not an integer: %s" arg) - | _ -> - let entries = EcCommands.pp_tree () in - let n = List.length entries in - let target = - match request with - | `Next -> if n <= 1 then 1 else 2 - | `At k -> k - | `Bad _ -> 1 - in - begin match EcCommands.focus_goal target with - | Ok _ -> Wire.reply_ok_goals () - | Error msg -> Wire.reply_error msg - end - end - else if String.starts_with line "CHECKPOINT " then begin + match EcCommands.focus_goal target with + | Ok _ -> Wire.reply_ok_goals () + | Error msg -> Wire.reply_error msg + + let do_checkpoint name = Buffer.clear notices; - let name = String.strip ( - String.sub line 11 (String.length line - 11)) in - if name = "" then - Wire.reply_error "CHECKPOINT: missing name" - else begin - Hashtbl.replace checkpoints name (EcCommands.uuid ()); - Wire.reply_ok (Printf.sprintf - "checkpoint '%s' set at uuid %d" name (EcCommands.uuid ())) - end - end - else if String.starts_with line "REVERT " then begin + Hashtbl.replace checkpoints name (EcCommands.uuid ()); + Wire.reply_ok (Printf.sprintf + "checkpoint '%s' set at uuid %d" name (EcCommands.uuid ())) + + let do_revert spec = Buffer.clear notices; - let n = String.strip ( - String.sub line 7 (String.length line - 7)) in let target = - try Some (int_of_string n) - with Failure _ -> Hashtbl.find_opt checkpoints n + try Some (int_of_string spec) + with Failure _ -> Hashtbl.find_opt checkpoints spec in - begin match target with + match target with | None -> Wire.reply_error (Printf.sprintf - "REVERT: '%s' is not a valid uuid or checkpoint name" n) + "REVERT: '%s' is not a valid uuid or checkpoint name" spec) | Some target -> let uuid = EcCommands.uuid () in if target < 0 || target > uuid then @@ -840,32 +861,78 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = Transcript.trim target; Wire.reply_ok_goals () end - end - end - else if line = "QUIET ON" then begin - Buffer.clear notices; - quiet := true; - Wire.reply_ok "" - end - else if line = "QUIET OFF" then begin + + let do_quiet on = Buffer.clear notices; - quiet := false; + quiet := on; Wire.reply_ok "" - end - else if String.starts_with line "SEARCH " then begin - let query = String.strip ( - String.sub line 7 (String.length line - 7)) in - let query = - if String.ends_with query "." - then String.sub query 0 (String.length query - 1) - else query - in + + let do_search query = process_ec_input (Printf.sprintf "search %s." query) - end - else if String.starts_with line "LOAD " then - Load.handle (String.sub line 5 (String.length line - 5)) - else - process_ec_input line + + let do_begin_multi () = + Buffer.clear multi_buf; + in_multi := true + + let do_done_multi () = + let input = Buffer.contents multi_buf in + Buffer.clear multi_buf; + in_multi := false; + if input <> "" then process_ec_input input + + let do_multi_line s = + if Buffer.length multi_buf > 0 then + Buffer.add_char multi_buf ' '; + Buffer.add_string multi_buf s + + let run (cmd : Parse.command) = + match cmd with + | Blank -> () + | Quit -> exit 0 + | Help -> do_help () + | Undo -> do_undo () + | Goals `One -> + Buffer.clear notices; + Wire.reply_ok (Goals.goals_to_string ()) + | Goals `All -> + Buffer.clear notices; + Wire.reply_ok (Goals.goals_to_string ~all:true ()) + | Tree `One -> + Buffer.clear notices; + Wire.reply_ok (Goals.tree_to_string ()) + | Tree `All -> + Buffer.clear notices; + Wire.reply_ok (Goals.tree_to_string ~all:true ()) + | Commit -> + Buffer.clear notices; + Wire.reply_ok (Commit.proof_text ()) + | Focus k -> do_focus_request (`At k) + | Next -> do_focus_request `Next + | Checkpoint n -> do_checkpoint n + | Revert s -> do_revert s + | Quiet on -> do_quiet on + | Search q -> do_search q + | Load args -> Load.handle args + | Ec input -> process_ec_input input + | Begin_multi -> do_begin_multi () + | Done_multi -> do_done_multi () + | Multi_line s -> do_multi_line s + end in + + (* ------------------------------------------------------------------ *) + (* Main loop. *) + + do_initialize (); + + Printf.printf "READY [uuid:%d]\n\n%!" (EcCommands.uuid ()); + + begin try while true do + let line = input_line stdin in + (try + let cmd = Parse.of_line ~multi_active:!in_multi line in + Dispatch.run cmd + with Parse.Parse_error msg -> + Wire.reply_error msg) done with | End_of_file -> () end; From 20c6076b554fed6d5c2c9e711e8a19745eac6505 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sun, 31 May 2026 07:47:08 +0200 Subject: [PATCH 08/10] [llm] diagnose missing-argument REPL commands at parse time 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) --- src/ecLlm.ml | 52 ++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 38 insertions(+), 14 deletions(-) diff --git a/src/ecLlm.ml b/src/ecLlm.ml index dc89c2a12..174734b4e 100644 --- a/src/ecLlm.ml +++ b/src/ecLlm.ml @@ -445,9 +445,10 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = let exception Trace_failed of exn in try + if args = "" then failwith "LOAD: missing filename"; (* Parse quoted or unquoted filename. *) let filename, rest = - if String.length args > 0 && args.[0] = '"' then + if args.[0] = '"' then let close = try String.index_from args 1 '"' with Not_found -> @@ -464,6 +465,7 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = | [f] -> (f, "") | f :: rest -> (f, String.concat " " rest) in + if filename = "" then failwith "LOAD: missing filename"; (* Parse optional LINE[:COL] and flags (-nosmt, -trace). *) let upto, nosmt, trace = @@ -732,10 +734,23 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = exception Parse_error of string - let rest n line = - String.strip (String.sub line n (String.length line - n)) + (* Match [kw] as a prefix: succeeds on exactly [kw] (no argument) + or [kw ^ " " ^ ...] (with argument), returning the stripped + argument tail. Returns [None] otherwise. This recognises both + "CHECKPOINT" and "CHECKPOINT foo" the same way, so we can + diagnose the missing-name case ourselves instead of falling + through to EC's parser. *) + let keyword_arg kw line = + if line = kw then Some "" + else if String.starts_with line (kw ^ " ") then + let n = String.length kw + 1 in + Some (String.strip + (String.sub line n (String.length line - n))) + else None let parse_focus arg = + if arg = "" then + raise (Parse_error "FOCUS: missing argument"); try Focus (int_of_string arg) with Failure _ -> raise (Parse_error @@ -746,7 +761,15 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = raise (Parse_error "CHECKPOINT: missing name"); Checkpoint name + let parse_revert spec = + if spec = "" then + raise (Parse_error + "REVERT: missing uuid or checkpoint name"); + Revert spec + let parse_search query = + if query = "" then + raise (Parse_error "SEARCH: missing query"); let query = if String.ends_with query "." then String.sub query 0 (String.length query - 1) @@ -754,6 +777,11 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = in Search query + let parse_load args = + (* [Load.handle] accepts an empty argument and reports a + specific error; keep that responsibility there. *) + Load args + let of_line ~multi_active (raw : string) : command = let line = String.strip raw in if multi_active then @@ -774,17 +802,13 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = | "NEXT" -> Next | "QUIET ON" -> Quiet true | "QUIET OFF" -> Quiet false - | _ when String.starts_with line "FOCUS " -> - parse_focus (rest 6 line) - | _ when String.starts_with line "CHECKPOINT " -> - parse_checkpoint (rest 11 line) - | _ when String.starts_with line "REVERT " -> - Revert (rest 7 line) - | _ when String.starts_with line "SEARCH " -> - parse_search (rest 7 line) - | _ when String.starts_with line "LOAD " -> - Load (rest 5 line) - | _ -> Ec line + | _ -> + match keyword_arg "FOCUS" line with Some a -> parse_focus a | None -> + match keyword_arg "CHECKPOINT" line with Some a -> parse_checkpoint a | None -> + match keyword_arg "REVERT" line with Some a -> parse_revert a | None -> + match keyword_arg "SEARCH" line with Some a -> parse_search a | None -> + match keyword_arg "LOAD" line with Some a -> parse_load a | None -> + Ec line end in (* ------------------------------------------------------------------ *) From 7ddb2ea227f485a11ccda7432bcff32c093a2fdc Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sun, 31 May 2026 08:00:48 +0200 Subject: [PATCH 09/10] [llm] nested TREE and dotted-path FOCUS 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. --- doc/llm/CLAUDE.md | 4 +- src/ecLlm.ml | 221 +++++++++++++++++++++++++++++++++++++--------- 2 files changed, 183 insertions(+), 42 deletions(-) diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index a06725467..1c215cd82 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -61,9 +61,9 @@ These are protocol-level commands, not EasyCrypt syntax: | `REVERT ` | Revert to a specific state (by uuid or checkpoint name) | | `GOALS` | Print the current goal (first subgoal only, with remaining count) | | `GOALS ALL` | Print all subgoals | -| `TREE` | List open subgoals as `[N] `, marking the focused one | +| `TREE` | List open subgoals with dotted-path labels showing nesting, marking the focused one | | `TREE ALL` | Same as `TREE`, but with full goal bodies | -| `FOCUS N` | Rotate focus so subgoal `[N]` (from `TREE`) becomes the focused goal | +| `FOCUS P` | Rotate focus to the leaf addressed by path `P` (`N` or `N1.N2.N3...`) | | `NEXT` | Rotate focus to the next subgoal (equivalent to `FOCUS 2`) | | `COMMIT` | Emit recorded REPL phrases as a bulleted proof body (works under `+strict_bullets`) | | `CHECKPOINT ` | Save current uuid under a name for later `REVERT` | diff --git a/src/ecLlm.ml b/src/ecLlm.ml index 174734b4e..9a7ce317c 100644 --- a/src/ecLlm.ml +++ b/src/ecLlm.ml @@ -146,14 +146,108 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = Format.pp_print_flush fmt (); Buffer.contents buf - (* Render the focus-tree of open subgoals. [all=false] gives a - one-line digest per goal; [all=true] gives the full goal body. *) - let tree_to_string ?(all=false) () = - let entries = EcCommands.pp_tree ~all () in - match entries with - | [] -> "No active proof.\n" - | _ -> - let buf = Buffer.create 256 in + (* Inline focus annotation ([focus: 1/N]) appended to reply tags + whenever the active proof has >=2 open subgoals. *) + let focus_tag () = + match EcCommands.pp_tree () with + | _ :: _ :: _ as entries -> + Printf.sprintf " [focus: 1/%d]" (List.length entries) + | _ -> "" + end in + + (* ------------------------------------------------------------------ *) + (* Frame tree: group currently-open goals by their shared multi-child + ancestors. Used by [Tree] (rendering) and [Focus] (path lookup). + The tree is a *derivation*: it depends only on [pr_opened] and + [parent_of], no recorded transcript. *) + let module FrameTree = struct + (* Internal nodes are split-point frames; leaves carry a handle + (the open goal), its index in [pr_opened] (1-based, used by + [EcCoreGoal.rotate_focus]), and its rendered text. *) + type node = + | Frame of node list (* >=2 child branches *) + | Leaf of + { idx : int (* 1-based in pr_opened *) + ; focused : bool (* idx = 1 *) + ; text : string } (* one-line conclusion *) + + (* Multi-child ancestors of [h], outermost first (= root-most + split first, deepest split last). This ordering means leaves + sharing the same OUTER frame will agree on the chain's first + element, which is what [group] partitions on. *) + let split_chain h = + let rec walk h acc = + match EcCommands.parent_of h with + | None -> acc + | Some p -> + match EcCommands.children_of p with + | [_] -> walk p acc + | _ -> walk p (p :: acc) + in + (* [walk] prepends each ancestor as we go up; the result has + outermost at the FRONT (we add it last). No reverse needed. *) + walk h [] + + (* Build the tree by grouping leaves with a common ancestor prefix. + [leaves] is a list of (chain, leaf) in [pr_opened] order. The + grouping is done recursively on the head of each chain. *) + let rec group (leaves : (EcCoreGoal.handle list * node) list) : node list = + let rec runs acc = function + | [] -> List.rev acc + | (chain, leaf) :: rest -> + match chain with + | [] -> runs (`Bare leaf :: acc) rest + | hd :: tl -> + let same_head, others = + List.partition_map (fun (c, l) -> + match c with + | h :: tail when EcCoreGoal.eq_handle h hd -> + Left (tail, l) + | _ -> Right (c, l)) + rest + in + runs (`Group ((tl, leaf) :: same_head) :: acc) others + in + List.map + (function + | `Bare leaf -> leaf + | `Group children -> Frame (group children)) + (runs [] leaves) + + (* Strip leading singleton frames so the top-level forest's + indices match what the user thinks of as "top-level subgoals + of the current frame." When all open leaves descend from a + single outermost split, the top-level forest has one Frame + containing the actual user-visible siblings; unwrap it. *) + let rec unwrap forest = + match forest with + | [Frame children] -> unwrap children + | _ -> forest + + let build () = + let handles = EcCommands.open_handles () in + let texts = EcCommands.pp_tree () in + if handles = [] then [] + else + let leaves = + List.mapi (fun i (h, (_, focused, text)) -> + let leaf = Leaf { idx = i + 1; focused; text } in + (split_chain h, leaf)) + (List.combine handles texts) + in + unwrap (group leaves) + + (* Render the tree with dotted-path labels matching what FOCUS + accepts. [all] requests full goal bodies (we re-query via + [pp_tree ~all:true] keyed by leaf index). *) + let render ?(all=false) () = + let forest = build () in + if forest = [] then "No active proof.\n" + else + let texts_all = + if all then Some (EcCommands.pp_tree ~all:true ()) + else None + in let one_line s = let s = match String.index_opt s '\n' with @@ -165,26 +259,61 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = then String.sub s 0 (limit - 1) ^ "…" else s in - List.iter (fun (i, focused, text) -> - let marker = if focused then " <- focused" else "" in - if all then - Buffer.add_string buf - (Printf.sprintf "[%d]%s\n%s\n" i marker text) - else - Buffer.add_string buf - (Printf.sprintf "[%d] %s%s\n" i (one_line text) marker) - ) entries; + let buf = Buffer.create 256 in + let rec emit ~depth ~path = function + | Leaf { idx; focused; text } -> + let label = String.concat "." (List.rev_map string_of_int path) in + let marker = if focused then " <- focused" else "" in + for _ = 1 to depth do Buffer.add_string buf " " done; + (match texts_all with + | None -> + Buffer.add_string buf + (Printf.sprintf "[%s] %s%s\n" + label (one_line text) marker) + | Some entries -> + let (_, _, full) = + List.nth entries (idx - 1) + in + Buffer.add_string buf + (Printf.sprintf "[%s]%s\n%s\n" label marker full)) + | Frame children -> + List.iteri (fun i child -> + emit ~depth:(depth + 1) ~path:((i + 1) :: path) child) + children + in + List.iteri (fun i node -> + emit ~depth:0 ~path:[i + 1] node) + forest; Buffer.contents buf - (* Inline focus annotation ([focus: 1/N]) appended to reply tags - whenever the active proof has >=2 open subgoals. *) - let focus_tag () = - match EcCommands.pp_tree () with - | _ :: _ :: _ as entries -> - Printf.sprintf " [focus: 1/%d]" (List.length entries) - | _ -> "" + (* Resolve a dotted path against the tree. Returns [Ok idx] where + [idx] is the 1-based position in [pr_opened] of the selected + leaf, or [Error msg]. *) + let resolve_path (path : int list) : (int, string) result = + let forest = build () in + let rec walk ~components nodes = + match components with + | [] -> Error "FOCUS: path must select a leaf goal" + | k :: rest -> + if k < 1 || k > List.length nodes then + Error (Printf.sprintf + "FOCUS: index %d out of range (1..%d)" + k (List.length nodes)) + else + match List.nth nodes (k - 1), rest with + | Leaf { idx; _ }, [] -> Ok idx + | Leaf _, _ -> + Error "FOCUS: path overshoots a leaf goal" + | Frame _, [] -> + Error "FOCUS: path must select a leaf goal, \ + not a frame" + | Frame kids, _ -> walk ~components:rest kids + in + if forest = [] then Error "FOCUS: no active proof" + else walk ~components:path forest end in + (* ------------------------------------------------------------------ *) (* OK/ERROR/ wire envelope. *) let module Wire = struct @@ -719,7 +848,7 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = | Goals of [`One | `All] | Tree of [`One | `All] | Commit - | Focus of int + | Focus of int list (* dotted path; [k] = "FOCUS k" *) | Next | Checkpoint of string | Revert of string (* uuid-or-name; Dispatch resolves *) @@ -751,10 +880,17 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = let parse_focus arg = if arg = "" then raise (Parse_error "FOCUS: missing argument"); - try Focus (int_of_string arg) - with Failure _ -> + let parts = String.split_on_char '.' arg in + let path = + try List.map int_of_string parts + with Failure _ -> + raise (Parse_error + (Printf.sprintf "FOCUS: not a path of integers: %s" arg)) + in + if List.exists (fun k -> k < 1) path then raise (Parse_error - (Printf.sprintf "FOCUS: not an integer: %s" arg)) + (Printf.sprintf "FOCUS: path indices must be >= 1: %s" arg)); + Focus path let parse_checkpoint name = if name = "" then @@ -845,19 +981,24 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = Wire.reply_error "nothing to undo" let do_focus_request request = - (* [request] is the user's intent normalized; [`Next] is "second - sibling unless only one open". *) + (* [request] is the user's intent normalized: + - [`Next] = rotate to the second open goal (or stay if <=1) + - [`Path p] = resolve dotted path [p] against the frame tree + and focus the matching leaf. *) Buffer.clear notices; - let entries = EcCommands.pp_tree () in - let n = List.length entries in - let target = + let resolved = match request with - | `Next -> if n <= 1 then 1 else 2 - | `At k -> k + | `Next -> + let n = List.length (EcCommands.open_handles ()) in + Ok (if n <= 1 then 1 else 2) + | `Path path -> FrameTree.resolve_path path in - match EcCommands.focus_goal target with - | Ok _ -> Wire.reply_ok_goals () + match resolved with | Error msg -> Wire.reply_error msg + | Ok target -> + match EcCommands.focus_goal target with + | Ok _ -> Wire.reply_ok_goals () + | Error msg -> Wire.reply_error msg let do_checkpoint name = Buffer.clear notices; @@ -923,14 +1064,14 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = Wire.reply_ok (Goals.goals_to_string ~all:true ()) | Tree `One -> Buffer.clear notices; - Wire.reply_ok (Goals.tree_to_string ()) + Wire.reply_ok (FrameTree.render ()) | Tree `All -> Buffer.clear notices; - Wire.reply_ok (Goals.tree_to_string ~all:true ()) + Wire.reply_ok (FrameTree.render ~all:true ()) | Commit -> Buffer.clear notices; Wire.reply_ok (Commit.proof_text ()) - | Focus k -> do_focus_request (`At k) + | Focus path -> do_focus_request (`Path path) | Next -> do_focus_request `Next | Checkpoint n -> do_checkpoint n | Revert s -> do_revert s From b1890de3909e9cc354038f5c9e6869f58e6b592b Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sun, 31 May 2026 19:51:21 +0200 Subject: [PATCH 10/10] [llm] update CLAUDE.md with current workflow status 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. --- doc/llm/CLAUDE.md | 72 ++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 68 insertions(+), 4 deletions(-) diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index 1c215cd82..f18137631 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -177,7 +177,69 @@ REVERT before_split apply H. ← try a different approach ``` -**4. Use QUIET mode to save tokens during bulk tactic application:** +**4. Inspect and navigate nested subgoals with `TREE` and `FOCUS`:** + +When a tactic opens multiple subgoals, the engine focuses the first +one. By default subsequent tactics act on it; siblings wait their +turn. Use `TREE` to see the structure, including nested splits: + +``` +TREE +→ OK [uuid:N] + [1.1.1] x = 0 <- focused + [1.1.2] y = 1 + [1.2] z = 2 +[2] w = 3 + +``` + +The labels are dotted paths. `FOCUS P` rotates focus to the leaf at +path `P`: + +``` +FOCUS 1.2 ← work on `z = 2` +FOCUS 2 ← work on `w = 3` +FOCUS 1.1.1 ← back to `x = 0` +``` + +`FOCUS k` (a single integer) targets the k-th open goal in the flat +listing. `NEXT` is shorthand for `FOCUS 2`. Selecting an internal +frame errors (`FOCUS: path must select a leaf goal, not a frame`). + +Replies carry a `[focus: k/N]` tag when more than one goal is open +(e.g. `OK [uuid:42] [focus: 1/3]`) so you always know which goal the +next tactic will hit. **TREE labels are not stable across focus +changes** — `FOCUS 1.2` from one state may name a different goal in +another, because the tree always shows the focused goal first. + +**5. Build a `+strict_bullets`-friendly proof with `COMMIT`:** + +The REPL records every successful interactive phrase. `COMMIT` walks +the proof DAG and emits the recorded tactics with bullets inserted +at every multi-child split. The output is a proof body that compiles +under `pragma +strict_bullets`: + +``` +LOAD "myfile.ec" 42 +split. +- rewrite H. trivial. ← REPL accepts the unbulleted form +- exact hq. +COMMIT +→ OK [uuid:N] +split. +- rewrite H. trivial. +- exact hq. + +``` + +Bullet characters cycle through `-`, `+`, `*`, `--`, `++`, `**`, ... +and are chosen to avoid colliding with any frames the LOAD prefix +already opened. Use `COMMIT` once the proof is complete (or at any +checkpoint) and paste the result back into the source file. + +`UNDO` / `REVERT` trim the COMMIT transcript automatically. + +**6. Use QUIET mode to save tokens during bulk tactic application:** ``` QUIET ON @@ -188,7 +250,7 @@ QUIET OFF GOALS ``` -**5. Search for lemmas using patterns:** +**7. Search for lemmas using patterns:** EasyCrypt `search` uses pattern syntax, not keywords. Use `_` as wildcard: @@ -267,8 +329,10 @@ SEARCH (_ %/ _) - `by` closes **all** remaining subgoals. If it fails, the error refers to the first unclosed goal, which may not be the intended one. -- When a tactic generates multiple subgoals, each subgoal must be - closed in order. Use `GOALS ALL` or `TREE` to see them all. +- When a tactic generates multiple subgoals, the engine focuses the + first one. Address them in any order via `FOCUS path`, or in the + default order by closing each in turn. Use `TREE` or `GOALS ALL` + to see what's open. - When more than one subgoal is open, replies carry a `[focus: k/N]` tag (e.g. `OK [uuid:42] [focus: 1/3]`) so you know which one the next tactic will hit.