The agent that never called the server
In July a Claude Code session working in
ualib/agda-algebras formalized about
1200 lines of literate Agda, ran fifteen or so typecheck iterations and four
full-library builds, and never once called the Agda server I had built for
exactly that job. The server was configured. Its four tools were listed in
front of the model on every turn. The session used agda from a shell prompt
instead, every single time.
The session wrote its own post-mortem, and that document turned out to be the design record. Four of the rules the server now runs on are in it, and each one is a defect I could name rather than a principle I liked. The project page has the artifacts and the current numbers.
What the post-mortem actually said¶
The report reconstructs the decision an agent makes at each check, and its first line is the whole thing: "a verdict I cannot trust costs more than no verdict". If the server can report green while the project's own gate fails, the real checker has to run anyway and the call was pure overhead. "Trust is the whole product," it says, and everything else in the document is filed as secondary to it.
Four more reasons follow, in descending order of how much they hurt. The edit
unit was a whole module, 200 to 900 lines drafted and then checked, and for that
loop agda <file> in one call is already minimal. Every module in that
repository is literate Agda, so if holes are unreliable in .lagda.md files
then the two tools with no shell equivalent are unavailable exactly where the
work is. The
questions it actually had were about scope and not about goals, about a dozen of
them answered by grep. And it could not tell what the server was doing:
which flags, the same library file as the project's own gate, a warm process or
a cold start, whether it saw the bytes just written.
The document asked to be doubted. Its own opening section grades every claim by
provenance, marks three as secondhand or inferred, and says plainly that each one
should be re-tested against the server before anything is filed. So I re-tested
them: one scripted session of a dozen calls over five fixtures against a pinned
commit, with every server verdict cross-checked against a direct agda run.
That step changed the plan, and it is the part I would keep if I kept nothing else.
The verdict is the exit code, and it says so¶
The report's headline claim was that check_file reported green on a module
carrying unsolved metavariables. It does not, and it never did: the server
shells out to a batch agda process per call, so it was strict from the start.
The inferred cause in the report, that the server ran Agda's interaction mode
where unsolved goals are not errors, was wrong too.
The trust failure was real anyway, one tool over. fill_hole answered
status: "ok" for a candidate that left an unsolved implicit argument, while
agda on byte-identical content exited 42. The cause was a tolerance check
meant to excuse the file's other open holes, written as a blacklist: a
non-zero exit was reported as success if the output mentioned open holes and did
not mention any of four named error tags. [UnsolvedMetaVariables] was not
one of the four, so an error nobody had thought of was an error nobody caught.
That is exactly the failure the report described, at a tool the report never
accused, and I would not have found it by reading the accusation.
The fix was to turn the list around. A blacklist fails open on everything its
author did not anticipate, which for a trust boundary is the wrong direction;
the check is now a whitelist, and a non-zero exit is success only when every
error Agda reported is the [UnsolvedInteractionMetas] of holes still open in
the file, including any sub-hole the candidate itself introduced, which is a
refinement rather than a failure. Anything else fails closed, including an
unrecognized error class and a failure whose output carries no error header the
parser recognizes at all.
It is worth being exact about what that makes the verdict, because the tidy
version of the sentence is wrong. For check_file and get_diagnostics,
success is the exit code and nothing else. For fill_hole it is the exit code
plus that one classification, and the classification can only ever withhold
success: the tolerated case is "there are still holes here", which is not a
proof of anything and never turns a failing build green.
The other half of that fix was not code. An agent picks a tool by reading its
one-line description and nothing else, and those descriptions did not say the
one thing that mattered, which is whether green means the build passes. Every
response that makes a checking judgment now carries the exact agda command it
is equivalent to, the exit code it was derived from, and a sentence saying what
green means, so a client can check a claim instead of trusting it. A response
that makes no judgment carries no verdict at all, which is the other half of the
same rule and is the shape at the end of this post. A later session used that echo to quote a
check in a pull request body "as a checkable claim rather than an assertion",
which is not a use I had designed for and is the one I am most pleased about.
A hole is whatever Agda thinks is a hole¶
Hole detection matched the literal four-character token {!!}. Agda's other
spellings, {! !} and {! e !} and a bare ?, were invisible. A fixture with
four holes Agda could see reported two, one of which was a {!!} written inside
a header comment, so "the first hole" addressed a comment. A
.lagda.md file whose only hole was {! zero !} reported no holes at all,
while get_diagnostics on the same file reported the unsolved interaction meta
that hole was causing.
The one that stopped me was fill_hole on a {!!} that appeared in a markdown
paragraph. It returned ok. The substituted text was invisible to Agda, the
file's real hole was excused by the tolerance heuristic above, and an agent
acting on that verdict would have edited its own documentation in the belief
that it had made progress on a proof.
The fix was to stop approximating. The server now ports Agda 2.8.0's literate preprocessor and a model of its lexer: every hole syntax including nesting, no hole inside a comment or a pragma or a string literal or literate prose, every literate flavor masked to its code regions, and all positions in the coordinates of the file as written rather than of some extracted code view. Parity tests hold that scan to batch Agda and to the interaction protocol's own list of interaction points across the whole fixture matrix, because this is a component that was wrong for months while looking right.
A diagnostic is data¶
Every error came back as prose. One UnsolvedConstraints message ran about
twenty lines of internal metavariable names before reaching anything useful. A
model can read that. What it does with it is paraphrase it, and paraphrase is
the step where a diagnosis turns into a guess.
Re-testing found something worse underneath: no diagnostic carried a position at
all. The extractor expected Agda's older file:10,5-15 spelling, and Agda 2.8.0
emits file:9.12-13. Every error in the session had arrived with a severity
and a message and no line number at all, and that had gone unnoticed.
Diagnostics now come back as data beside the prose: Agda's own bracketed code,
a one-based range in the file as written, the full message body bounded and
with the elision stated, and a payload that varies by code (expected and actual
types, did-you-mean candidates, each unsolved meta with its type). They are
ordered most-likely-root-cause first, so the ModuleDoesntExport warning comes
before the NotInScope error it caused, and the list is capped with the
pre-cap total reported.
The payoff shows up in the field reports as a change of tempo rather than of capability. Six errors in a 737-line module, each localized on the first read. A fixity bug that was "a ten-second read" from the expected and actual fields. An unsolved-metas payload whose types showed that the metas were the proof components of an implicit record argument, a known disease in this codebase, identified in one read where raw batch output smears the same information across a hundred lines.
A handle that does not move¶
Holes were addressed by a zero-based index. Indices shift whenever an earlier hole is filled or any hole is added, so a multi-hole edit becomes bookkeeping, which is precisely the state an agent loses between calls. Phantom matches made it worse: the token in the header comment was hole 0, so the real hole was hole 1.
Holes are now addressed by position, and every answer re-anchors the client. Here is the response to a candidate that refines rather than closes, captured from the live server and trimmed to the fields at issue:
{
"candidate": "lemma {!!} {!!}",
"status": "ok",
"remainingHoles": 2,
"holes": [
{"index": 0, "line": 26, "col": 14, "goal": "?"},
{"index": 1, "line": 26, "col": 19, "goal": "?"}
],
"elapsedMs": 220
}
The hole list describes the file as that candidate would leave it, not as it is on disk, which the server has already restored. One accepted candidate, two new obligations, both already addressed. The search loop built on this server adopts that list wholesale rather than computing hole positions itself, so client-side arithmetic cannot drift from Agda's, and there is nothing to reconcile when a splice moves a line.
The rule underneath all four¶
Say what an answer's source is, and prefer Agda's. In the server's own words,
answer = whatAgdaSaid <|> whatWeDerived: when Agda can answer a question, in
output a call already captured or through a query, Agda's answer is the
authority, and anything derived from source text is a pre-flight approximation
and a fallback.
The clearest case is a small one. get_goal used to scan the file for its
module line, so a literate file whose prose happened to begin a line with the
word "module" was reported under the prose's name. Agda had printed the true
answer in the same run, in the Checking M (path). line the call already had in
hand. And Agda's answer is better than a correct scan's would be: it is the
name Agda resolved, AnonModule for an anonymous header or the full
hierarchical name for a nested one, where a scan can only repeat what the header
claims. The difference between those two strings is a diagnosis.
The same rule is why the server runs Agda in two lanes and lets only one of them judge, and why a query answered from the fast lane carries no verdict at all:
Knowledge and verdicts are different kinds of thing, and a response that does not say which it is holding is an invitation to treat one as the other.
What the record says now, including what it says against me¶
Nine sessions since have used the server as a working instrument, in
agda-algebras and in a second, unrelated project, and the honest summary is
narrower than I would have written in advance.
Warm checks run 2 to 35 seconds against 20 seconds to ten minutes for the shell equivalent, and that is most of the value: the loop becomes typecheck after every block instead of twice a day. Structured diagnostics are the rest of it. The per-call project resolution, which walks up to the nearest library file and echoes what it found, is named in eight of the nine reports as the reason a verdict from another worktree could be trusted at all.
Against that: hole-driven development went almost unused, and the reports argue that this was right rather than an adoption failure. When an agent can read the relevant sources into context and design a proof whole, write-then-check wins, and holes pay when the goal types are genuinely unknown. One session's summary of a refactor says the server "was a wash against the CLI on the type-checking side and absent on the profiling side", with its single real save being the confirmation of which tree it was checking. Another notes that a nine-file sweep was better as a shell loop. I would rather have those sentences in the record than a cleaner story.
The substitution of reading for asking has a ceiling, though, and it is the
library's size. An audit of one session found most of its time spent finding
what the library already contained and what it was called, with more such
questions than proof obligations, all of them answered by grep. The agent
knows the type and not the name, which is the one question text search cannot
answer. Retrieval is what that argues for, and
what happened when I measured it
was not what I expected.