From 3f360ab6435470992d6438b1cd3a54d7dc2fbaeb Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 16 Dec 2025 17:19:11 +0000 Subject: [PATCH 01/12] Switch from mcp-server to Tritlo/mcp library - Update flake.nix to use github:Tritlo/mcp source - Update dependencies in agda-mcp.cabal (mcp >= 0.3.0.0) - Rewrite Main.hs to use MCPServer typeclass API - Update Server.hs handlers to use new MCP.Types - Update test files to use new Content/TextContent patterns --- Main.hs | 476 +++++++++++++++++++++++++--- agda-mcp.cabal | 12 +- flake.nix | 8 +- src/AgdaMCP/Server.hs | 50 +-- test/AgdaMCP/EditPersistenceSpec.hs | 4 +- test/AgdaMCP/MultiAgentSpec.hs | 10 +- test/AgdaMCP/ServerSpec.hs | 14 +- 7 files changed, 494 insertions(+), 80 deletions(-) diff --git a/Main.hs b/Main.hs index b3e8a53..c636722 100644 --- a/Main.hs +++ b/Main.hs @@ -1,48 +1,452 @@ {-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE DuplicateRecordFields #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} +{-# OPTIONS_GHC -Wno-orphans #-} module Main where -import MCP.Server -import MCP.Server.Derive +import Control.Monad.IO.Class (liftIO) +import Data.Aeson (Value, toJSON) +import qualified Data.Aeson as JSON +import Data.IORef +import qualified Data.Map.Strict as Map +import Data.Text (Text) import System.IO (hSetEncoding, stderr, stdout, utf8, hPutStrLn) +import System.IO.Unsafe (unsafePerformIO) + +import MCP.Protocol +import MCP.Server +import MCP.Server.HTTP +import MCP.Types import AgdaMCP.Server import AgdaMCP.Types +import qualified AgdaMCP.SessionManager as SessionManager + +-- | Use IORef for global session manager +{-# NOINLINE globalSessionManagerRef #-} +globalSessionManagerRef :: IORef (Maybe (SessionManager.SessionManager ServerState)) +globalSessionManagerRef = unsafePerformIO $ newIORef Nothing + +setGlobalSessionManager :: SessionManager.SessionManager ServerState -> IO () +setGlobalSessionManager mgr = writeIORef globalSessionManagerRef (Just mgr) + +getGlobalSessionManager :: IO (SessionManager.SessionManager ServerState) +getGlobalSessionManager = do + mMgr <- readIORef globalSessionManagerRef + case mMgr of + Just mgr -> return mgr + Nothing -> error "Session manager not initialized" + +-- | Instance of MCPServer for our Agda MCP Server +-- We need to use MCPServerM monad for the implementation +instance MCPServer MCPServerM where + handleListTools _params = do + let tools = agdaTools + return $ ListToolsResult + { tools = tools + , nextCursor = Nothing + , _meta = Nothing + } + + handleCallTool CallToolParams{name = toolName, arguments = mArgs} = do + result <- liftIO $ do + -- Get session manager from global state + manager <- getGlobalSessionManager + let args = maybe Map.empty id mArgs + callAgdaTool manager toolName args + return result + + -- Resources - use default implementations for now + handleListResources _params = do + return $ ListResourcesResult + { resources = agdaResources + , nextCursor = Nothing + , _meta = Nothing + } + + handleReadResource ReadResourceParams{uri = resourceUri} = do + result <- liftIO $ do + manager <- getGlobalSessionManager + readAgdaResource manager resourceUri + return result + + -- Prompts - not implemented yet + handleListPrompts _params = return $ ListPromptsResult + { prompts = [] + , nextCursor = Nothing + , _meta = Nothing + } + + handleGetPrompt _params = return $ GetPromptResult + { messages = [] + , description = Nothing + , _meta = Nothing + } + + -- Other handlers use defaults + handleSetLevel _params = liftIO $ putStrLn "Log level set" + +-- | Define the Agda tools list for the MCP protocol +agdaTools :: [Tool] +agdaTools = + [ mkTool "agda_load" "Load and type-check an Agda file" + [("file", "string", "Path to the Agda file", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_get_goals" "List all goals/holes in the currently loaded file" + [("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_get_goal_type" "Get the type of a specific goal" + [("goalId", "integer", "The numeric ID of the goal/hole (starting from 0)", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_get_goal_type_implicits" "Get the type of a specific goal with implicit arguments shown" + [("goalId", "integer", "The numeric ID of the goal/hole (starting from 0)", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_get_context" "Get the context (available variables and their types) at a goal" + [("goalId", "integer", "The numeric ID of the goal/hole (starting from 0)", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_get_context_implicits" "Get the context at a goal with implicit arguments shown" + [("goalId", "integer", "The numeric ID of the goal/hole (starting from 0)", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_give" "Fill a goal/hole with an expression" + [("goalId", "integer", "The numeric ID of the goal/hole", True) + ,("expression", "string", "Agda expression to use", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_refine" "Refine a goal with a constructor or function, introducing new sub-goals" + [("goalId", "integer", "The numeric ID of the goal/hole", True) + ,("expression", "string", "Agda expression to refine with", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_case_split" "Split a goal by pattern matching on a variable" + [("goalId", "integer", "The numeric ID of the goal/hole", True) + ,("variable", "string", "Name of the variable to case-split on", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_compute" "Parse and display an expression in a goal's context" + [("goalId", "integer", "The numeric ID of the goal/hole", True) + ,("expression", "string", "Agda expression to compute", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_infer_type" "Infer the type of an expression in a goal's context" + [("goalId", "integer", "The numeric ID of the goal/hole", True) + ,("expression", "string", "Agda expression to infer type for", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_intro" "Introduce variables using the intro tactic" + [("goalId", "integer", "The numeric ID of the goal/hole", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_auto" "Attempt automatic proof search to fill a goal" + [("goalId", "integer", "The numeric ID of the goal/hole", True) + ,("timeout", "integer", "Optional timeout in milliseconds", False) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_auto_all" "Attempt automatic proof search on all goals" + [("timeout", "integer", "Optional timeout in milliseconds", False) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_solve_one" "Attempt to solve a specific goal using Agda's constraint solver" + [("goalId", "integer", "The numeric ID of the goal/hole", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_helper_function" "Generate a helper function skeleton for a goal" + [("goalId", "integer", "The numeric ID of the goal/hole", True) + ,("helperName", "string", "Suggested name for the helper function", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_goal_type_context" "Get both the goal type and context together" + [("goalId", "integer", "The numeric ID of the goal/hole", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_goal_at_position" "Find which goal exists at a specific file position" + [("file", "string", "Path to the Agda file", True) + ,("line", "integer", "Line number (1-indexed)", True) + ,("column", "integer", "Column number (1-indexed)", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_goto_definition" "Navigate to the definition of a symbol at a specific position" + [("file", "string", "Path to the Agda file", True) + ,("line", "integer", "Line number (1-indexed)", True) + ,("column", "integer", "Column number (1-indexed)", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_search_about" "Search for definitions by name or type signature" + [("query", "string", "Search query", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_show_module" "Show the contents of a module" + [("moduleName", "string", "Fully qualified module name", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_show_constraints" "Show all unsolved type-checking constraints" + [("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_why_in_scope" "Look up documentation and scope information for a name" + [("name", "string", "Name to look up", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + , mkTool "agda_list_postulates" "List all postulates in a file" + [("file", "string", "Path to the Agda file", True) + ,("sessionId", "string", "Optional session ID for multi-agent isolation", False) + ,("format", "string", "Response format: Concise (default) or Full", False) + ] + ] + +-- | Helper to create a tool definition +mkTool :: Text -> Text -> [(Text, Text, Text, Bool)] -> Tool +mkTool toolName desc params = Tool + { name = toolName + , title = Nothing + , description = Just desc + , inputSchema = InputSchema + { schemaType = "object" + , properties = Just $ Map.fromList + [(pName, toJSON $ Map.fromList + [ ("type" :: Text, JSON.String pType) + , ("description", JSON.String pDesc) + ]) | (pName, pType, pDesc, _) <- params] + , required = Just [pName | (pName, _, _, True) <- params] + } + , outputSchema = Nothing + , annotations = Nothing + , _meta = Nothing + } + +-- | Define Agda resources +agdaResources :: [Resource] +agdaResources = + [ Resource + { uri = "agda://goals" + , name = "goals" + , title = Just "Agda Goals" + , description = Just "List of all goals in the currently loaded Agda file" + , mimeType = Just "application/json" + , size = Nothing + , annotations = Nothing + , _meta = Nothing + } + , Resource + { uri = "agda://file-context" + , name = "file-context" + , title = Just "File Context" + , description = Just "Overall context and scope information for the loaded file" + , mimeType = Just "application/json" + , size = Nothing + , annotations = Nothing + , _meta = Nothing + } + ] + +-- | Call an Agda tool based on name and arguments +callAgdaTool :: SessionManager.SessionManager ServerState -> Text -> Map.Map Text Value -> IO CallToolResult +callAgdaTool manager toolName args = do + -- Parse tool and call handler + mTool <- parseAgdaTool toolName args + case mTool of + Nothing -> return $ CallToolResult + { content = [TextContentType $ TextContent "text" ("Unknown tool: " <> toolName) Nothing Nothing] + , structuredContent = Nothing + , isError = Just True + , _meta = Nothing + } + Just tool -> do + result <- handleAgdaToolWithSession manager tool + return $ CallToolResult + { content = [result] + , structuredContent = Nothing + , isError = Nothing + , _meta = Nothing + } + +-- | Parse tool name and arguments to AgdaTool +parseAgdaTool :: Text -> Map.Map Text Value -> IO (Maybe AgdaTool) +parseAgdaTool toolName args = do + let sessionId = getTextArg "sessionId" args + format = getTextArg "format" args + + return $ case toolName of + "agda_load" -> do + file <- getTextArg "file" args + Just $ AgdaLoad file sessionId format + "agda_get_goals" -> + Just $ AgdaGetGoals sessionId format + "agda_get_goal_type" -> do + goalId <- getIntArg "goalId" args + Just $ AgdaGetGoalType goalId sessionId format + "agda_get_goal_type_implicits" -> do + goalId <- getIntArg "goalId" args + Just $ AgdaGetGoalTypeImplicits goalId sessionId format + "agda_get_context" -> do + goalId <- getIntArg "goalId" args + Just $ AgdaGetContext goalId sessionId format + "agda_get_context_implicits" -> do + goalId <- getIntArg "goalId" args + Just $ AgdaGetContextImplicits goalId sessionId format + "agda_give" -> do + goalId <- getIntArg "goalId" args + expression <- getTextArg "expression" args + Just $ AgdaGive goalId expression sessionId format + "agda_refine" -> do + goalId <- getIntArg "goalId" args + expression <- getTextArg "expression" args + Just $ AgdaRefine goalId expression sessionId format + "agda_case_split" -> do + goalId <- getIntArg "goalId" args + variable <- getTextArg "variable" args + Just $ AgdaCaseSplit goalId variable sessionId format + "agda_compute" -> do + goalId <- getIntArg "goalId" args + expression <- getTextArg "expression" args + Just $ AgdaCompute goalId expression sessionId format + "agda_infer_type" -> do + goalId <- getIntArg "goalId" args + expression <- getTextArg "expression" args + Just $ AgdaInferType goalId expression sessionId format + "agda_intro" -> do + goalId <- getIntArg "goalId" args + Just $ AgdaIntro goalId sessionId format + "agda_auto" -> do + goalId <- getIntArg "goalId" args + let timeout = getIntArg "timeout" args + Just $ AgdaAuto goalId timeout sessionId format + "agda_auto_all" -> do + let timeout = getIntArg "timeout" args + Just $ AgdaAutoAll timeout sessionId format + "agda_solve_one" -> do + goalId <- getIntArg "goalId" args + Just $ AgdaSolveOne goalId sessionId format + "agda_helper_function" -> do + goalId <- getIntArg "goalId" args + helperName <- getTextArg "helperName" args + Just $ AgdaHelperFunction goalId helperName sessionId format + "agda_goal_type_context" -> do + goalId <- getIntArg "goalId" args + Just $ AgdaGoalTypeContext goalId sessionId format + "agda_goal_at_position" -> do + file <- getTextArg "file" args + line <- getIntArg "line" args + column <- getIntArg "column" args + Just $ AgdaGoalAtPosition file line column sessionId format + "agda_goto_definition" -> do + file <- getTextArg "file" args + line <- getIntArg "line" args + column <- getIntArg "column" args + Just $ AgdaGotoDefinition file line column sessionId format + "agda_search_about" -> do + query <- getTextArg "query" args + Just $ AgdaSearchAbout query sessionId format + "agda_show_module" -> do + moduleName <- getTextArg "moduleName" args + Just $ AgdaShowModule moduleName sessionId format + "agda_show_constraints" -> + Just $ AgdaShowConstraints sessionId format + "agda_why_in_scope" -> do + nameArg <- getTextArg "name" args + Just $ AgdaWhyInScope nameArg sessionId format + "agda_list_postulates" -> do + file <- getTextArg "file" args + Just $ AgdaListPostulates file sessionId format + _ -> Nothing + +-- | Get a text argument from the map +getTextArg :: Text -> Map.Map Text Value -> Maybe Text +getTextArg key args = case Map.lookup key args of + Just (JSON.String s) -> Just s + _ -> Nothing + +-- | Get an integer argument from the map +getIntArg :: Text -> Map.Map Text Value -> Maybe Int +getIntArg key args = case Map.lookup key args of + Just (JSON.Number n) -> Just (floor n) + _ -> Nothing + +-- | Read an Agda resource +readAgdaResource :: SessionManager.SessionManager ServerState -> Text -> IO ReadResourceResult +readAgdaResource _manager _resourceUri = do + -- For now, return empty result - resources need more implementation + return $ ReadResourceResult + { contents = [] + , _meta = Nothing + } main :: IO () main = do - -- Set UTF-8 encoding for proper Unicode handling - hSetEncoding stdout utf8 - hSetEncoding stderr utf8 - - hPutStrLn stderr "Starting Agda MCP Server on http://localhost:3000/mcp" - hPutStrLn stderr "Session isolation enabled: pass 'sessionId' parameter for multi-agent support" - - -- Initialize session manager (replaces single server state) - sessionManager <- initSessionManager - - -- Define handlers that close over sessionManager - let handleTool :: AgdaTool -> IO Content - handleTool = handleAgdaToolWithSession sessionManager - - handleResource :: URI -> AgdaResource -> IO ResourceContent - handleResource = handleAgdaResourceWithSession sessionManager - - -- Derive MCP handlers using Template Haskell - tools = $(deriveToolHandlerWithDescription ''AgdaTool 'handleTool agdaToolDescriptions) - resources = $(deriveResourceHandlerWithDescription ''AgdaResource 'handleResource agdaResourceDescriptions) - - in -- Run the MCP server with HTTP transport - runMcpServerHttp - McpServerInfo - { serverName = "Agda MCP Server" - , serverVersion = "1.0.0" - , serverInstructions = "A Model Context Protocol server for interactive Agda development. Provides tools for loading files, working with goals/holes, refining proofs, and exploring scope. Supports multi-agent isolation via sessionId parameter." - } - McpServerHandlers - { prompts = Nothing -- No prompts defined yet - , resources = Just resources - , tools = Just tools - } + -- Set UTF-8 encoding for proper Unicode handling + hSetEncoding stdout utf8 + hSetEncoding stderr utf8 + + hPutStrLn stderr "Starting Agda MCP Server on http://localhost:3000/mcp" + hPutStrLn stderr "Session isolation enabled: pass 'sessionId' parameter for multi-agent support" + + -- Initialize session manager + sessionManager <- initSessionManager + setGlobalSessionManager sessionManager + + let serverInfo = Implementation + { name = "Agda MCP Server" + , title = Just "Agda MCP Server" + , version = "1.0.0" + } + + let resourcesCap = ResourcesCapability + { subscribe = Just False + , listChanged = Just False + } + let promptsCap = PromptsCapability + { listChanged = Just False + } + let toolsCap = ToolsCapability + { listChanged = Just False + } + + let capabilities = ServerCapabilities + { resources = Just resourcesCap + , prompts = Just promptsCap + , tools = Just toolsCap + , completions = Nothing + , logging = Nothing + , experimental = Nothing + } + + let config = HTTPServerConfig + { httpPort = 3000 + , httpBaseUrl = "http://localhost:3000" + , httpServerInfo = serverInfo + , httpCapabilities = capabilities + , httpEnableLogging = True + , httpOAuthConfig = Nothing + , httpJWK = Nothing + , httpProtocolVersion = mcpProtocolVersion + } + + runServerHTTP config diff --git a/agda-mcp.cabal b/agda-mcp.cabal index 2572e63..5850072 100644 --- a/agda-mcp.cabal +++ b/agda-mcp.cabal @@ -30,7 +30,8 @@ library directory >= 1.3, bytestring >= 0.10, vector >= 0.12, - mcp-server >= 0.1.0.15, + mcp >= 0.3.0.0, + data-default >= 0.7, unordered-containers >= 0.2, uuid >= 1.3, stm >= 2.5, @@ -49,7 +50,11 @@ executable agda-mcp build-depends: base >= 4.14 && < 5, agda-mcp, - mcp-server >= 0.1.0.15 + mcp >= 0.3.0.0, + data-default >= 0.7, + text >= 1.2, + aeson >= 2.0, + containers >= 0.6 default-language: Haskell2010 default-extensions: OverloadedStrings @@ -75,7 +80,8 @@ test-suite agda-mcp-tests vector >= 0.12, filepath >= 1.4, directory >= 1.3, - mcp-server >= 0.1.0.15, + mcp >= 0.3.0.0, + containers >= 0.6, async >= 2.2, random >= 1.2 hs-source-dirs: test diff --git a/flake.nix b/flake.nix index 13bfe5a..3dece4d 100644 --- a/flake.nix +++ b/flake.nix @@ -3,7 +3,7 @@ nixpkgs.url = "github:nixos/nixpkgs/e643668fd71b949c53f8626614b21ff71a07379d"; flake-parts.url = "github:hercules-ci/flake-parts"; haskell-flake.url = "github:srid/haskell-flake"; - mcp-server-hs = { url = "github:drshade/haskell-mcp-server"; flake = false; }; + mcp = { url = "github:Tritlo/mcp"; flake = false; }; }; outputs = inputs@{ self, nixpkgs, flake-parts, ... }: flake-parts.lib.mkFlake { inherit inputs; } { @@ -26,11 +26,7 @@ # (defined by `defaults.packages` option). # packages = { - mcp-server.source = pkgs.applyPatches { - name = "mcp-server-patched"; - src = inputs.mcp-server-hs; - patches = [ ./patches/mcp-server-header-optional.patch ]; - }; + mcp.source = inputs.mcp; # aeson.source = "1.5.0.0"; # Override aeson to a custom version from Hackage # shower.source = inputs.shower; # Override shower to a custom source path }; diff --git a/src/AgdaMCP/Server.hs b/src/AgdaMCP/Server.hs index 3ded240..88f636d 100644 --- a/src/AgdaMCP/Server.hs +++ b/src/AgdaMCP/Server.hs @@ -42,7 +42,7 @@ import System.FilePath (takeDirectory) import System.Directory (listDirectory) -- MCP Server library -import qualified MCP.Server +import MCP.Types (Content, TextContent(..), TextContentType(..), TextResourceContents(..), ResourceContents(..)) import qualified AgdaMCP.Types import qualified AgdaMCP.Repl as Repl import qualified AgdaMCP.SessionManager as SessionManager @@ -884,9 +884,13 @@ initServerState = do putStrLn "Persistent REPL started" pure stateRef +-- | Helper to create a text content response +mkTextContent :: Text -> Content +mkTextContent txt = TextContentType $ TextContent "text" txt Nothing Nothing + -- MCP Tool Handler - routes commands through persistent REPL -- This will be called by the mcp-server library when a tool is invoked -handleAgdaTool :: IORef ServerState -> AgdaMCP.Types.AgdaTool -> IO MCP.Server.Content +handleAgdaTool :: IORef ServerState -> AgdaMCP.Types.AgdaTool -> IO Content handleAgdaTool stateRef tool = do -- Special handling for tools that need custom logic (don't use REPL) case tool of @@ -894,34 +898,34 @@ handleAgdaTool stateRef tool = do -- Run directly in TCM (not through REPL) result <- runTCMTop $ mcpListPostulates stateRef (T.unpack file) case result of - Left err -> pure $ MCP.Server.ContentText $ "Error: " <> T.pack (show err) + Left err -> pure $ mkTextContent $ "Error: " <> T.pack (show err) Right (AgdaResult _ _ (Just val)) -> do let responseFormat = Format.getFormat tool let responseText = Format.formatResponse responseFormat val - pure $ MCP.Server.ContentText responseText - Right _ -> pure $ MCP.Server.ContentText "No postulates found" + pure $ mkTextContent responseText + Right _ -> pure $ mkTextContent "No postulates found" AgdaMCP.Types.AgdaGoalAtPosition{file, line, column} -> do -- Run directly in TCM to find goal at position result <- runTCMTop $ mcpGoalAtPosition stateRef (T.unpack file) line column case result of - Left err -> pure $ MCP.Server.ContentText $ "Error: " <> T.pack (show err) + Left err -> pure $ mkTextContent $ "Error: " <> T.pack (show err) Right (AgdaResult _ _ (Just val)) -> do let responseFormat = Format.getFormat tool let responseText = Format.formatResponse responseFormat val - pure $ MCP.Server.ContentText responseText - Right (AgdaResult _ msg Nothing) -> pure $ MCP.Server.ContentText msg + pure $ mkTextContent responseText + Right (AgdaResult _ msg Nothing) -> pure $ mkTextContent msg AgdaMCP.Types.AgdaGotoDefinition{file, line, column} -> do -- Run directly in TCM to find definition at position result <- runTCMTop $ mcpGotoDefinition stateRef (T.unpack file) line column case result of - Left err -> pure $ MCP.Server.ContentText $ "Error: " <> T.pack (show err) + Left err -> pure $ mkTextContent $ "Error: " <> T.pack (show err) Right (AgdaResult _ _ (Just val)) -> do let responseFormat = Format.getFormat tool let responseText = Format.formatResponse responseFormat val - pure $ MCP.Server.ContentText responseText - Right (AgdaResult _ msg Nothing) -> pure $ MCP.Server.ContentText msg + pure $ mkTextContent responseText + Right (AgdaResult _ msg Nothing) -> pure $ mkTextContent msg -- All other tools go through REPL _ -> do @@ -958,11 +962,15 @@ handleAgdaTool stateRef tool = do -- Format response based on requested format (default: Concise) let responseFormat = Format.getFormat tool let responseText = Format.formatResponse responseFormat jsonValue - pure $ MCP.Server.ContentText responseText + pure $ mkTextContent responseText + +-- | Helper to create text resource contents +mkTextResource :: Text -> Text -> Maybe Text -> ResourceContents +mkTextResource resourceUri txt mimeType = TextResource $ TextResourceContents resourceUri txt mimeType Nothing -- MCP Resource Handler - exposes Agda file information as resources -- Resources extract parameters from the URI path -handleAgdaResource :: IORef ServerState -> MCP.Server.URI -> AgdaMCP.Types.AgdaResource -> IO MCP.Server.ResourceContent +handleAgdaResource :: IORef ServerState -> Text -> AgdaMCP.Types.AgdaResource -> IO ResourceContents handleAgdaResource stateRef uri resource = do result <- runTCMTop $ case resource of AgdaMCP.Types.Goals -> do @@ -983,13 +991,13 @@ handleAgdaResource stateRef uri resource = do case result of Left err -> - pure $ MCP.Server.ResourceText uri "text/plain" $ "Error: " <> T.pack (show err) + pure $ mkTextResource uri ("Error: " <> T.pack (show err)) (Just "text/plain") Right agdaRes -> case agdaResult agdaRes of Nothing -> - pure $ MCP.Server.ResourceText uri "text/plain" $ message agdaRes + pure $ mkTextResource uri (message agdaRes) (Just "text/plain") Just val -> - pure $ MCP.Server.ResourceText uri "application/json" $ TE.decodeUtf8 $ LBS.toStrict $ JSON.encode val + pure $ mkTextResource uri (TE.decodeUtf8 $ LBS.toStrict $ JSON.encode val) (Just "application/json") -- ============================================================================ -- Session-based Handlers (Multi-agent Support) @@ -1020,22 +1028,22 @@ initSessionManager = do -- | Session-aware tool handler -- Extracts sessionId from tool, gets or creates session, routes to appropriate ServerState -handleAgdaToolWithSession :: SessionManager.SessionManager ServerState -> AgdaMCP.Types.AgdaTool -> IO MCP.Server.Content +handleAgdaToolWithSession :: SessionManager.SessionManager ServerState -> AgdaMCP.Types.AgdaTool -> IO Content handleAgdaToolWithSession manager tool = do -- Extract session ID from tool (all tools now have this field) - let sessionId = AgdaMCP.Types.sessionId tool + let sessionIdVal = AgdaMCP.Types.sessionId tool -- Get or create session - stateRef <- SessionManager.getOrCreateSession manager sessionId + stateRef <- SessionManager.getOrCreateSession manager sessionIdVal -- Update last used timestamp - SessionManager.updateLastUsed manager sessionId + SessionManager.updateLastUsed manager sessionIdVal -- Route to existing handler handleAgdaTool stateRef tool -- | Session-aware resource handler -handleAgdaResourceWithSession :: SessionManager.SessionManager ServerState -> MCP.Server.URI -> AgdaMCP.Types.AgdaResource -> IO MCP.Server.ResourceContent +handleAgdaResourceWithSession :: SessionManager.SessionManager ServerState -> Text -> AgdaMCP.Types.AgdaResource -> IO ResourceContents handleAgdaResourceWithSession manager uri resource = do -- Resources don't have sessionId parameter, so use default session -- In the future, we could extract session from URI query parameters diff --git a/test/AgdaMCP/EditPersistenceSpec.hs b/test/AgdaMCP/EditPersistenceSpec.hs index c577d82..ca8c3d8 100644 --- a/test/AgdaMCP/EditPersistenceSpec.hs +++ b/test/AgdaMCP/EditPersistenceSpec.hs @@ -21,7 +21,7 @@ import Control.Exception (try, SomeException, bracket, catch) import AgdaMCP.Server import qualified AgdaMCP.Types as Types import qualified AgdaMCP.SessionManager as SessionManager -import qualified MCP.Server as MCP +import MCP.Types (Content(..), TextContent(..)) import AgdaMCP.TestUtils (withTempTestFile) -- | Simple test case type @@ -103,7 +103,7 @@ getGoalCount manager sessionId = do let tool = Types.AgdaGetGoals { Types.sessionId = Just sessionId, Types.format = Just "Full" } result <- handleAgdaToolWithSession manager tool case result of - MCP.ContentText txt -> do + TextContentType (TextContent _ txt _ _) -> do case JSON.decode (LBS.fromStrict $ TE.encodeUtf8 txt) of Just (JSON.Object obj) -> do case JSON.KeyMap.lookup (JSON.Key.fromText "info") obj of diff --git a/test/AgdaMCP/MultiAgentSpec.hs b/test/AgdaMCP/MultiAgentSpec.hs index 27a8760..6fbc3b4 100644 --- a/test/AgdaMCP/MultiAgentSpec.hs +++ b/test/AgdaMCP/MultiAgentSpec.hs @@ -25,7 +25,7 @@ import System.IO.Unsafe (unsafePerformIO) import AgdaMCP.Server import qualified AgdaMCP.Types as Types import qualified AgdaMCP.SessionManager as SessionManager -import qualified MCP.Server as MCP +import MCP.Types (Content(..), TextContent(..)) import AgdaMCP.TestUtils (withTempTestFile) -- | Simple test case type @@ -65,11 +65,11 @@ runTool manager tool = do let toolWithFullFormat = setFormat tool (Just "Full") result <- handleAgdaToolWithSession manager toolWithFullFormat case result of - MCP.ContentText txt -> do + TextContentType (TextContent _ txt _ _) -> do case JSON.decode (LBS.fromStrict $ TE.encodeUtf8 txt) of Just val -> pure val Nothing -> fail $ "Failed to parse JSON response: " ++ T.unpack txt - _ -> fail "Expected ContentText response" + _ -> fail "Expected TextContent response" -- | Helper to run a tool and get the response as Text (forces Concise format) runToolConcise :: SessionManager.SessionManager ServerState -> Types.AgdaTool -> IO Text @@ -78,8 +78,8 @@ runToolConcise manager tool = do let toolWithConciseFormat = setFormat tool (Just "Concise") result <- handleAgdaToolWithSession manager toolWithConciseFormat case result of - MCP.ContentText txt -> pure txt - _ -> fail "Expected ContentText response" + TextContentType (TextContent _ txt _ _) -> pure txt + _ -> fail "Expected TextContent response" -- | Set format on a tool (preserves sessionId) - simplified for GetGoals and other tools setFormat :: Types.AgdaTool -> Maybe Text -> Types.AgdaTool diff --git a/test/AgdaMCP/ServerSpec.hs b/test/AgdaMCP/ServerSpec.hs index 9339c1c..0a1fe8a 100644 --- a/test/AgdaMCP/ServerSpec.hs +++ b/test/AgdaMCP/ServerSpec.hs @@ -24,7 +24,7 @@ import System.Timeout (timeout) import AgdaMCP.Server import qualified AgdaMCP.Types as Types import qualified AgdaMCP.SessionManager as SessionManager -import qualified MCP.Server as MCP +import MCP.Types (Content(..), TextContent(..)) import qualified AgdaMCP.MultiAgentSpec as MultiAgent import AgdaMCP.TestUtils (withTempTestFile) @@ -65,11 +65,11 @@ runTool manager tool = do let toolWithFullFormat = setFormat tool (Just "Full") result <- handleAgdaToolWithSession manager toolWithFullFormat case result of - MCP.ContentText txt -> do + TextContentType (TextContent _ txt _ _) -> do case JSON.decode (LBS.fromStrict $ TE.encodeUtf8 txt) of Just val -> pure val Nothing -> fail $ "Failed to parse JSON response: " ++ T.unpack txt - _ -> fail "Expected ContentText response" + _ -> fail "Expected TextContent response" -- | Helper to run a tool and get concise text response runToolConcise :: SessionManager.SessionManager ServerState -> Types.AgdaTool -> IO Text @@ -78,8 +78,8 @@ runToolConcise manager tool = do let toolWithConciseFormat = setFormat tool (Just "Concise") result <- handleAgdaToolWithSession manager toolWithConciseFormat case result of - MCP.ContentText txt -> pure txt - _ -> fail "Expected ContentText response" + TextContentType (TextContent _ txt _ _) -> pure txt + _ -> fail "Expected TextContent response" -- | Set format on a tool (preserves sessionId) setFormat :: Types.AgdaTool -> Maybe Text -> Types.AgdaTool @@ -973,8 +973,8 @@ goalAtPositionTests = testGroup "agda_goal_at_position" result <- handleAgdaToolWithSession manager tool case result of - MCP.ContentText txt -> assertBool "Should mention no goal found" (T.isInfixOf "No goal found" txt) - _ -> assertFailure "Expected ContentText response" + TextContentType (TextContent _ txt _ _) -> assertBool "Should mention no goal found" (T.isInfixOf "No goal found" txt) + _ -> assertFailure "Expected TextContent response" , withSessionManager $ \getManager ->simpleTestCase "formats concisely" $ do manager <- getManager From 0ab7a9e5e9f213502c9515b05170be06d88bfc03 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 16 Dec 2025 17:20:45 +0000 Subject: [PATCH 02/12] Add GitHub Actions CI workflow with Nix - Build project using nix build - Run tests via nix flake checks - Uses DeterminateSystems Nix installer and magic cache --- .github/workflows/ci.yml | 50 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) create mode 100644 .github/workflows/ci.yml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 0000000..6bcc45d --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,50 @@ +name: CI + +on: + push: + branches: [main, master] + pull_request: + branches: [main, master] + +jobs: + build-and-test: + runs-on: ubuntu-latest + + steps: + - name: Checkout repository + uses: actions/checkout@v4 + + - name: Install Nix + uses: DeterminateSystems/nix-installer-action@main + with: + extra-conf: | + experimental-features = nix-command flakes + + - name: Setup Nix cache + uses: DeterminateSystems/magic-nix-cache-action@main + + - name: Build project + run: nix build .#agda-mcp + + - name: Run tests + run: nix build .#checks.x86_64-linux.agda-mcp-tests --print-build-logs + + # Optional: Check that flake evaluates correctly + flake-check: + runs-on: ubuntu-latest + + steps: + - name: Checkout repository + uses: actions/checkout@v4 + + - name: Install Nix + uses: DeterminateSystems/nix-installer-action@main + with: + extra-conf: | + experimental-features = nix-command flakes + + - name: Setup Nix cache + uses: DeterminateSystems/magic-nix-cache-action@main + + - name: Check flake + run: nix flake check From 3e5e63e69eda8d56e56b0aa20848130c60a8913a Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 16 Dec 2025 17:24:32 +0000 Subject: [PATCH 03/12] Fix flake.nix: reference agda-mcp instead of example package --- flake.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/flake.nix b/flake.nix index 3dece4d..019e5c5 100644 --- a/flake.nix +++ b/flake.nix @@ -57,7 +57,7 @@ }; # haskell-flake doesn't set the default package, but you can do it here. - packages.default = self'.packages.example; + packages.default = self'.packages.agda-mcp; }; }; } From 7ceb25ccee483a2b1c8c99b92e8b364a8672a21b Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 16 Dec 2025 18:06:12 +0000 Subject: [PATCH 04/12] Add patch to relax mcp dependency version bounds The mcp library has strict version bounds that don't work with GHC 9.10. This patch relaxes the bounds for bytestring, containers, text, warp, time, and other dependencies to allow building with newer package versions. --- flake.nix | 6 +++- patches/mcp-relax-bounds.patch | 65 ++++++++++++++++++++++++++++++++++ 2 files changed, 70 insertions(+), 1 deletion(-) create mode 100644 patches/mcp-relax-bounds.patch diff --git a/flake.nix b/flake.nix index 019e5c5..e166ab6 100644 --- a/flake.nix +++ b/flake.nix @@ -26,7 +26,11 @@ # (defined by `defaults.packages` option). # packages = { - mcp.source = inputs.mcp; + mcp.source = pkgs.applyPatches { + name = "mcp-patched"; + src = inputs.mcp; + patches = [ ./patches/mcp-relax-bounds.patch ]; + }; # aeson.source = "1.5.0.0"; # Override aeson to a custom version from Hackage # shower.source = inputs.shower; # Override shower to a custom source path }; diff --git a/patches/mcp-relax-bounds.patch b/patches/mcp-relax-bounds.patch new file mode 100644 index 0000000..d7a3064 --- /dev/null +++ b/patches/mcp-relax-bounds.patch @@ -0,0 +1,65 @@ +diff --git a/mcp.cabal b/mcp.cabal +index 1234567..abcdefg 100644 +--- a/mcp.cabal ++++ b/mcp.cabal +@@ -101,30 +101,30 @@ library + + -- Other library packages from which modules are imported. + build-depends: +- base >= 4.18.2.1 && <= 4.21.0.0, +- aeson >= 2.1 && < 2.3, +- text >= 2.0 && <= 2.1.2, +- containers >= 0.6 && < 0.7, +- bytestring >= 0.11 && < 0.12, +- unordered-containers >= 0.2 && < 0.3, +- stm >= 2.5 && < 2.6, +- async >= 2.2 && < 2.3, +- mtl >= 2.3 && < 2.4, +- transformers >= 0.6 && < 0.7, +- warp >= 3.3 && < 3.4, +- wai >= 3.2 && < 3.3, +- wai-extra >= 3.1 && < 3.2, +- servant-server >= 0.19 && < 0.21, +- servant >= 0.19 && < 0.21, +- http-types >= 0.12 && < 0.13, +- servant-auth >= 0.4 && < 0.5, +- servant-auth-server >= 0.4 && < 0.5, +- jose >= 0.10 && < 0.12, +- cryptonite >= 0.30 && < 0.31, +- memory >= 0.18 && < 0.19, +- base64-bytestring >= 1.2 && < 1.3, +- http-conduit >= 2.3 && < 2.4, +- random >= 1.2 && < 1.3, +- time >= 1.12 && < 1.13, +- uuid >= 1.3 && < 1.4, +- data-default >= 0.7 && < 0.8 ++ base >= 4.18, ++ aeson >= 2.1, ++ text >= 2.0, ++ containers >= 0.6, ++ bytestring >= 0.11, ++ unordered-containers >= 0.2, ++ stm >= 2.5, ++ async >= 2.2, ++ mtl >= 2.3, ++ transformers >= 0.6, ++ warp >= 3.3, ++ wai >= 3.2, ++ wai-extra >= 3.1, ++ servant-server >= 0.19, ++ servant >= 0.19, ++ http-types >= 0.12, ++ servant-auth >= 0.4, ++ servant-auth-server >= 0.4, ++ jose >= 0.10, ++ cryptonite >= 0.30, ++ memory >= 0.18, ++ base64-bytestring >= 1.2, ++ http-conduit >= 2.3, ++ random >= 1.2, ++ time >= 1.12, ++ uuid >= 1.3, ++ data-default >= 0.7 + + -- Directories containing source files. + hs-source-dirs: src From 1169b89e75b2502e07ac734045f7ebfde05f0828 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 17 Dec 2025 09:31:48 +0000 Subject: [PATCH 05/12] Use jailbreak instead of patch for mcp dependency bounds Replace the manual cabal bounds patch with haskell-flake's built-in jailbreak option, which is cleaner and more maintainable. --- flake.nix | 7 ++-- patches/mcp-relax-bounds.patch | 65 ---------------------------------- 2 files changed, 2 insertions(+), 70 deletions(-) delete mode 100644 patches/mcp-relax-bounds.patch diff --git a/flake.nix b/flake.nix index e166ab6..cd163d5 100644 --- a/flake.nix +++ b/flake.nix @@ -26,15 +26,12 @@ # (defined by `defaults.packages` option). # packages = { - mcp.source = pkgs.applyPatches { - name = "mcp-patched"; - src = inputs.mcp; - patches = [ ./patches/mcp-relax-bounds.patch ]; - }; + mcp.source = inputs.mcp; # aeson.source = "1.5.0.0"; # Override aeson to a custom version from Hackage # shower.source = inputs.shower; # Override shower to a custom source path }; settings = { + mcp.jailbreak = true; # aeson = { # check = false; # }; diff --git a/patches/mcp-relax-bounds.patch b/patches/mcp-relax-bounds.patch deleted file mode 100644 index d7a3064..0000000 --- a/patches/mcp-relax-bounds.patch +++ /dev/null @@ -1,65 +0,0 @@ -diff --git a/mcp.cabal b/mcp.cabal -index 1234567..abcdefg 100644 ---- a/mcp.cabal -+++ b/mcp.cabal -@@ -101,30 +101,30 @@ library - - -- Other library packages from which modules are imported. - build-depends: -- base >= 4.18.2.1 && <= 4.21.0.0, -- aeson >= 2.1 && < 2.3, -- text >= 2.0 && <= 2.1.2, -- containers >= 0.6 && < 0.7, -- bytestring >= 0.11 && < 0.12, -- unordered-containers >= 0.2 && < 0.3, -- stm >= 2.5 && < 2.6, -- async >= 2.2 && < 2.3, -- mtl >= 2.3 && < 2.4, -- transformers >= 0.6 && < 0.7, -- warp >= 3.3 && < 3.4, -- wai >= 3.2 && < 3.3, -- wai-extra >= 3.1 && < 3.2, -- servant-server >= 0.19 && < 0.21, -- servant >= 0.19 && < 0.21, -- http-types >= 0.12 && < 0.13, -- servant-auth >= 0.4 && < 0.5, -- servant-auth-server >= 0.4 && < 0.5, -- jose >= 0.10 && < 0.12, -- cryptonite >= 0.30 && < 0.31, -- memory >= 0.18 && < 0.19, -- base64-bytestring >= 1.2 && < 1.3, -- http-conduit >= 2.3 && < 2.4, -- random >= 1.2 && < 1.3, -- time >= 1.12 && < 1.13, -- uuid >= 1.3 && < 1.4, -- data-default >= 0.7 && < 0.8 -+ base >= 4.18, -+ aeson >= 2.1, -+ text >= 2.0, -+ containers >= 0.6, -+ bytestring >= 0.11, -+ unordered-containers >= 0.2, -+ stm >= 2.5, -+ async >= 2.2, -+ mtl >= 2.3, -+ transformers >= 0.6, -+ warp >= 3.3, -+ wai >= 3.2, -+ wai-extra >= 3.1, -+ servant-server >= 0.19, -+ servant >= 0.19, -+ http-types >= 0.12, -+ servant-auth >= 0.4, -+ servant-auth-server >= 0.4, -+ jose >= 0.10, -+ cryptonite >= 0.30, -+ memory >= 0.18, -+ base64-bytestring >= 1.2, -+ http-conduit >= 2.3, -+ random >= 1.2, -+ time >= 1.12, -+ uuid >= 1.3, -+ data-default >= 0.7 - - -- Directories containing source files. - hs-source-dirs: src From 6f808d0e6e831c903e3263c4428c1645a85e8c8a Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 17 Dec 2025 09:42:52 +0000 Subject: [PATCH 06/12] Update flake.lock for Tritlo/mcp dependency Updates lock file to reflect the switch from drshade/haskell-mcp-server to Tritlo/mcp library. --- flake.lock | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/flake.lock b/flake.lock index 81ebfff..f25eef4 100644 --- a/flake.lock +++ b/flake.lock @@ -33,19 +33,19 @@ "type": "github" } }, - "mcp-server-hs": { + "mcp": { "flake": false, "locked": { - "lastModified": 1755071752, - "narHash": "sha256-DaSefoJKo6AJ9Gd8gwalVkkd5P7MVnstdeL6LV2izvY=", - "owner": "drshade", - "repo": "haskell-mcp-server", - "rev": "92c70a93446adca0c7cfced97a93eed23bfb5200", + "lastModified": 1753988023, + "narHash": "sha256-gTV52O4chiB8ehw/nNFvX5cYXACswrqE7aPA+5w/61g=", + "owner": "Tritlo", + "repo": "mcp", + "rev": "5ef0860698e0e2beecad7ea7d64bba53efca8034", "type": "github" }, "original": { - "owner": "drshade", - "repo": "haskell-mcp-server", + "owner": "Tritlo", + "repo": "mcp", "type": "github" } }, @@ -84,7 +84,7 @@ "inputs": { "flake-parts": "flake-parts", "haskell-flake": "haskell-flake", - "mcp-server-hs": "mcp-server-hs", + "mcp": "mcp", "nixpkgs": "nixpkgs" } } From 2f34a327502a68bbf860267e2a8e2baef8825ca9 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 17 Dec 2025 10:10:56 +0000 Subject: [PATCH 07/12] Fix MCP.Types import and pattern match warning - Server.hs: Import ContentBlock(..) instead of TextContentType(..) since TextContentType is a data constructor of ContentBlock - FileEdit.hs: Make splitAt pattern match total by using case expression instead of irrefutable pattern binding --- src/AgdaMCP/FileEdit.hs | 36 +++++++++++++++++++----------------- src/AgdaMCP/Server.hs | 2 +- 2 files changed, 20 insertions(+), 18 deletions(-) diff --git a/src/AgdaMCP/FileEdit.hs b/src/AgdaMCP/FileEdit.hs index 82accd1..f0eb8bd 100644 --- a/src/AgdaMCP/FileEdit.hs +++ b/src/AgdaMCP/FileEdit.hs @@ -139,23 +139,25 @@ applyReplaceLine file lineNum clauses _indentLevel _needsReload = do then putStrLn $ "Warning: Line number " ++ show lineNum ++ " out of bounds" else do -- Split at line position - let (beforeLines, originalLine:afterLines) = splitAt (lineNum - 1) lines' - - -- Calculate indentation from the original line (leading whitespace) - let originalIndent = T.takeWhile (== ' ') originalLine - let indentLevel = T.length originalIndent - - -- Apply the same indentation to each clause - -- Note: Agda provides clauses without leading whitespace - let indentedClauses = map (originalIndent <>) clauses - - -- Reconstruct file - let newContent = T.unlines $ beforeLines ++ indentedClauses ++ afterLines - TIO.writeFile file newContent - - putStrLn $ "Replaced line " ++ show lineNum ++ " with " ++ - show (length clauses) ++ " clauses (indent level: " ++ - show indentLevel ++ ")" + let (beforeLines, rest) = splitAt (lineNum - 1) lines' + case rest of + [] -> putStrLn $ "Warning: Line number " ++ show lineNum ++ " resulted in empty rest" + (originalLine:afterLines) -> do + -- Calculate indentation from the original line (leading whitespace) + let originalIndent = T.takeWhile (== ' ') originalLine + let indentLevel = T.length originalIndent + + -- Apply the same indentation to each clause + -- Note: Agda provides clauses without leading whitespace + let indentedClauses = map (originalIndent <>) clauses + + -- Reconstruct file + let newContent = T.unlines $ beforeLines ++ indentedClauses ++ afterLines + TIO.writeFile file newContent + + putStrLn $ "Replaced line " ++ show lineNum ++ " with " ++ + show (length clauses) ++ " clauses (indent level: " ++ + show indentLevel ++ ")" -- ============================================================================ -- Strategy 3: BatchEdits (reverse-order application) diff --git a/src/AgdaMCP/Server.hs b/src/AgdaMCP/Server.hs index 88f636d..8884a5a 100644 --- a/src/AgdaMCP/Server.hs +++ b/src/AgdaMCP/Server.hs @@ -42,7 +42,7 @@ import System.FilePath (takeDirectory) import System.Directory (listDirectory) -- MCP Server library -import MCP.Types (Content, TextContent(..), TextContentType(..), TextResourceContents(..), ResourceContents(..)) +import MCP.Types (Content, ContentBlock(..), TextContent(..), TextResourceContents(..), ResourceContents(..)) import qualified AgdaMCP.Types import qualified AgdaMCP.Repl as Repl import qualified AgdaMCP.SessionManager as SessionManager From 9c853033bc0639b9c6ca573cba020065ae0365a5 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 17 Dec 2025 10:16:05 +0000 Subject: [PATCH 08/12] Fix MCP.Types import in test files Import ContentBlock(..) instead of Content(..) since TextContentType is a data constructor of ContentBlock. --- test/AgdaMCP/EditPersistenceSpec.hs | 2 +- test/AgdaMCP/MultiAgentSpec.hs | 2 +- test/AgdaMCP/ServerSpec.hs | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/test/AgdaMCP/EditPersistenceSpec.hs b/test/AgdaMCP/EditPersistenceSpec.hs index ca8c3d8..ff212d9 100644 --- a/test/AgdaMCP/EditPersistenceSpec.hs +++ b/test/AgdaMCP/EditPersistenceSpec.hs @@ -21,7 +21,7 @@ import Control.Exception (try, SomeException, bracket, catch) import AgdaMCP.Server import qualified AgdaMCP.Types as Types import qualified AgdaMCP.SessionManager as SessionManager -import MCP.Types (Content(..), TextContent(..)) +import MCP.Types (Content, ContentBlock(..), TextContent(..)) import AgdaMCP.TestUtils (withTempTestFile) -- | Simple test case type diff --git a/test/AgdaMCP/MultiAgentSpec.hs b/test/AgdaMCP/MultiAgentSpec.hs index 6fbc3b4..2ee7936 100644 --- a/test/AgdaMCP/MultiAgentSpec.hs +++ b/test/AgdaMCP/MultiAgentSpec.hs @@ -25,7 +25,7 @@ import System.IO.Unsafe (unsafePerformIO) import AgdaMCP.Server import qualified AgdaMCP.Types as Types import qualified AgdaMCP.SessionManager as SessionManager -import MCP.Types (Content(..), TextContent(..)) +import MCP.Types (Content, ContentBlock(..), TextContent(..)) import AgdaMCP.TestUtils (withTempTestFile) -- | Simple test case type diff --git a/test/AgdaMCP/ServerSpec.hs b/test/AgdaMCP/ServerSpec.hs index 0a1fe8a..3bda55c 100644 --- a/test/AgdaMCP/ServerSpec.hs +++ b/test/AgdaMCP/ServerSpec.hs @@ -24,7 +24,7 @@ import System.Timeout (timeout) import AgdaMCP.Server import qualified AgdaMCP.Types as Types import qualified AgdaMCP.SessionManager as SessionManager -import MCP.Types (Content(..), TextContent(..)) +import MCP.Types (Content, ContentBlock(..), TextContent(..)) import qualified AgdaMCP.MultiAgentSpec as MultiAgent import AgdaMCP.TestUtils (withTempTestFile) From 9e87de62f0ea5c90c17cb465be23e0312a6aa70c Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 17 Dec 2025 10:20:55 +0000 Subject: [PATCH 09/12] Fix ServerState name collision and id ambiguity in Main.hs - Hide MCP.Server.ServerState to avoid collision with AgdaMCP.Server.ServerState - Use fromMaybe instead of maybe+id to avoid potential id ambiguity --- Main.hs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Main.hs b/Main.hs index c636722..d28b740 100644 --- a/Main.hs +++ b/Main.hs @@ -11,12 +11,13 @@ import Data.Aeson (Value, toJSON) import qualified Data.Aeson as JSON import Data.IORef import qualified Data.Map.Strict as Map +import Data.Maybe (fromMaybe) import Data.Text (Text) import System.IO (hSetEncoding, stderr, stdout, utf8, hPutStrLn) import System.IO.Unsafe (unsafePerformIO) import MCP.Protocol -import MCP.Server +import MCP.Server hiding (ServerState) import MCP.Server.HTTP import MCP.Types @@ -54,7 +55,7 @@ instance MCPServer MCPServerM where result <- liftIO $ do -- Get session manager from global state manager <- getGlobalSessionManager - let args = maybe Map.empty id mArgs + let args = fromMaybe Map.empty mArgs callAgdaTool manager toolName args return result From c0ec80cf6f2edd581a9a911ef0029f4fc9718e2d Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 17 Dec 2025 10:24:06 +0000 Subject: [PATCH 10/12] Hide error field from MCP.Protocol to avoid Prelude collision --- Main.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Main.hs b/Main.hs index d28b740..143632f 100644 --- a/Main.hs +++ b/Main.hs @@ -16,7 +16,7 @@ import Data.Text (Text) import System.IO (hSetEncoding, stderr, stdout, utf8, hPutStrLn) import System.IO.Unsafe (unsafePerformIO) -import MCP.Protocol +import MCP.Protocol hiding (error) import MCP.Server hiding (ServerState) import MCP.Server.HTTP import MCP.Types From c216d1d44887b98df52806b2e8bcd6ca4597f16e Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 17 Dec 2025 10:27:40 +0000 Subject: [PATCH 11/12] Add TypeSynonymInstances and FlexibleInstances for MCPServerM --- Main.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Main.hs b/Main.hs index 143632f..b1c30aa 100644 --- a/Main.hs +++ b/Main.hs @@ -1,6 +1,8 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE FlexibleInstances #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} {-# OPTIONS_GHC -Wno-orphans #-} From c3d3e6f10300f16954c817ddb8b25d6306b97c11 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 17 Dec 2025 10:32:37 +0000 Subject: [PATCH 12/12] Use Paths_agda_mcp for test fixture locations - Add data-dir and data-files to cabal for test fixtures - Update TestUtils and EditPersistenceSpec to use getDataDir - This ensures test files are found in Nix builds --- agda-mcp.cabal | 10 ++++++++++ test/AgdaMCP/EditPersistenceSpec.hs | 7 ++++--- test/AgdaMCP/TestUtils.hs | 7 ++++--- 3 files changed, 18 insertions(+), 6 deletions(-) diff --git a/agda-mcp.cabal b/agda-mcp.cabal index 5850072..816b6c4 100644 --- a/agda-mcp.cabal +++ b/agda-mcp.cabal @@ -9,6 +9,13 @@ author: Claude Code maintainer: claude-code@anthropic.com category: Development build-type: Simple +extra-source-files: + test/*.agda + test/edit-persistence/*.agda +data-dir: test +data-files: + *.agda + edit-persistence/*.agda library exposed-modules: @@ -69,6 +76,9 @@ test-suite agda-mcp-tests AgdaMCP.MultiAgentSpec AgdaMCP.EditPersistenceSpec AgdaMCP.TestUtils + Paths_agda_mcp + autogen-modules: + Paths_agda_mcp build-depends: base >= 4.14 && < 5, agda-mcp, diff --git a/test/AgdaMCP/EditPersistenceSpec.hs b/test/AgdaMCP/EditPersistenceSpec.hs index ff212d9..1d73c1e 100644 --- a/test/AgdaMCP/EditPersistenceSpec.hs +++ b/test/AgdaMCP/EditPersistenceSpec.hs @@ -14,9 +14,10 @@ import qualified Data.Text.Encoding as TE import qualified Data.ByteString.Lazy as LBS import Data.Text (Text) import System.FilePath ((), takeDirectory, takeFileName) -import System.Directory (getCurrentDirectory, copyFile, createDirectoryIfMissing, removeFile, removeDirectoryRecursive, getTemporaryDirectory) +import System.Directory (copyFile, createDirectoryIfMissing, removeFile, removeDirectoryRecursive, getTemporaryDirectory) import System.Random (randomIO) import Control.Exception (try, SomeException, bracket, catch) +import Paths_agda_mcp (getDataDir) import AgdaMCP.Server import qualified AgdaMCP.Types as Types @@ -70,10 +71,10 @@ assertNotContains needle haystack = -- | Custom version for edit-persistence subdirectory copyEditTestFile :: FilePath -> IO FilePath copyEditTestFile filename = do - cwd <- getCurrentDirectory + dataDir <- getDataDir tmpDir <- getTemporaryDirectory randomHash <- randomIO :: IO Int - let sourceFile = cwd "test" "edit-persistence" filename + let sourceFile = dataDir "edit-persistence" filename let tempDir = tmpDir ("agda-mcp-persist-test-" ++ show (abs randomHash)) let tempFile = tempDir filename createDirectoryIfMissing True tempDir diff --git a/test/AgdaMCP/TestUtils.hs b/test/AgdaMCP/TestUtils.hs index 60a4e76..81be961 100644 --- a/test/AgdaMCP/TestUtils.hs +++ b/test/AgdaMCP/TestUtils.hs @@ -8,9 +8,10 @@ module AgdaMCP.TestUtils ) where import System.FilePath ((), takeDirectory) -import System.Directory (getCurrentDirectory, copyFile, createDirectoryIfMissing, removeDirectoryRecursive, getTemporaryDirectory) +import System.Directory (copyFile, createDirectoryIfMissing, removeDirectoryRecursive, getTemporaryDirectory) import System.Random (randomIO) import Control.Exception (SomeException, bracket, catch) +import Paths_agda_mcp (getDataDir) -- ============================================================================ -- Temp File Utilities (for tests that modify files) @@ -20,10 +21,10 @@ import Control.Exception (SomeException, bracket, catch) -- Uses random temp directory to preserve module name and avoid conflicts copyTestFile :: FilePath -> IO FilePath copyTestFile filename = do - cwd <- getCurrentDirectory + dataDir <- getDataDir tmpDir <- getTemporaryDirectory randomHash <- randomIO :: IO Int - let sourceFile = cwd "test" filename + let sourceFile = dataDir filename let tempDir = tmpDir ("agda-mcp-test-" ++ show (abs randomHash)) let tempFile = tempDir filename createDirectoryIfMissing True tempDir