|
| 1 | +#!/usr/bin/env python3 |
| 2 | +""" |
| 3 | +Fifo-backed daemon exposing one persistent `easycrypt llm` instance to many |
| 4 | +shell callers. Typical use case: an LLM agent (Claude Code, etc.) that |
| 5 | +invokes a bash tool *once per tactic* — the agent can't hold stdin/stdout |
| 6 | +open across turns, so without a daemon every tactic would re-LOAD the |
| 7 | +whole file prefix. |
| 8 | +
|
| 9 | +Protocol (matches the JSON line format produced by `ec_send.sh`): |
| 10 | +
|
| 11 | + request (one line on stdin-fifo): |
| 12 | + {"op": "<op>", "arg": "...", "arg2": "...", "nosmt": bool} |
| 13 | +
|
| 14 | + response (one line on stdout-fifo): |
| 15 | + {"ok": bool, "uuid": N, "resp": "..."} |
| 16 | +
|
| 17 | +Supported ops: |
| 18 | + load arg=path, arg2=line (string or int), optional nosmt: bool |
| 19 | + tactic arg="proc." |
| 20 | + tactic_multiline arg="<multi-line body>" (wraps in <BEGIN>/<DONE>) |
| 21 | + undo |
| 22 | + revert arg="<uuid-or-name>" |
| 23 | + checkpoint arg="<name>" |
| 24 | + goals |
| 25 | + goals_all |
| 26 | + search arg="<pattern>" |
| 27 | + quiet arg="on"|"off" |
| 28 | + close |
| 29 | +
|
| 30 | +Usage: |
| 31 | + # start daemon (in background) |
| 32 | + python3 scripts/llm/daemon.py --cwd /path/to/project \\ |
| 33 | + --in-fifo /tmp/ec_in --out-fifo /tmp/ec_out & |
| 34 | +
|
| 35 | + # then drive with scripts/llm/ec_send.sh (see that file for details) |
| 36 | +
|
| 37 | +The fifos are created if they don't exist. Only one connected writer and |
| 38 | +one connected reader are expected at a time — the client (`ec_send.sh`) |
| 39 | +enforces this by opening them sequentially. |
| 40 | +""" |
| 41 | + |
| 42 | +import argparse |
| 43 | +import json |
| 44 | +import os |
| 45 | +import sys |
| 46 | +import traceback |
| 47 | + |
| 48 | +HERE = os.path.dirname(os.path.abspath(__file__)) |
| 49 | +sys.path.insert(0, HERE) |
| 50 | +from ec_llm import ECLLM # noqa: E402 |
| 51 | + |
| 52 | + |
| 53 | +def _ensure_fifo(path): |
| 54 | + if not os.path.exists(path): |
| 55 | + os.mkfifo(path) |
| 56 | + elif not os.path.exists(path): # raced out; recreate |
| 57 | + os.mkfifo(path) |
| 58 | + |
| 59 | + |
| 60 | +def _handle(req, ec): |
| 61 | + op = req.get("op") |
| 62 | + arg = req.get("arg", "") |
| 63 | + arg2 = req.get("arg2", "") |
| 64 | + |
| 65 | + if op == "load": |
| 66 | + ok, resp = ec.load(arg, int(arg2), nosmt=bool(req.get("nosmt", False))) |
| 67 | + elif op == "tactic": |
| 68 | + ok, resp = ec.tactic(arg) |
| 69 | + elif op == "tactic_multiline": |
| 70 | + ok, resp = ec.tactic_multiline(arg) |
| 71 | + elif op == "undo": |
| 72 | + ok, resp = ec.undo() |
| 73 | + elif op == "revert": |
| 74 | + ok, resp = ec.revert(arg) |
| 75 | + elif op == "checkpoint": |
| 76 | + ok, resp = ec.checkpoint(arg) |
| 77 | + elif op == "goals": |
| 78 | + resp, ok = ec.goals(), True |
| 79 | + elif op == "goals_all": |
| 80 | + resp, ok = ec.goals_all(), True |
| 81 | + elif op == "search": |
| 82 | + resp, ok = ec.search(arg), True |
| 83 | + elif op == "quiet": |
| 84 | + ok, resp = ec.quiet(on=(arg.lower() == "on")) |
| 85 | + elif op == "close": |
| 86 | + ec.close() |
| 87 | + return {"ok": True, "uuid": ec.uuid, "resp": "bye"}, True |
| 88 | + else: |
| 89 | + return {"ok": False, "uuid": ec.uuid, "resp": f"unknown op: {op}"}, False |
| 90 | + |
| 91 | + return {"ok": ok, "uuid": ec.uuid, "resp": resp}, False |
| 92 | + |
| 93 | + |
| 94 | +def main(): |
| 95 | + p = argparse.ArgumentParser(description=__doc__.splitlines()[1]) |
| 96 | + p.add_argument("--cwd", default=None, help="Project root (default: cwd)") |
| 97 | + p.add_argument("--in-fifo", default="/tmp/ec_in", help="Request fifo path") |
| 98 | + p.add_argument("--out-fifo", default="/tmp/ec_out", help="Response fifo path") |
| 99 | + p.add_argument("--log", default="/tmp/ec_daemon.log", help="Log file") |
| 100 | + p.add_argument("--prover", default=None, help="SMT prover (e.g. Z3)") |
| 101 | + p.add_argument("--timeout", type=int, default=None, help="Per-goal SMT timeout (s)") |
| 102 | + args = p.parse_args() |
| 103 | + |
| 104 | + _ensure_fifo(args.in_fifo) |
| 105 | + _ensure_fifo(args.out_fifo) |
| 106 | + |
| 107 | + extra = [] |
| 108 | + if args.prover: |
| 109 | + extra += ["-p", args.prover] |
| 110 | + if args.timeout is not None: |
| 111 | + extra += ["-timeout", str(args.timeout)] |
| 112 | + |
| 113 | + ec = ECLLM(cwd=args.cwd, extra_args=extra) |
| 114 | + with open(args.log, "w") as lf: |
| 115 | + lf.write(f"EC started. uuid={ec.uuid}\n") |
| 116 | + |
| 117 | + while True: |
| 118 | + try: |
| 119 | + # Opening a fifo for reading blocks until a writer opens it. |
| 120 | + with open(args.in_fifo, "r") as fi: |
| 121 | + line = fi.readline() |
| 122 | + if not line.strip(): |
| 123 | + continue |
| 124 | + req = json.loads(line) |
| 125 | + result, should_exit = _handle(req, ec) |
| 126 | + with open(args.out_fifo, "w") as fo: |
| 127 | + fo.write(json.dumps(result) + "\n") |
| 128 | + if should_exit: |
| 129 | + break |
| 130 | + except Exception: |
| 131 | + with open(args.log, "a") as lf: |
| 132 | + lf.write("EXCEPTION: " + traceback.format_exc() + "\n") |
| 133 | + try: |
| 134 | + with open(args.out_fifo, "w") as fo: |
| 135 | + fo.write(json.dumps({"ok": False, "uuid": -1, |
| 136 | + "resp": traceback.format_exc()}) + "\n") |
| 137 | + except Exception: |
| 138 | + pass |
| 139 | + |
| 140 | + |
| 141 | +if __name__ == "__main__": |
| 142 | + main() |
0 commit comments