From 4a171350dfcabdd73e504cc5d584e133038192c8 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 20 Jul 2026 17:29:12 +0000 Subject: [PATCH 1/5] [agda-mcp] get_goal/fill_hole: typecheck in place so library modules resolve (#66) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Claude-Session: https://claude.ai/code/session_011ZxeUxJHyQsF9p2DjpCHct --- .../data/fixtures/hier-lib/hier-lib.agda-lib | 2 + .../fixtures/hier-lib/src/Proofs/Use.agda | 23 ++ .../fixtures/hier-lib/src/Widgets/Thing.agda | 16 ++ agda-mcp/README.md | 15 +- agda-mcp/src/AgdaMCP/Tools/ProofState.hs | 205 ++++++++---------- agda-mcp/test/Main.hs | 77 ++++++- 6 files changed, 222 insertions(+), 116 deletions(-) create mode 100644 agda-dojang/data/fixtures/hier-lib/hier-lib.agda-lib create mode 100644 agda-dojang/data/fixtures/hier-lib/src/Proofs/Use.agda create mode 100644 agda-dojang/data/fixtures/hier-lib/src/Widgets/Thing.agda diff --git a/agda-dojang/data/fixtures/hier-lib/hier-lib.agda-lib b/agda-dojang/data/fixtures/hier-lib/hier-lib.agda-lib new file mode 100644 index 0000000..060ee6b --- /dev/null +++ b/agda-dojang/data/fixtures/hier-lib/hier-lib.agda-lib @@ -0,0 +1,2 @@ +name: hier-lib +include: src diff --git a/agda-dojang/data/fixtures/hier-lib/src/Proofs/Use.agda b/agda-dojang/data/fixtures/hier-lib/src/Proofs/Use.agda new file mode 100644 index 0000000..62f7258 --- /dev/null +++ b/agda-dojang/data/fixtures/hier-lib/src/Proofs/Use.agda @@ -0,0 +1,23 @@ +-- Use.agda +-- +-- File: agda-dojang/data/fixtures/hier-lib/src/Proofs/Use.agda +-- +-- Description: +-- Regression fixture for issue #66: a hierarchically-named module (`Proofs.Use`) +-- embedded in a library (`hier-lib`) that imports across a sibling directory +-- (`Widgets.Thing`). This is the shape that broke the old temp-copy get_goal / +-- fill_hole path (ModuleDefinedInOtherFile), and that the in-place implementation +-- must handle. +-- +-- It deliberately does NOT `open import AgdaDojang.Debug`, so exercising get_goal +-- on it also tests the transient import injection. +module Proofs.Use where + +open import Agda.Builtin.Nat +open import Agda.Builtin.Unit +open import Widgets.Thing + +-- A single hole with a local variable in context, mirroring Fixture01's `id x`. +-- Correct fill: `thing` (a cross-directory Nat). Ill-typed fill: `tt` (⊤ ≢ Nat). +useIt : Nat → Nat +useIt x = {!!} diff --git a/agda-dojang/data/fixtures/hier-lib/src/Widgets/Thing.agda b/agda-dojang/data/fixtures/hier-lib/src/Widgets/Thing.agda new file mode 100644 index 0000000..69407af --- /dev/null +++ b/agda-dojang/data/fixtures/hier-lib/src/Widgets/Thing.agda @@ -0,0 +1,16 @@ +-- Thing.agda +-- +-- File: agda-dojang/data/fixtures/hier-lib/src/Widgets/Thing.agda +-- +-- Description: +-- A trivial module in the `hier-lib` regression fixture, living under a +-- top-level directory (`Widgets/`) distinct from the module that imports it +-- (`Proofs.Use`). Its only job is to be a cross-directory dependency, so that +-- type-checking `Proofs.Use` exercises hierarchical include-path resolution. +-- See issue #66 and agda-mcp/test/Main.hs. +module Widgets.Thing where + +open import Agda.Builtin.Nat + +thing : Nat +thing = 7 diff --git a/agda-mcp/README.md b/agda-mcp/README.md index 57176fe..3173484 100644 --- a/agda-mcp/README.md +++ b/agda-mcp/README.md @@ -185,7 +185,7 @@ Given a file path and hole identifier, return the hole's expected type and its l } ``` -**How it works**. Injects the `reportGoalCtx` macro into the hole, runs Agda, and parses the `AGDADOJANG_REQ_BEGIN/END` marker block from stderr. +**How it works**. Ensures `AgdaDojang.Debug` is imported (injecting the import transiently if the file does not already import it), replaces the hole with the `reportGoalCtx` macro, typechecks the file **in place**, and parses the `AGDADOJANG_REQ_BEGIN/END` marker block. Checking at the file's real path (rather than a scratch copy) lets hierarchically-named modules embedded in a library resolve normally; the original source is restored after the call. #### `fill_hole` @@ -218,6 +218,8 @@ Submit a candidate term for a hole and receive typecheck feedback: success (hole } ``` +**How it works**. Substitutes the candidate into the hole, typechecks the file **in place** (restoring the original afterwards), and reports success — tolerating unsolved metas from the file's other open holes — or the type error. As with `get_goal`, checking at the real path lets library-embedded modules resolve. + #### `check_file` Load or reload an Agda file and return all diagnostics — errors, warnings, unsolved metas, and remaining holes. @@ -407,6 +409,17 @@ tool invocation. This mirrors how `agda-dojang`'s Python tooling **Advantages:** simple, decoupled from Agda's GHC version, reuses all existing AgdaDojang macros without modification. +**In-place typechecking.** All four tools typecheck the file at its real +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 +in place, rather than against a scratch copy, is what lets a +hierarchically-named module embedded in a library resolve its own name and +cross-directory imports the same way it does for the developer; an earlier +scratch-copy approach failed on such modules with `ModuleDefinedInOtherFile` +(issue #66). + **Limitations:** each tool call spawns a new Agda process (cold typechecking, no persistent state). This is acceptable for the v0 demo and benchmark fixtures, but will need optimization for larger files. diff --git a/agda-mcp/src/AgdaMCP/Tools/ProofState.hs b/agda-mcp/src/AgdaMCP/Tools/ProofState.hs index 351cb79..07580fc 100644 --- a/agda-mcp/src/AgdaMCP/Tools/ProofState.hs +++ b/agda-mcp/src/AgdaMCP/Tools/ProofState.hs @@ -14,6 +14,21 @@ -- * fill_hole - try a candidate term and report typecheck result -- * check_file - load/reload a file and return all diagnostics -- * get_diagnostics - lightweight summary (hole count, error count) +-- +-- Design note — all four tools typecheck the file IN PLACE. +-- Agda decides a module's name from where its file sits relative to the include +-- path, so a module embedded in a library at a hierarchical path (e.g. FLRP.Bridge +-- at src/FLRP/Bridge.lagda.md) only resolves when it is checked at its real +-- location, with the library's src root on the include path (supplied by the +-- caller's `-l ` flag). An earlier version copied the file to a scratch +-- directory before checking it; that works for flat top-level modules but collides +-- with the module's canonical file for library-embedded ones (ModuleDefinedInOtherFile +-- / ModuleNameDoesntMatchFileName). See issue #66. +-- +-- 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. {-# LANGUAGE OverloadedStrings #-} @@ -24,18 +39,14 @@ module AgdaMCP.Tools.ProofState , handleGetDiagnostics ) where -import Control.Exception (SomeException, catch) -import Control.Monad (forM_) +import Control.Exception (bracket_) +import Data.List (findIndex) import Data.Text (Text) import qualified Data.Text as T import qualified Data.Text.IO as TIO -import System.Directory ( copyFile, createDirectoryIfMissing, doesDirectoryExist - , getTemporaryDirectory, listDirectory, makeAbsolute - , removeDirectoryRecursive ) - -import System.FilePath ((), takeFileName, takeDirectory, takeBaseName) -import System.IO (hPutStrLn, stderr) +import System.Directory (makeAbsolute) +import System.FilePath (takeDirectory, takeBaseName) import AgdaMCP.Agda ( AgdaConfig, AgdaResult (..), agdaFlags, debugLog @@ -51,35 +62,23 @@ import AgdaMCP.Types -- | handleGetGoal: inspect goal type and local context at hole @n@ in given file. -- -- 1. Read source file. --- 2. Replace hole @n@ with @reportGoalCtx ?@. --- 3. Write a temporary copy and run Agda on it. --- 4. Parse AGDADOJANG_REQ_BEGIN/END block from stderr. --- 5. Return structured (goal, context). +-- 2. Ensure @open import AgdaDojang.Debug@ is in scope (inject it if absent) so the +-- @reportGoalCtx@ macro resolves. +-- 3. Replace hole @n@ with @reportGoalCtx ?@. +-- 4. Typecheck the patched file IN PLACE (restoring the original afterwards). +-- 5. Parse the AGDADOJANG_REQ_BEGIN/END block from Agda's output. +-- 6. Return structured (goal, context). handleGetGoal :: AgdaConfig -> GetGoalParams -> IO (Either Text GoalInfo) handleGetGoal cfg params = do absPath <- makeAbsolute (ggFilePath params) src <- TIO.readFile absPath - case injectReportExpr cfg (ggHoleIndex params) src of + let withImport = ensureDebugImport src + case injectReportExpr cfg (ggHoleIndex params) withImport of Nothing -> pure . Left $ "Hole index " <> T.pack (show (ggHoleIndex params)) <> " not found in " <> T.pack absPath Just patched -> do - tmpDir <- makeTmpDir "agda-mcp-goal" - let tmpFile = tmpDir takeFileName absPath - srcDir = takeDirectory absPath - TIO.writeFile tmpFile patched - -- Create an overlay of the source directory WITHOUT the file being - -- checked, to avoid Agda's ModuleDefinedInOtherFile error. - overlay <- makeOverlay tmpDir srcDir (takeFileName absPath) - -- Port of agent_bridge.py's include-path strategy: - -- 1. Strip -i from base flags (avoids AmbiguousTopLevelModuleName - -- if srcDir happens to be on the include path). - -- 2. Add -i (where the patched file lives — resolves - -- ModuleNameDoesntMatchFileName) and -i (sibling modules). - let baseFlags = stripIncludeDir srcDir (agdaFlags cfg) - extraFlags = ["-i", tmpDir, "-i", overlay] - cfgWithDir = cfg { agdaFlags = baseFlags <> extraFlags } - result <- runAgda cfgWithDir tmpFile + result <- runInPlace cfg absPath src patched -- DEBUG: show what Agda actually returned debugLog cfg $ "get_goal: exit=" <> T.pack (show (arExitCode result)) debugLog cfg $ "get_goal stdout: " <> T.take 500 (arStdout result) @@ -105,8 +104,9 @@ handleGetGoal cfg params = do -- | handleFillHole: try substituting @candidate@ into hole @n@ and typecheck. -- -- 1. Read source, substitute candidate into hole n. --- 2. Write temp copy, run Agda. --- 3. If exit 0 → success; otherwise → type error. +-- 2. Typecheck the patched file IN PLACE (restoring the original afterwards). +-- 3. If exit 0 → success; otherwise → type error (tolerating unsolved metas from +-- the file's other, still-open holes). handleFillHole :: AgdaConfig -> FillHoleParams -> IO (Either Text FillResult) handleFillHole cfg params = do absPath <- makeAbsolute (fhFilePath params) @@ -116,16 +116,8 @@ handleFillHole cfg params = do "Hole index " <> T.pack (show (fhHoleIndex params)) <> " not found in " <> T.pack (fhFilePath params) Just patched -> do - tmpDir <- makeTmpDir "agda-mcp-fill" - let tmpFile = tmpDir takeFileName absPath - srcDir = takeDirectory absPath - TIO.writeFile tmpFile patched - overlay <- makeOverlay tmpDir srcDir (takeFileName absPath) - let baseFlags = stripIncludeDir srcDir (agdaFlags cfg) - extraFlags = ["-i", tmpDir, "-i", overlay] - cfgWithDir = cfg { agdaFlags = baseFlags <> extraFlags } - result <- runAgda cfgWithDir tmpFile - -- Agda 2.8.0 emits some errors on stdout; check both streams. + result <- runInPlace cfg absPath src patched + -- Agda 2.8.0 emits some errors on stdout; check both streams. let combined = arStdout result <> "\n" <> arStderr result -- A non-zero exit is acceptable if the *only* errors are unsolved -- interaction metas (from other holes we haven't filled yet). @@ -209,6 +201,69 @@ handleGetDiagnostics cfg params = do -- Internal helpers -- --------------------------------------------------------------------------- +-- | runInPlace: typecheck a transiently-patched version of a file at its real path. +-- +-- Writes @patched@ over @absPath@, runs Agda there with the same include strategy +-- 'handleCheckFile' uses (base flags — which carry the caller's @-l \@, hence the +-- library's src root — plus @-i \@), 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 +-- scratch copy) is what lets hierarchically-named library modules resolve — see the +-- module header and issue #66. +runInPlace :: AgdaConfig -> FilePath -> Text -> Text -> IO AgdaResult +runInPlace cfg absPath original patched = + bracket_ + (TIO.writeFile absPath patched) + (TIO.writeFile absPath original) + (runAgda cfgInPlace absPath) + where + cfgInPlace = cfg { agdaFlags = agdaFlags cfg <> ["-i", takeDirectory absPath] } + + +-- | ensureDebugImport: guarantee @open import AgdaDojang.Debug@ is in scope. +-- +-- The @reportGoalCtx@ macro get_goal injects lives in @AgdaDojang.Debug@; a library +-- file being inspected will not normally import it. If the module already imports it +-- this is a no-op; otherwise the import is inserted immediately after the module +-- header — i.e. after the header's closing @where@, which may be several lines below +-- the @module@ keyword when the module is parameterised (common in agda-algebras). +-- Placing it there is valid for both @.agda@ and literate @.lagda.md@ sources, since +-- the header sits in code context in both. agda-dojang is on the library path +-- (@-l agda-dojang@), so the import resolves. +-- +-- Both the "already imported?" test and the header search look at real import/module +-- lines (not mere substrings), so a passing mention of @AgdaDojang.Debug@ or @module@ +-- in a comment neither suppresses the injection nor misplaces it. +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) + where + ls = T.lines src + + -- A genuine import line: after stripping leading space it begins with + -- @open@ or @import@ and names the module. + isDebugImportLine ln = + let s = T.stripStart ln + in ("open" `T.isPrefixOf` s || "import" `T.isPrefixOf` s) + && "AgdaDojang.Debug" `T.isInfixOf` ln + +-- | splitAfterModuleHeader: split source lines just after the top-level module +-- header. The header runs from the first line whose code begins with @module@ +-- through the first subsequent line that carries a standalone @where@ token +-- (they may be the same line, or several apart for a parameterised module). +-- Returns @Nothing@ if no such header is found. +splitAfterModuleHeader :: [Text] -> Maybe ([Text], [Text]) +splitAfterModuleHeader ls = do + 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) + + -- | parseDiagnostics: parse Agda stderr into a list of diagnostics. -- -- This is a best-effort heuristic parser. Agda error messages typically @@ -242,71 +297,3 @@ parseDiagnostics stderr' = _ -> Nothing _ -> Nothing _ -> Nothing - - --- | stripIncludeDir: strip @-i @ token pairs from flag list when @dir@ matches @dropDir@. --- --- In shadow mode we typecheck a temp copy; if the original directory is also on the --- include path, Agda sees two files for the same module → AmbiguousTopLevelModuleName. --- (Port of agent_bridge.py's @_drop_include_dir_tokens@.) -stripIncludeDir :: FilePath -> [String] -> [String] -stripIncludeDir _ [] = [] -stripIncludeDir dropDir ("-i" : dir : rest) - | norm dir == norm dropDir = stripIncludeDir dropDir rest - where norm p = reverse $ dropWhile (== '/') $ reverse p -stripIncludeDir dropDir (x : rest) = x : stripIncludeDir dropDir rest - - --- | makeTmpDir: create a temp directory for scratch Agda files. -makeTmpDir :: String -> IO FilePath -makeTmpDir label = do - tmp <- getTemporaryDirectory - let dir = tmp label - -- NOTE: v0 uses a fixed name (sequential requests only). - -- TODO: switch to createTempDirectory for concurrent safety. - -- SEE: https://github.com/formalverification/agda-native-air/pull/38#discussion_r2969684711 - createDirectoryIfMissing True dir - pure dir - --- Bring concatMap into scope for the list comprehension in parseDiagnostics. --- (It's in Prelude, but explicit for clarity with GHC2021.) - --- | makeOverlay: create overlay directory mirroring @srcDir@ except for @excludeFile@. --- --- This avoids Agda's @ModuleDefinedInOtherFile@ error when we typecheck a patched --- copy of a file while still needing sibling imports to resolve. --- (Port of agent_bridge.py's _ensure_overlay_dir.) -makeOverlay :: FilePath -> FilePath -> String -> IO FilePath -makeOverlay tmpDir srcDir excludeFile = do - let overlay = tmpDir "_overlay" - -- Remove stale overlay from previous invocations — a prior call may have - -- excluded a different file, leaving entries that must now be absent. - removeDirectoryRecursive overlay `catch` \(_ :: SomeException) -> pure () - createDirectoryIfMissing True overlay - entries <- listDirectory srcDir - let keep = [ e | e <- entries, e /= excludeFile ] - mapM_ (copyEntry overlay) keep - pure overlay - where - copyEntry overlay name = do - let target = srcDir name - link = overlay name - isDir <- doesDirectoryExist target - if isDir - then copyDirectoryRecursive target link - else copyFile target link - `catch` \(e :: SomeException) -> - hPutStrLn stderr $ "agda-mcp: overlay copy failed for " <> name <> ": " <> show e - - -- | Recursively copy a directory tree from @src@ to @dst@. - copyDirectoryRecursive :: FilePath -> FilePath -> IO () - copyDirectoryRecursive src dst = do - createDirectoryIfMissing True dst - entries <- listDirectory src - forM_ entries $ \entry -> do - let srcPath = src entry - dstPath = dst entry - isSubDir <- doesDirectoryExist srcPath - if isSubDir - then copyDirectoryRecursive srcPath dstPath - else copyFile srcPath dstPath diff --git a/agda-mcp/test/Main.hs b/agda-mcp/test/Main.hs index 06e193d..c844ccf 100644 --- a/agda-mcp/test/Main.hs +++ b/agda-mcp/test/Main.hs @@ -32,6 +32,7 @@ import qualified Data.Map.Strict as Map import Data.Maybe (isJust, isNothing) import Data.Text (Text) import qualified Data.Text as T +import qualified Data.Text.IO as TIO import System.Directory (findExecutable, doesFileExist, getCurrentDirectory) import System.Exit (exitFailure, exitSuccess) import System.FilePath ((), takeDirectory) @@ -316,7 +317,7 @@ corpusTests = do -- 2. fixture file exists -- 3. agda-dojang libraries file exists -- Returns Just AgdaConfig if everything is available, Nothing otherwise. -probeAgdaEnv :: IO (Maybe (AgdaConfig, FilePath)) +probeAgdaEnv :: IO (Maybe (AgdaConfig, FilePath, FilePath)) probeAgdaEnv = do mAgda <- findExecutable "agda" case mAgda of @@ -354,15 +355,15 @@ probeAgdaEnv = do , "-l", "standard-library" ] } - pure (Just (cfg, fixturePath)) + pure (Just (cfg, fixturePath, repoRoot)) -- | integrationTests: Tier 2 tests that call tool handlers on real fixture files -- with a real Agda binary. -integrationTests :: AgdaConfig -> FilePath -> IO [Bool] -integrationTests cfg fixturePath = do +integrationTests :: AgdaConfig -> FilePath -> FilePath -> IO [Bool] +integrationTests cfg fixturePath repoRoot = do hPutStrLn stderr "\n── Integration tests (tier 2: Agda subprocess) ──" - sequence + base <- sequence [ runTest "get_goal: Fixture01 hole 0 returns a non-empty goal" $ do let params = GetGoalParams { ggFilePath = fixturePath, ggHoleIndex = 0 } result <- handleGetGoal cfg params @@ -418,7 +419,71 @@ integrationTests cfg fixturePath = do Right dr -> assert "should report at least 1 hole" (not . null $ drHoles dr) ] + hier <- hierIntegrationTests cfg repoRoot + pure (base <> hier) + +-- | hierIntegrationTests: issue #66 regression. +-- +-- get_goal / fill_hole must work on a hierarchically-named module embedded in a +-- library that imports across directories (the shape that broke the old temp-copy +-- path with ModuleDefinedInOtherFile). The fixture library's src root is placed on +-- the include path via @-i@, the way a caller's @-l \@ supplies it in real use. +-- The fixture deliberately does not import @AgdaDojang.Debug@, so get_goal here also +-- exercises the transient import injection. Skipped (with a note) if absent. +hierIntegrationTests :: AgdaConfig -> FilePath -> IO [Bool] +hierIntegrationTests cfg repoRoot = do + let hierSrc = repoRoot "agda-dojang" "data" "fixtures" + "hier-lib" "src" + useFile = hierSrc "Proofs" "Use.agda" + hierCfg = cfg { agdaFlags = agdaFlags cfg <> ["-i", hierSrc] } + exists <- doesFileExist useFile + if not exists + then do + hPutStrLn stderr $ "\n [skip] hier fixture not found: " <> useFile + pure [] + else do + hPutStrLn stderr + "\n── Integration tests (tier 2b: library-embedded module, #66) ──" + before <- TIO.readFile useFile + results <- sequence + [ runTest "get_goal: Proofs.Use (hierarchical) returns a non-empty goal" $ do + let params = GetGoalParams { ggFilePath = useFile, ggHoleIndex = 0 } + result <- handleGetGoal hierCfg params + case result of + Left err -> pure (Fail $ "get_goal failed: " <> T.unpack err) + Right info -> assert "goal should be non-empty" (not . T.null $ giGoal info) + + , runTest "get_goal: Proofs.Use context contains 'x' (Debug import injected)" $ do + let params = GetGoalParams { ggFilePath = useFile, ggHoleIndex = 0 } + result <- handleGetGoal hierCfg params + case result of + Left err -> pure (Fail $ "get_goal failed: " <> T.unpack err) + Right info -> + assert "'x' should be in context" + ("x" `elem` map ctxName (giContext info)) + + , runTest "fill_hole: Proofs.Use with cross-directory 'thing' succeeds" $ do + let params = FillHoleParams + { fhFilePath = useFile, fhHoleIndex = 0, fhCandidate = "thing" } + result <- handleFillHole hierCfg params + case result of + Left err -> pure (Fail $ "fill_hole failed: " <> T.unpack err) + Right fr -> assertEqual "status" FillOk (frStatus fr) + + , runTest "fill_hole: Proofs.Use with ill-typed 'tt' is a type error" $ do + let params = FillHoleParams + { fhFilePath = useFile, fhHoleIndex = 0, fhCandidate = "tt" } + result <- handleFillHole hierCfg params + case result of + Left err -> pure (Fail $ "fill_hole failed unexpectedly: " <> T.unpack err) + Right fr -> assertEqual "status" FillTypeError (frStatus fr) + ] + -- 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) + pure (results <> [restored]) -- --------------------------------------------------------------------------- @@ -439,7 +504,7 @@ main = do Nothing -> do hPutStrLn stderr "\n── Integration tests (tier 2): SKIPPED ──" pure [] - Just (cfg, fixture) -> integrationTests cfg fixture + Just (cfg, fixture, repoRoot) -> integrationTests cfg fixture repoRoot let allResults = pureResults <> corpusResults <> integrationResults total = length allResults From 4157e5534ef3179d6d5d0abfcb2cc68c9fdc8739 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 24 Jul 2026 05:42:27 +0000 Subject: [PATCH 2/5] [agda-mcp] address PR #67 review: byte-exact restore + robust import injection MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Claude-Session: https://claude.ai/code/session_011ZxeUxJHyQsF9p2DjpCHct --- agda-mcp/README.md | 15 ++--- agda-mcp/src/AgdaMCP/Tools/ProofState.hs | 77 +++++++++++++++--------- agda-mcp/test/Main.hs | 53 ++++++++++++++-- 3 files changed, 104 insertions(+), 41 deletions(-) diff --git a/agda-mcp/README.md b/agda-mcp/README.md index 3173484..c9270e4 100644 --- a/agda-mcp/README.md +++ b/agda-mcp/README.md @@ -412,13 +412,14 @@ existing AgdaDojang macros without modification. **In-place typechecking.** All four tools typecheck the file at its real 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 -in place, rather than against a scratch copy, is what lets a -hierarchically-named module embedded in a library resolve its own name and -cross-directory imports the same way it does for the developer; an earlier -scratch-copy approach failed on such modules with `ModuleDefinedInOtherFile` -(issue #66). +transiently and restore it afterwards under `bracket_`. The original is +captured and rewritten as raw bytes (`Data.ByteString`), so the file is +returned byte-for-byte — no encoding or newline round-trip — even if Agda +errors or the call is interrupted. Checking in place, rather than against a +scratch copy, is what lets a hierarchically-named module embedded in a +library resolve its own name and cross-directory imports the same way it does +for the developer; an earlier scratch-copy approach failed on such modules +with `ModuleDefinedInOtherFile` (issue #66). **Limitations:** each tool call spawns a new Agda process (cold typechecking, no persistent state). This is acceptable for the v0 demo diff --git a/agda-mcp/src/AgdaMCP/Tools/ProofState.hs b/agda-mcp/src/AgdaMCP/Tools/ProofState.hs index 07580fc..c9b54b5 100644 --- a/agda-mcp/src/AgdaMCP/Tools/ProofState.hs +++ b/agda-mcp/src/AgdaMCP/Tools/ProofState.hs @@ -27,8 +27,9 @@ -- -- 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. +-- it under 'Control.Exception.bracket_'. The original is captured and restored as +-- raw bytes ('Data.ByteString'), so the file is returned byte-for-byte even if Agda +-- errors or the call is interrupted — no encoding or newline round-trip is involved. {-# LANGUAGE OverloadedStrings #-} @@ -37,12 +38,16 @@ module AgdaMCP.Tools.ProofState , handleFillHole , handleCheckFile , handleGetDiagnostics + -- * Exposed for testing + , ensureDebugImport ) where import Control.Exception (bracket_) +import qualified Data.ByteString as BS import Data.List (findIndex) import Data.Text (Text) import qualified Data.Text as T +import qualified Data.Text.Encoding as TE import qualified Data.Text.IO as TIO import System.Directory (makeAbsolute) @@ -71,14 +76,15 @@ import AgdaMCP.Types handleGetGoal :: AgdaConfig -> GetGoalParams -> IO (Either Text GoalInfo) handleGetGoal cfg params = do absPath <- makeAbsolute (ggFilePath params) - src <- TIO.readFile absPath - let withImport = ensureDebugImport src + origBytes <- BS.readFile absPath + let src = TE.decodeUtf8 origBytes + withImport = ensureDebugImport src case injectReportExpr cfg (ggHoleIndex params) withImport of Nothing -> pure . Left $ "Hole index " <> T.pack (show (ggHoleIndex params)) <> " not found in " <> T.pack absPath Just patched -> do - result <- runInPlace cfg absPath src patched + result <- runInPlace cfg absPath origBytes patched -- DEBUG: show what Agda actually returned debugLog cfg $ "get_goal: exit=" <> T.pack (show (arExitCode result)) debugLog cfg $ "get_goal stdout: " <> T.take 500 (arStdout result) @@ -110,13 +116,14 @@ handleGetGoal cfg params = do handleFillHole :: AgdaConfig -> FillHoleParams -> IO (Either Text FillResult) handleFillHole cfg params = do absPath <- makeAbsolute (fhFilePath params) - src <- TIO.readFile absPath + origBytes <- BS.readFile absPath + let src = TE.decodeUtf8 origBytes case substituteHole (fhHoleIndex params) (fhCandidate params) src of Nothing -> pure . Left $ "Hole index " <> T.pack (show (fhHoleIndex params)) <> " not found in " <> T.pack (fhFilePath params) Just patched -> do - result <- runInPlace cfg absPath src patched + result <- runInPlace cfg absPath origBytes patched -- Agda 2.8.0 emits some errors on stdout; check both streams. let combined = arStdout result <> "\n" <> arStderr result -- A non-zero exit is acceptable if the *only* errors are unsolved @@ -203,18 +210,20 @@ handleGetDiagnostics cfg params = do -- | runInPlace: typecheck a transiently-patched version of a file at its real path. -- --- Writes @patched@ over @absPath@, runs Agda there with the same include strategy --- 'handleCheckFile' uses (base flags — which carry the caller's @-l \@, hence the --- library's src root — plus @-i \@), 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 --- scratch copy) is what lets hierarchically-named library modules resolve — see the --- module header and issue #66. -runInPlace :: AgdaConfig -> FilePath -> Text -> Text -> IO AgdaResult -runInPlace cfg absPath original patched = +-- Writes @patched@ (as UTF-8) over @absPath@, runs Agda there with the same include +-- strategy 'handleCheckFile' uses (base flags — which carry the caller's @-l \@, +-- hence the library's src root — plus @-i \@), then restores +-- @originalBytes@. Both the write and the restore go through 'Data.ByteString', and +-- the restore runs under 'bracket_', so the file is returned to its exact original +-- bytes even if Agda errors or the call is interrupted — no encoding or newline +-- round-trip is involved. Checking at the real path (rather than a scratch copy) is +-- what lets hierarchically-named library modules resolve — see the module header and +-- issue #66. +runInPlace :: AgdaConfig -> FilePath -> BS.ByteString -> Text -> IO AgdaResult +runInPlace cfg absPath originalBytes patched = bracket_ - (TIO.writeFile absPath patched) - (TIO.writeFile absPath original) + (BS.writeFile absPath (TE.encodeUtf8 patched)) + (BS.writeFile absPath originalBytes) (runAgda cfgInPlace absPath) where cfgInPlace = cfg { agdaFlags = agdaFlags cfg <> ["-i", takeDirectory absPath] } @@ -245,24 +254,36 @@ ensureDebugImport src where ls = T.lines src - -- A genuine import line: after stripping leading space it begins with - -- @open@ or @import@ and names the module. + -- A genuine import of the module: with any line comment stripped, the first + -- token is an import-introducing keyword, @import@ is present, and + -- @AgdaDojang.Debug@ appears as a whole module token — so none of a comment + -- mention, an inline @-- … AgdaDojang.Debug@ trailer, or a longer name such as + -- @AgdaDojang.Debug.Extra@ is mistaken for the import. isDebugImportLine ln = - let s = T.stripStart ln - in ("open" `T.isPrefixOf` s || "import" `T.isPrefixOf` s) - && "AgdaDojang.Debug" `T.isInfixOf` ln + case T.words (stripLineComment ln) of + ws@(w : _) -> w `elem` ["import", "open", "private"] + && "import" `elem` ws + && "AgdaDojang.Debug" `elem` ws + [] -> False -- | splitAfterModuleHeader: split source lines just after the top-level module -- header. The header runs from the first line whose code begins with @module@ --- through the first subsequent line that carries a standalone @where@ token --- (they may be the same line, or several apart for a parameterised module). --- Returns @Nothing@ if no such header is found. +-- through the first subsequent line that carries a standalone @where@ token (they may +-- be the same line, or several apart for a parameterised module). Line comments are +-- stripped before the scan, so a @where@ (or @module@) sitting inside a @--@ comment on +-- a header line is ignored. Returns @Nothing@ if no such header is found. splitAfterModuleHeader :: [Text] -> Maybe ([Text], [Text]) splitAfterModuleHeader ls = do - i <- findIndex (\l -> "module" `T.isPrefixOf` T.stripStart l) ls - jRel <- findIndex (\l -> "where" `elem` T.words l) (drop i ls) + i <- findIndex (\l -> "module" `T.isPrefixOf` T.stripStart (stripLineComment l)) ls + jRel <- findIndex (\l -> "where" `elem` T.words (stripLineComment l)) (drop i ls) pure (splitAt (i + jRel + 1) ls) +-- | stripLineComment: drop an Agda @--@ line comment (best-effort: treats the first +-- @--@ as the comment start). Enough to keep comment text out of the keyword and +-- @where@ scans above; block comments (@{- … -}@) are not handled. +stripLineComment :: Text -> Text +stripLineComment = fst . T.breakOn "--" + -- | parseDiagnostics: parse Agda stderr into a list of diagnostics. -- diff --git a/agda-mcp/test/Main.hs b/agda-mcp/test/Main.hs index c844ccf..9736cfb 100644 --- a/agda-mcp/test/Main.hs +++ b/agda-mcp/test/Main.hs @@ -32,7 +32,7 @@ import qualified Data.Map.Strict as Map import Data.Maybe (isJust, isNothing) import Data.Text (Text) import qualified Data.Text as T -import qualified Data.Text.IO as TIO +import qualified Data.ByteString as BS import System.Directory (findExecutable, doesFileExist, getCurrentDirectory) import System.Exit (exitFailure, exitSuccess) import System.FilePath ((), takeDirectory) @@ -45,7 +45,8 @@ import AgdaMCP.Agda ) import AgdaMCP.Corpus (loadCorpus, searchByName, searchByType, getDeps) import AgdaMCP.Tools.ProofState - ( handleGetGoal, handleFillHole, handleCheckFile, handleGetDiagnostics ) + ( handleGetGoal, handleFillHole, handleCheckFile, handleGetDiagnostics + , ensureDebugImport ) import AgdaMCP.Tools.Search ( handleSearchByName, handleSearchByType, handleGetDependencies ) import AgdaMCP.Types @@ -181,6 +182,44 @@ pureTests = do , runTest "parseGoalContext: no markers → Nothing" $ assert "should be Nothing" (isNothing $ parseGoalContext "no markers here") + + -- ensureDebugImport: the get_goal import-injection heuristic (issue #66 review). + , runTest "ensureDebugImport: no-op when already imported" $ do + let s = T.unlines + [ "module M where", "open import AgdaDojang.Debug", "foo = {!!}" ] + assertEqual "unchanged" s (ensureDebugImport s) + + , runTest "ensureDebugImport: recognizes a private-qualified import (no duplicate)" $ do + let s = T.unlines + [ "module M where", "private open import AgdaDojang.Debug", "foo = {!!}" ] + assertEqual "unchanged" s (ensureDebugImport s) + + , runTest "ensureDebugImport: a longer name (.Debug.Extra) is not the module" $ do + let s = T.unlines + [ "module M where", "open import AgdaDojang.Debug.Extra", "foo = {!!}" ] + assert "injects the real import" + ("open import AgdaDojang.Debug" `elem` T.lines (ensureDebugImport s)) + + , runTest "ensureDebugImport: a comment mention does not count as an import" $ do + let s = T.unlines + [ "module M where" + , "open import Data.Nat -- also see AgdaDojang.Debug" + , "foo = {!!}" ] + assert "injects the real import" + ("open import AgdaDojang.Debug" `elem` T.lines (ensureDebugImport s)) + + , runTest "ensureDebugImport: 'where' in a header comment does not misplace the import" $ do + let inp = [ "module M" + , " {a : Level} -- a level where needed" + , " (X : Set a)" + , " where" + , "foo = {!!}" ] + out = T.lines (ensureDebugImport (T.unlines inp)) + r1 <- assert "header block is intact" (take 4 out == take 4 inp) + case r1 of + Fail m -> pure (Fail m) + Pass -> assert "import sits just after the real where" + (length out > 4 && out !! 4 == "open import AgdaDojang.Debug") ] @@ -316,7 +355,8 @@ corpusTests = do -- 1. agda binary is on PATH -- 2. fixture file exists -- 3. agda-dojang libraries file exists --- Returns Just AgdaConfig if everything is available, Nothing otherwise. +-- Returns @Just (cfg, fixturePath, repoRoot)@ if everything is available, +-- @Nothing@ otherwise. probeAgdaEnv :: IO (Maybe (AgdaConfig, FilePath, FilePath)) probeAgdaEnv = do mAgda <- findExecutable "agda" @@ -445,7 +485,7 @@ hierIntegrationTests cfg repoRoot = do else do hPutStrLn stderr "\n── Integration tests (tier 2b: library-embedded module, #66) ──" - before <- TIO.readFile useFile + before <- BS.readFile useFile results <- sequence [ runTest "get_goal: Proofs.Use (hierarchical) returns a non-empty goal" $ do let params = GetGoalParams { ggFilePath = useFile, ggHoleIndex = 0 } @@ -480,9 +520,10 @@ hierIntegrationTests cfg repoRoot = do Right fr -> assertEqual "status" FillTypeError (frStatus fr) ] -- The transiently-patched source must be restored byte-for-byte. - after <- TIO.readFile useFile + after <- BS.readFile useFile restored <- runTest "get_goal/fill_hole restore the source file exactly" $ - assert "file should be unchanged after in-place tools" (before == after) + assert "file should be byte-for-byte unchanged after in-place tools" + (before == after) pure (results <> [restored]) From baa53d90c0af45e8ce526a26332a0e797f1c55d5 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 24 Jul 2026 06:00:59 +0000 Subject: [PATCH 3/5] [agda-mcp] review follow-up: graceful UTF-8 decode + declared module 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 Claude-Session: https://claude.ai/code/session_011ZxeUxJHyQsF9p2DjpCHct --- agda-mcp/src/AgdaMCP/Tools/ProofState.hs | 137 ++++++++++++++--------- agda-mcp/test/Main.hs | 23 +++- 2 files changed, 104 insertions(+), 56 deletions(-) diff --git a/agda-mcp/src/AgdaMCP/Tools/ProofState.hs b/agda-mcp/src/AgdaMCP/Tools/ProofState.hs index c9b54b5..72e3d62 100644 --- a/agda-mcp/src/AgdaMCP/Tools/ProofState.hs +++ b/agda-mcp/src/AgdaMCP/Tools/ProofState.hs @@ -40,18 +40,20 @@ module AgdaMCP.Tools.ProofState , handleGetDiagnostics -- * Exposed for testing , ensureDebugImport + , moduleNameOf ) where import Control.Exception (bracket_) import qualified Data.ByteString as BS -import Data.List (findIndex) +import Data.List (find, findIndex) import Data.Text (Text) import qualified Data.Text as T import qualified Data.Text.Encoding as TE +import Data.Text.Encoding.Error (UnicodeException) import qualified Data.Text.IO as TIO import System.Directory (makeAbsolute) -import System.FilePath (takeDirectory, takeBaseName) +import System.FilePath (takeDirectory) import AgdaMCP.Agda ( AgdaConfig, AgdaResult (..), agdaFlags, debugLog @@ -77,30 +79,33 @@ handleGetGoal :: AgdaConfig -> GetGoalParams -> IO (Either Text GoalInfo) handleGetGoal cfg params = do absPath <- makeAbsolute (ggFilePath params) origBytes <- BS.readFile absPath - let src = TE.decodeUtf8 origBytes - withImport = ensureDebugImport src - case injectReportExpr cfg (ggHoleIndex params) withImport of - Nothing -> pure . Left $ - "Hole index " <> T.pack (show (ggHoleIndex params)) - <> " not found in " <> T.pack absPath - Just patched -> do - result <- runInPlace cfg absPath origBytes patched - -- DEBUG: show what Agda actually returned - debugLog cfg $ "get_goal: exit=" <> T.pack (show (arExitCode result)) - debugLog cfg $ "get_goal stdout: " <> T.take 500 (arStdout result) - debugLog cfg $ "get_goal stderr: " <> T.take 500 (arStderr result) - -- Agda may emit markers on stdout or stderr; check both. - let combined = arStdout result <> "\n" <> arStderr result - case parseGoalContext combined of + case TE.decodeUtf8' origBytes of + Left err -> pure (Left (decodeError absPath err)) + Right src -> + case injectReportExpr cfg (ggHoleIndex params) (ensureDebugImport src) of Nothing -> pure . Left $ - "Could not parse goal/context markers from Agda output.\n" - <> "output:\n" <> T.take 2000 combined - Just (goal, ctx) -> - pure . Right $ GoalInfo - { giGoal = goal - , giContext = ctx - , giModule = Just . T.pack . takeBaseName $ ggFilePath params - } + "Hole index " <> T.pack (show (ggHoleIndex params)) + <> " not found in " <> T.pack absPath + Just patched -> do + result <- runInPlace cfg absPath origBytes patched + -- DEBUG: show what Agda actually returned + debugLog cfg $ "get_goal: exit=" <> T.pack (show (arExitCode result)) + debugLog cfg $ "get_goal stdout: " <> T.take 500 (arStdout result) + debugLog cfg $ "get_goal stderr: " <> T.take 500 (arStderr result) + -- Agda may emit markers on stdout or stderr; check both. + let combined = arStdout result <> "\n" <> arStderr result + case parseGoalContext combined of + Nothing -> pure . Left $ + "Could not parse goal/context markers from Agda output.\n" + <> "output:\n" <> T.take 2000 combined + Just (goal, ctx) -> + pure . Right $ GoalInfo + { giGoal = goal + , giContext = ctx + -- The declared module name (e.g. FLRP.Bridge), parsed from the + -- header — not the file's base name. + , giModule = moduleNameOf src + } -- --------------------------------------------------------------------------- @@ -117,36 +122,38 @@ handleFillHole :: AgdaConfig -> FillHoleParams -> IO (Either Text FillResult) handleFillHole cfg params = do absPath <- makeAbsolute (fhFilePath params) origBytes <- BS.readFile absPath - let src = TE.decodeUtf8 origBytes - case substituteHole (fhHoleIndex params) (fhCandidate params) src of - Nothing -> pure . Left $ - "Hole index " <> T.pack (show (fhHoleIndex params)) - <> " not found in " <> T.pack (fhFilePath params) - Just patched -> do - result <- runInPlace cfg absPath origBytes patched - -- Agda 2.8.0 emits some errors on stdout; check both streams. - let combined = arStdout result <> "\n" <> arStderr result - -- A non-zero exit is acceptable if the *only* errors are unsolved - -- interaction metas (from other holes we haven't filled yet). - -- This mirrors agent_bridge.py's _only_unsolved_metas logic. - onlyMetas = arExitCode result /= 0 - && "[UnsolvedInteractionMetas]" `T.isInfixOf` combined - && not ("[GenericDocError]" `T.isInfixOf` combined) - && not ("[UnequalTerms]" `T.isInfixOf` combined) - && not ("[TypeMismatch]" `T.isInfixOf` combined) - && not ("[ModuleNameDoesntMatchFileName]" `T.isInfixOf` combined) - status = if arExitCode result == 0 || onlyMetas then FillOk else FillTypeError - msg = if status == FillOk - then Nothing - else Just (T.take 2000 combined) - -- Count remaining holes in the patched source after substitution. - remainingHoles = length (findHoles patched) - pure . Right $ FillResult - { frStatus = status - , frCandidate = fhCandidate params - , frMessage = msg - , frRemainingHoles = Just remainingHoles - } + case TE.decodeUtf8' origBytes of + Left err -> pure (Left (decodeError absPath err)) + Right src -> + case substituteHole (fhHoleIndex params) (fhCandidate params) src of + Nothing -> pure . Left $ + "Hole index " <> T.pack (show (fhHoleIndex params)) + <> " not found in " <> T.pack (fhFilePath params) + Just patched -> do + result <- runInPlace cfg absPath origBytes patched + -- Agda 2.8.0 emits some errors on stdout; check both streams. + let combined = arStdout result <> "\n" <> arStderr result + -- A non-zero exit is acceptable if the *only* errors are unsolved + -- interaction metas (from other holes we haven't filled yet). + -- This mirrors agent_bridge.py's _only_unsolved_metas logic. + onlyMetas = arExitCode result /= 0 + && "[UnsolvedInteractionMetas]" `T.isInfixOf` combined + && not ("[GenericDocError]" `T.isInfixOf` combined) + && not ("[UnequalTerms]" `T.isInfixOf` combined) + && not ("[TypeMismatch]" `T.isInfixOf` combined) + && not ("[ModuleNameDoesntMatchFileName]" `T.isInfixOf` combined) + status = if arExitCode result == 0 || onlyMetas then FillOk else FillTypeError + msg = if status == FillOk + then Nothing + else Just (T.take 2000 combined) + -- Count remaining holes in the patched source after substitution. + remainingHoles = length (findHoles patched) + pure . Right $ FillResult + { frStatus = status + , frCandidate = fhCandidate params + , frMessage = msg + , frRemainingHoles = Just remainingHoles + } -- --------------------------------------------------------------------------- @@ -284,6 +291,26 @@ splitAfterModuleHeader ls = do stripLineComment :: Text -> Text stripLineComment = fst . T.breakOn "--" +-- | moduleNameOf: the declared top-level module name, parsed from the @module …@ +-- header line (with any line comment stripped). This is the *declared* name — e.g. +-- @FLRP.Bridge@ — not the file's base name, which would mangle a hierarchical module +-- to its last segment and strip only one extension from a literate @.lagda.md@ file. +-- Returns @Nothing@ when no @module@ header is found. +moduleNameOf :: Text -> Maybe Text +moduleNameOf src = do + hdr <- find (\l -> "module" `T.isPrefixOf` T.stripStart (stripLineComment l)) (T.lines src) + case dropWhile (/= "module") (T.words (stripLineComment hdr)) of + (_ : name : _) -> Just name + _ -> Nothing + +-- | decodeError: a structured error for a file whose bytes are not valid UTF-8. Agda +-- source is required to be UTF-8, so this should not arise in practice, but returning a +-- 'Left' is friendlier than letting a 'UnicodeException' escape the tool call. +decodeError :: FilePath -> UnicodeException -> Text +decodeError path err = + "Could not decode " <> T.pack path <> " as UTF-8 (Agda source must be UTF-8): " + <> T.pack (show err) + -- | parseDiagnostics: parse Agda stderr into a list of diagnostics. -- diff --git a/agda-mcp/test/Main.hs b/agda-mcp/test/Main.hs index 9736cfb..40d35ae 100644 --- a/agda-mcp/test/Main.hs +++ b/agda-mcp/test/Main.hs @@ -46,7 +46,7 @@ import AgdaMCP.Agda import AgdaMCP.Corpus (loadCorpus, searchByName, searchByType, getDeps) import AgdaMCP.Tools.ProofState ( handleGetGoal, handleFillHole, handleCheckFile, handleGetDiagnostics - , ensureDebugImport ) + , ensureDebugImport, moduleNameOf ) import AgdaMCP.Tools.Search ( handleSearchByName, handleSearchByType, handleGetDependencies ) import AgdaMCP.Types @@ -220,6 +220,20 @@ pureTests = do Fail m -> pure (Fail m) Pass -> assert "import sits just after the real where" (length out > 4 && out !! 4 == "open import AgdaDojang.Debug") + + -- moduleNameOf: the goal's `module` field is the declared name, not the base name. + , runTest "moduleNameOf: hierarchical name from the header" $ + assertEqual "name" (Just "FLRP.Bridge") + (moduleNameOf (T.unlines [ "module FLRP.Bridge where", "foo = {!!}" ])) + + , runTest "moduleNameOf: parameterised header, comment ignored" $ + assertEqual "name" (Just "M") + (moduleNameOf (T.unlines + [ "module M {a : Level} where -- not FLRP.Bridge", "x = {!!}" ])) + + , runTest "moduleNameOf: no header → Nothing" $ + assertEqual "name" Nothing + (moduleNameOf (T.unlines [ "-- just a comment", "x = 1" ])) ] @@ -494,6 +508,13 @@ hierIntegrationTests cfg repoRoot = do Left err -> pure (Fail $ "get_goal failed: " <> T.unpack err) Right info -> assert "goal should be non-empty" (not . T.null $ giGoal info) + , runTest "get_goal: Proofs.Use reports its declared (hierarchical) module name" $ do + let params = GetGoalParams { ggFilePath = useFile, ggHoleIndex = 0 } + result <- handleGetGoal hierCfg params + case result of + Left err -> pure (Fail $ "get_goal failed: " <> T.unpack err) + Right info -> assertEqual "module" (Just "Proofs.Use") (giModule info) + , runTest "get_goal: Proofs.Use context contains 'x' (Debug import injected)" $ do let params = GetGoalParams { ggFilePath = useFile, ggHoleIndex = 0 } result <- handleGetGoal hierCfg params From 7ffbbfa1c2ce937d6ca89033fbe562e50ca05a63 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Fri, 24 Jul 2026 00:17:21 -0600 Subject: [PATCH 4/5] Potential fix for pull request finding Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> Signed-off-by: William DeMeo --- agda-mcp/src/AgdaMCP/Tools/ProofState.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/agda-mcp/src/AgdaMCP/Tools/ProofState.hs b/agda-mcp/src/AgdaMCP/Tools/ProofState.hs index 72e3d62..0643b7f 100644 --- a/agda-mcp/src/AgdaMCP/Tools/ProofState.hs +++ b/agda-mcp/src/AgdaMCP/Tools/ProofState.hs @@ -236,7 +236,7 @@ runInPlace cfg absPath originalBytes patched = cfgInPlace = cfg { agdaFlags = agdaFlags cfg <> ["-i", takeDirectory absPath] } --- | ensureDebugImport: guarantee @open import AgdaDojang.Debug@ is in scope. +-- | ensureDebugImport: ensure @open import AgdaDojang.Debug@ is in scope (best-effort). -- -- The @reportGoalCtx@ macro get_goal injects lives in @AgdaDojang.Debug@; a library -- file being inspected will not normally import it. If the module already imports it From 1920b092143b538bcd331817bd40b37017cce2ef Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 24 Jul 2026 06:33:17 +0000 Subject: [PATCH 5/5] [agda-mcp] review follow-up: top-level-only import scan; document mtime 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 Claude-Session: https://claude.ai/code/session_011ZxeUxJHyQsF9p2DjpCHct --- agda-mcp/src/AgdaMCP/Tools/ProofState.hs | 47 ++++++++++++++++-------- agda-mcp/test/Main.hs | 14 +++++++ 2 files changed, 46 insertions(+), 15 deletions(-) diff --git a/agda-mcp/src/AgdaMCP/Tools/ProofState.hs b/agda-mcp/src/AgdaMCP/Tools/ProofState.hs index 0643b7f..5497f13 100644 --- a/agda-mcp/src/AgdaMCP/Tools/ProofState.hs +++ b/agda-mcp/src/AgdaMCP/Tools/ProofState.hs @@ -226,6 +226,14 @@ handleGetDiagnostics cfg params = do -- round-trip is involved. Checking at the real path (rather than a scratch copy) is -- what lets hierarchically-named library modules resolve — see the module header and -- issue #66. +-- +-- Only the file's /contents/ are restored, not its modification time: the restore write +-- deliberately leaves a fresh mtime. That is intentional — a newer mtime forces Agda to +-- re-typecheck from the restored source on its next load under any interface-freshness +-- rule, whereas resetting mtime to the original (older) value could let Agda reuse an +-- @.agdai@ built from the transiently-patched content (e.g. a fill_hole candidate that +-- completed the module). Editors that compare content, not mtime alone, will not prompt, +-- since the bytes are unchanged. runInPlace :: AgdaConfig -> FilePath -> BS.ByteString -> Text -> IO AgdaResult runInPlace cfg absPath originalBytes patched = bracket_ @@ -236,31 +244,40 @@ runInPlace cfg absPath originalBytes patched = cfgInPlace = cfg { agdaFlags = agdaFlags cfg <> ["-i", takeDirectory absPath] } --- | ensureDebugImport: ensure @open import AgdaDojang.Debug@ is in scope (best-effort). +-- | ensureDebugImport: ensure @open import AgdaDojang.Debug@ is in scope at the top +-- level (best-effort). -- -- The @reportGoalCtx@ macro get_goal injects lives in @AgdaDojang.Debug@; a library --- file being inspected will not normally import it. If the module already imports it --- this is a no-op; otherwise the import is inserted immediately after the module --- header — i.e. after the header's closing @where@, which may be several lines below --- the @module@ keyword when the module is parameterised (common in agda-algebras). +-- file being inspected will not normally import it. If the top-level module already +-- imports it this is a no-op; otherwise the import is inserted immediately after the +-- module header — i.e. after the header's closing @where@, which may be several lines +-- below the @module@ keyword when the module is parameterised (common in agda-algebras). -- Placing it there is valid for both @.agda@ and literate @.lagda.md@ sources, since -- the header sits in code context in both. agda-dojang is on the library path -- (@-l agda-dojang@), so the import resolves. -- --- Both the "already imported?" test and the header search look at real import/module --- lines (not mere substrings), so a passing mention of @AgdaDojang.Debug@ or @module@ --- in a comment neither suppresses the injection nor misplaces it. +-- The "already imported?" scan is restricted to the *top-level* prelude — the lines +-- after the top-level module header, up to the first nested @module@ — so an import +-- inside a nested module (which does not bring names into the surrounding scope) does +-- not suppress injection. Both that scan and the header search look at real +-- import/module lines (not mere substrings), so a passing mention of @AgdaDojang.Debug@ +-- or @module@ in a comment neither suppresses the injection nor misplaces it. When no +-- @module … where@ header is found the source is returned unchanged (get_goal then +-- surfaces the resulting scope error), so injection is best-effort, not guaranteed. 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) +ensureDebugImport src = + case splitAfterModuleHeader ls of + Nothing -> src -- no top-level module header found; leave as-is (best-effort) + Just (hdr, rest) + | any isDebugImportLine (takeWhile (not . startsModule) rest) -> src + | otherwise -> T.unlines (hdr <> ["open import AgdaDojang.Debug"] <> rest) where ls = T.lines src + -- A nested `module …` line ends the top-level prelude; imports below it are not in + -- the surrounding scope, so they must not count as "already imported". + startsModule l = "module" `T.isPrefixOf` T.stripStart (stripLineComment l) + -- A genuine import of the module: with any line comment stripped, the first -- token is an import-introducing keyword, @import@ is present, and -- @AgdaDojang.Debug@ appears as a whole module token — so none of a comment diff --git a/agda-mcp/test/Main.hs b/agda-mcp/test/Main.hs index 40d35ae..42ba467 100644 --- a/agda-mcp/test/Main.hs +++ b/agda-mcp/test/Main.hs @@ -221,6 +221,20 @@ pureTests = do Pass -> assert "import sits just after the real where" (length out > 4 && out !! 4 == "open import AgdaDojang.Debug") + , runTest "ensureDebugImport: a nested-module import does not suppress injection" $ do + let s = T.unlines + [ "module Top where" + , "module Inner where" + , " open import AgdaDojang.Debug" + , "foo = {!!}" ] + out = T.lines (ensureDebugImport s) + r1 <- assert "injects at top level, right after the header" + (length out > 1 && out !! 1 == "open import AgdaDojang.Debug") + case r1 of + Fail m -> pure (Fail m) + Pass -> assert "the nested import is left in place" + (" open import AgdaDojang.Debug" `elem` out) + -- moduleNameOf: the goal's `module` field is the declared name, not the base name. , runTest "moduleNameOf: hierarchical name from the header" $ assertEqual "name" (Just "FLRP.Bridge")