[agda-mcp] get_goal/fill_hole: typecheck in place so library-embedded modules resolve (#66)#67
Conversation
…resolve (#66) get_goal and fill_hole copied the target file to a scratch directory before typechecking. That works for flat, top-level modules (the benchmark fixtures) but for a module embedded in a library at a hierarchical path — e.g. FLRP.Bridge at src/FLRP/Bridge.lagda.md in agda-algebras — the copy collides with the module's canonical file once the library's src root is on the include path, and Agda rejects it with ModuleDefinedInOtherFile. check_file and get_diagnostics were unaffected because they already load in place. Typecheck get_goal and fill_hole in place too, mirroring check_file's include strategy, with the source patched transiently and restored under bracket_ — the original bytes are written back even if Agda errors or the call is interrupted. get_goal also ensures `open import AgdaDojang.Debug` is in scope, injecting it after the module header when absent. The check for an existing import and the header search both look at real import/module lines, so a passing mention in a comment neither suppresses nor misplaces the injection, and parameterised (multi-line) module headers are handled. The old temp-copy machinery (makeTmpDir / makeOverlay / stripIncludeDir) is removed, which also makes #43 moot for these two tools. Adds a regression fixture — a two-directory mini-library whose hierarchically named module imports across directories and does not import AgdaDojang.Debug — and five tier-2 tests: get_goal returns a goal with the local variable in context, fill_hole accepts a cross-directory term and rejects an ill-typed one, and the source is byte-for-byte unchanged afterwards. 42/42 tests pass. Closes #66. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011ZxeUxJHyQsF9p2DjpCHct
There was a problem hiding this comment.
Pull request overview
This PR updates agda-mcp’s proof-state tools so get_goal and fill_hole typecheck the target file in place (matching check_file / get_diagnostics), fixing failures on hierarchically-named, library-embedded modules (issue #66). It also adds a small regression “mini library” fixture plus tier-2 integration tests, and updates the README to document the new in-place architecture.
Changes:
- Make
get_goal/fill_holetransiently patch and restore the real source file and run Agda against the real path, avoiding scratch-copy module-collision errors. - Add tier-2 regression tests + a committed hierarchical fixture library (
hier-lib) that imports across sibling directories and omitsAgdaDojang.Debug. - Document the in-place typechecking approach in
agda-mcp/README.md.
Reviewed changes
Copilot reviewed 6 out of 6 changed files in this pull request and generated 7 comments.
Show a summary per file
| File | Description |
|---|---|
| agda-mcp/src/AgdaMCP/Tools/ProofState.hs | Switch get_goal / fill_hole to in-place patching via bracket_, add Debug-import injection and module-header parsing helpers, and remove temp-overlay machinery. |
| agda-mcp/test/Main.hs | Extend tier-2 subprocess tests with an issue #66 regression suite using the hierarchical fixture; adjust env probing to pass repo root. |
| agda-mcp/README.md | Update tool “how it works” notes and add an architecture note explaining in-place typechecking and why scratch copies fail for library modules. |
| agda-dojang/data/fixtures/hier-lib/src/Widgets/Thing.agda | Add cross-directory dependency module used by the hierarchical regression fixture. |
| agda-dojang/data/fixtures/hier-lib/src/Proofs/Use.agda | Add hierarchical module-with-hole fixture that imports Widgets.Thing and intentionally omits AgdaDojang.Debug. |
| agda-dojang/data/fixtures/hier-lib/hier-lib.agda-lib | Add minimal .agda-lib descriptor for the hierarchical regression fixture. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| isDebugImportLine ln = | ||
| let s = T.stripStart ln | ||
| in ("open" `T.isPrefixOf` s || "import" `T.isPrefixOf` s) | ||
| && "AgdaDojang.Debug" `T.isInfixOf` ln |
There was a problem hiding this comment.
Good catch — fixed in 4157e55. isDebugImportLine no longer does a whole-line substring scan. It now tokenizes the line (after stripping any -- comment) and requires the first token to be an import keyword (import/open/private) and AgdaDojang.Debug to appear as a whole token. So AgdaDojang.Debug.Extra is no longer mistaken for the module, private open import AgdaDojang.Debug is recognized, and a comment mention (or an inline -- … AgdaDojang.Debug trailer) does not count. Added pure unit tests for each of these cases, so the module comment and the code now agree.
Generated by Claude Code
| i <- findIndex (\l -> "module" `T.isPrefixOf` T.stripStart l) ls | ||
| jRel <- findIndex (\l -> "where" `elem` T.words l) (drop i ls) | ||
| pure (splitAt (i + jRel + 1) ls) |
There was a problem hiding this comment.
Fixed in 4157e55. splitAfterModuleHeader now strips the -- line comment from each line before scanning for the where token, so a where sitting inside a comment on a parameterised (multi-line) header no longer terminates the header early. Added a unit test with -- a level where needed on a header line that asserts the injected import lands after the real where, with the header block left intact. (Block comments {- … -} spanning a header are still a documented best-effort gap in stripLineComment.)
Generated by Claude Code
| -- get_goal and fill_hole must still alter the source (inject the reporting macro, | ||
| -- or substitute a candidate), so they patch the real file transiently and restore | ||
| -- it under 'Control.Exception.bracket_' — the original bytes are written back even | ||
| -- if Agda errors or the call is interrupted. |
There was a problem hiding this comment.
Addressed in 4157e55 by making the claim true rather than softening it. get_goal/fill_hole now capture the original with Data.ByteString.readFile and restore those exact bytes under bracket_ (the patched copy is written as UTF-8 via TE.encodeUtf8). Restoration is a raw-byte round-trip now — no decode/encode or newline translation — so "byte-for-byte" holds unconditionally. Updated this header comment to state that explicitly.
Generated by Claude Code
| -- library's src root — plus @-i \<dir-of-file\>@), then restores @original@. The | ||
| -- restore runs under 'bracket_', so the file is returned to its original bytes even if | ||
| -- Agda errors or the call is interrupted. Checking at the real path (rather than a |
There was a problem hiding this comment.
Fixed in 4157e55 — runInPlace now takes the original as a ByteString and restores it with BS.writeFile (writing the patched copy via TE.encodeUtf8), so it is a raw-byte round-trip rather than a textual one. The doc comment is updated to match, and the tests assert byte-level equality (see the reply on test/Main.hs).
Generated by Claude Code
| -- Returns Just AgdaConfig if everything is available, Nothing otherwise. | ||
| probeAgdaEnv :: IO (Maybe (AgdaConfig, FilePath)) | ||
| probeAgdaEnv :: IO (Maybe (AgdaConfig, FilePath, FilePath)) |
There was a problem hiding this comment.
Fixed in 4157e55 — the docstring now reads Returns Just (cfg, fixturePath, repoRoot) if everything is available, Nothing otherwise.
Generated by Claude Code
| -- The transiently-patched source must be restored byte-for-byte. | ||
| after <- TIO.readFile useFile | ||
| restored <- runTest "get_goal/fill_hole restore the source file exactly" $ | ||
| assert "file should be unchanged after in-place tools" (before == after) |
There was a problem hiding this comment.
Fixed in 4157e55 — before and after are now read with Data.ByteString.readFile and compared as ByteString, so the test asserts byte-level equality. The underlying restore is byte-exact too now (see the runInPlace reply), so the "byte-for-byte" wording is backed by both the implementation and the assertion.
Generated by Claude Code
| path on disk. `get_goal` and `fill_hole` must alter the source (inject the | ||
| reporting macro, or substitute a candidate), so they patch the file | ||
| transiently and restore it afterwards under `bracket_` — the original bytes | ||
| are written back even if Agda errors or the call is interrupted. Checking |
There was a problem hiding this comment.
Addressed in 4157e55 by switching the restore to raw bytes (Data.ByteString read + restore, patched copy written as UTF-8), so the README's "byte-for-byte" claim is now accurate. I also tightened the wording to say the original is captured and rewritten as raw bytes with no encoding or newline round-trip.
Generated by Claude Code
…injection Copilot review follow-ups on the in-place get_goal/fill_hole change: + Restore the file as raw bytes. get_goal/fill_hole now read the original with Data.ByteString and restore those exact bytes (writing the patched copy as UTF-8), so restoration is genuinely byte-for-byte with no encoding or newline round-trip — matching the "byte-for-byte" claims in the code, tests, and README. The restore test compares ByteString rather than Text. + Make the AgdaDojang.Debug import detection token-based instead of a substring scan: a line counts as importing the module only if, with its line comment stripped, its first token is an import keyword (import/open/private) and `AgdaDojang.Debug` appears as a whole token. This no longer misfires on a comment mention, an inline `-- ... AgdaDojang.Debug` trailer, or a longer name like `AgdaDojang.Debug.Extra`, and it recognizes `private open import ...`. + Strip line comments before the module-header `where` scan, so a `where` inside a comment on a multi-line (parameterised) header no longer misplaces the injected import. + Fix the stale probeAgdaEnv docstring (it returns a triple now). Exposes ensureDebugImport and adds five pure unit tests for the cases above. 47/47 tests pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011ZxeUxJHyQsF9p2DjpCHct
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 6 out of 6 changed files in this pull request and generated 1 comment.
Comments suppressed due to low confidence (1)
agda-mcp/src/AgdaMCP/Tools/ProofState.hs:121
TE.decodeUtf8 origBytescan throw aUnicodeExceptionfor non‑UTF8 input, crashingfill_holerather than returningLeft. Consider handling decode failures explicitly (e.g.TE.decodeUtf8'and returning a descriptiveLeft), similar toget_goal.
origBytes <- BS.readFile absPath
let src = TE.decodeUtf8 origBytes
case substituteHole (fhHoleIndex params) (fhCandidate params) src of
| origBytes <- BS.readFile absPath | ||
| let src = TE.decodeUtf8 origBytes | ||
| withImport = ensureDebugImport src | ||
| case injectReportExpr cfg (ggHoleIndex params) withImport of | ||
| Nothing -> pure . Left $ |
There was a problem hiding this comment.
Fixed in baa53d9 — both points addressed.
-
UTF-8 decode.
get_goalandfill_holenow decode withData.Text.Encoding.decodeUtf8'and return a structuredLeft "Could not decode … as UTF-8 …"on failure, so non-UTF-8 bytes no longer let aUnicodeExceptionescape the handler. Both call sites — the block here and the one on line 119 you pointed to — go through the same guard (decodeError). -
giModule. ReplacedtakeBaseNamewithmoduleNameOf, which parses the declared module name from themodule …header (with the line comment stripped), so it reports e.g.FLRP.Bridgerather thanBridge.lagdaor just the last path segment — andNothingwhen no header is found.
Added three pure tests (hierarchical name; parameterised header with a trailing comment; no-header → Nothing) plus an integration assertion that get_goal on the Proofs.Use fixture returns Just "Proofs.Use". 51/51 tests pass.
Generated by Claude Code
…name Two points from Copilot's re-review of get_goal/fill_hole: + Decode the source with Data.Text.Encoding.decodeUtf8', returning a structured Left "Could not decode ... as UTF-8" instead of letting a UnicodeException escape the handler on non-UTF-8 bytes. + Report the goal's `module` field as the *declared* module name, parsed from the `module ...` header (moduleNameOf), rather than takeBaseName -- which mangled a hierarchical module to its last segment and left ".lagda" on a literate file. Exposes moduleNameOf and adds four tests: three pure (hierarchical name; parameterised header with a trailing comment; no header -> Nothing) and one integration (get_goal on Proofs.Use reports "Proofs.Use"). 51/51 tests pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011ZxeUxJHyQsF9p2DjpCHct
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 6 out of 6 changed files in this pull request and generated 1 comment.
Comments suppressed due to low confidence (1)
agda-mcp/src/AgdaMCP/Tools/ProofState.hs:258
- This inline comment says “no single-line-terminated module header found”, but
splitAfterModuleHeaderexplicitly supports multi-line/parameterised headers and only fails when nomodule … whereheader is found at all. Updating the comment avoids suggesting a limitation that isn’t real.
Nothing -> src -- no single-line-terminated module header found
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> Signed-off-by: William DeMeo <williamdemeo@gmail.com>
| ensureDebugImport :: Text -> Text | ||
| ensureDebugImport src | ||
| | any isDebugImportLine ls = src | ||
| | otherwise = | ||
| case splitAfterModuleHeader ls of | ||
| Nothing -> src -- no single-line-terminated module header found | ||
| Just (hdr, rest) -> | ||
| T.unlines (hdr <> ["open import AgdaDojang.Debug"] <> rest) |
There was a problem hiding this comment.
Fixed in 1920b09. ensureDebugImport now restricts its "already imported?" scan to the top-level prelude — the lines after the top-level module header, up to the first nested module. So an AgdaDojang.Debug import that lives only inside a nested module no longer counts as "already imported" (its names aren't in the surrounding scope), and the top-level injection get_goal needs still happens. Added a regression test (nested-module import does not suppress injection) that asserts the import is injected right after the top-level header while the nested import is left in place.
Generated by Claude Code
| runInPlace :: AgdaConfig -> FilePath -> BS.ByteString -> Text -> IO AgdaResult | ||
| runInPlace cfg absPath originalBytes patched = | ||
| bracket_ | ||
| (BS.writeFile absPath (TE.encodeUtf8 patched)) | ||
| (BS.writeFile absPath originalBytes) | ||
| (runAgda cfgInPlace absPath) | ||
| where | ||
| cfgInPlace = cfg { agdaFlags = agdaFlags cfg <> ["-i", takeDirectory absPath] } |
There was a problem hiding this comment.
Assessed — and I'm intentionally not restoring the mtime, because doing so would trade a cosmetic win for a correctness hazard.
get_goal/fill_hole run Agda on the patched file, and Agda writes an .agdai interface keyed on the source's modification time. A fill_hole candidate that completes the module produces an interface built from the patched content; if I then reset the file's mtime back to the original (older) value, Agda's next load could treat that interface as up-to-date and reuse it — so a later check_file might report the module as complete when the real source still has {!!}. Leaving a fresh mtime (the current behaviour) forces Agda to re-typecheck from the restored source under every interface-freshness rule, which is the safe choice.
The file contents are still restored byte-for-byte — only the mtime is left fresh, on purpose — and editors that compare content (not mtime alone) won't prompt. Permissions aren't touched either: writeFile on an existing file preserves its mode. I documented this rationale in runInPlace's doc comment (1920b09) rather than change the behaviour.
Generated by Claude Code
…me choice Third Copilot re-review of the in-place get_goal/fill_hole change: + ensureDebugImport now restricts its "already imported?" scan to the top-level prelude -- the lines after the top-level module header, up to the first nested `module` -- so an AgdaDojang.Debug import that lives only inside a nested module (and so is not in the surrounding scope) no longer suppresses the top-level injection get_goal needs. Added a regression test. + Documented why runInPlace deliberately leaves a fresh mtime rather than restoring the original: a newer mtime forces Agda to re-typecheck from the restored source, whereas resetting it could let Agda reuse an .agdai built from the transiently-patched content. Contents are still restored byte-for-byte; only the (cosmetic) mtime is left fresh, on purpose. Also softened the ensureDebugImport doc from "guarantee" to "best-effort" to match the headerless-file fallback. 52/52 tests pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011ZxeUxJHyQsF9p2DjpCHct
Description
What changed.
get_goalandfill_holenow typecheck the target file in place, the waycheck_file/get_diagnosticsalready do, instead of copying it to a scratch directory first.Why. The scratch-copy approach works for flat, top-level modules (every
data/benchmarks/fixture) but breaks on a module embedded in a library at a hierarchical path — e.g.FLRP.Bridgeatsrc/FLRP/Bridge.lagda.mdinagda-algebras. Once the library'ssrcroot is on the include path (via the caller's-l <lib>), the scratch copy collides with the module's canonical file and Agda rejects it withModuleDefinedInOtherFile. That blocked using the two temp-copy tools on real libraries — the "agda-mcp onagda-algebras/formal-ledger-specifications" use case.check_file/get_diagnosticswere unaffected because they already load in place.How.
get_goalandfill_holepatch the real file transiently and restore it underbracket_, so the original bytes are written back even if Agda errors or the call is interrupted. They reusecheck_file's include strategy, so a hierarchically-named module resolves its own name and cross-directory imports exactly as it does for the developer.get_goaladditionally ensuresopen import AgdaDojang.Debugis in scope (a library file will not import it), injecting it after the module header when absent. The "already imported?" check and the header search both look at realimport/modulelines, so a passing mention in a comment neither suppresses nor misplaces the injection; parameterised (multi-line) module headers are handled.makeTmpDir/makeOverlay/stripIncludeDir), which also makes [M1-2 follow-up] makeOverlay: optimize overlay creation for large source trees #43 moot for these two tools.How tested.
make agda-mcp-test(cabal test) insidenix develop .#backend— 42/42 tests pass, up from 37. Five new tier-2 tests run against a committed regression fixture (agda-dojang/data/fixtures/hier-lib/): a two-directory mini-library whose hierarchically-named moduleProofs.Useimports across a sibling directory (Widgets.Thing) and does not importAgdaDojang.Debug. They assertget_goalreturns a goal with the local variablexin context (proving the transient import injection),fill_holeaccepts a cross-directory term (thing) and rejects an ill-typed one (tt), and the source file is byte-for-byte unchanged after the calls. I also reproduced the originalModuleDefinedInOtherFilefailure against a scratch copy of the same shape and confirmed the in-place path fixes it.Docs. Updates
agda-mcp/README.md(theget_goal/fill_hole"how it works" notes and an "In-place typechecking" architecture note). The cross-project walkthrough indocs/HowToRun.md§13.5 (on PR #65) currently documents this as a known limitation; once both land, that caveat should be lifted.Closes #66.
Acceptance Criteria
All checks(the CI aggregator gate) is green.README.md,docs/,CONTRIBUTING.md, ...).*.agdai,target/,.venv/, generateddata/).Generated by Claude Code