Fix #89 (review's local toolset) and #102 (spec_agent taught the wrong DSL entirely) - #103
Merged
Merged
Conversation
…g DSL entirely) ## #89: review_dynamic_tools() review.lex's ollama_agent()/litellm_agent() used the same shared dynamic_tools() as every other local-model mode, which never included attestation_query/effects_of/lex_audit/sigid_lookup — the four tools review.lex's own prompt is built around ("Attestation is the trust anchor here, not your own reading"). Confirmed live: five straight "unknown tool: effects_of" failures in yesterday's pipeline audit. Unlike lex_test (a single narrow gap, fixed in #100 by adding it to the shared minimal_tools()), these four are review-specific and would bloat every other mode's toolset if added there — so this adds review_dynamic_tools() = dynamic_tools() + the four review tools, and switches only review's two local variants to use it. ## #102: spec_agent.lex was teaching a fictional Spec format The real bug, found by reading lex-lang's spec-checker crate (crates/spec-checker) directly: `lex spec check <spec-file> --source <lex-file>` (what the lex_spec_check tool literally shells out to) reads spec files in spec-checker's own textual DSL — spec clamp { forall x :: Int, lo :: Int, hi :: Int where lo <= hi: let r := clamp(x, lo, hi) (r >= lo) and (r <= hi) } — verified against examples/agent_merge/clamp.spec, a real, working example already in the lex-lang repo. spec_agent.lex's prompt taught none of this. It described specs as Lex *values* of type `{ name, quantifiers, predicate }` with predicate :: (...) -> Bool — a closure-based lookalike that isn't lex-spec's Spec type (predicate is a SpecExpr AST node, not a Lex function — it has to be, since the same spec gets randomly tested AND exported to SMT-LIB, which needs to inspect its structure) and isn't spec-checker's DSL either. Every spec mode run today wrote this fictional shape, which is exactly why lex_spec_check's real args (`spec`, `source`) always came back as "missing field": the tool was never going to accept what the prompt taught it to produce. Rewrote the prompt to teach the actual DSL — grammar, operators, the verified clamp example, and the real lex_spec_check(spec, source) call shape — and corrected the workflow (write a .spec file, not a .lex Spec record; lex_check doesn't apply to .spec files; Proved by lex_spec_check is the actual completion signal, not lex_check passing on the wrong kind of file). **Live-verified, not just type-checked**, against litellm/qwen3.8:27b-mlx, mode=spec, on a fresh clamp() function: - First attempt: wrote fully correct, genuinely-Proved .spec content on the first try (independently re-verified with `lex spec check` myself) — but the model wrote the file and assumed a "grading harness" would run lex_spec_check, without calling the tool itself. - Strengthened the WORKFLOW/WHEN YOU ARE DONE sections to make "you must call the tool yourself, nothing verifies it for you" explicit. - Second attempt: model called lex_spec_check itself, got a genuine Proved result, reported it accurately — independently re-verified again, same spec, same result. lex check --strict, lex fmt --check, lex test, and the bar-mode gate are all green. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #89, closes #102.
#89:
review_dynamic_tools()review.lex's local variants used the same shareddynamic_tools()asevery other mode, which never included
attestation_query/effects_of/lex_audit/sigid_lookup— the four tools review's own prompt is builtaround. Confirmed live: five straight
"unknown tool: effects_of"failures in the pipeline audit that surfaced this. Added
review_dynamic_tools()scoped to review's two local variants only, soother modes' toolsets are untouched.
#102:
spec_agent.lexwas teaching a fictional Spec formatTraced the real contract by reading
lex-lang'sspec-checkercratedirectly:
lex spec check <spec-file> --source <lex-file>readsspec-checker's own textual DSL, verified against a real working example
already in that repo (
examples/agent_merge/clamp.spec).spec_agent.lextaught something else entirely — Lex values of type
{ name, quantifiers, predicate :: (...) -> Bool }— which is neitherthis DSL nor
lex-spec's ownSpec/SpecExprAST type (the realpredicatehas to be a data structure, not a closure, since the samespec gets randomly tested and exported to SMT-LIB). Every spec-mode run
was writing something the tool could never accept.
Rewrote the prompt with the real grammar, the verified example, and the
correct
lex_spec_check(spec, source)call shape.Live-verified twice against litellm/qwen3.8:27b-mlx on a fresh
clamp():.speccontent on the first try(independently re-checked with
lex spec checkmyself) — but the modelwrote the file and assumed something else would verify it, without
calling the tool.
WORKFLOW/WHEN YOU ARE DONEto make "you call the toolyourself, nothing does it for you" explicit.
lex_spec_checkitself, got a real Provedresult, reported it accurately — independently re-checked again, same
result.
lex check --strict,lex fmt --check,lex test, and the bar-modegate are all green.
Co-Authored-By: Claude Sonnet 5 noreply@anthropic.com