Replace mcp-server dependency with mcp package

.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

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:
@@ -30,7 +37,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 +57,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
@@ -64,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,
@@ -75,7 +90,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

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,15 +26,12 @@
           # (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
           };
           settings = {
+            mcp.jailbreak = true;
             #  aeson = {
             #    check = false;
             #  };
@@ -61,7 +58,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;
       };
     };
 }

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)

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, ContentBlock(..), TextContent(..), TextResourceContents(..), ResourceContents(..))
 import qualified AgdaMCP.Types
 import qualified AgdaMCP.Repl as Repl
 import qualified AgdaMCP.SessionManager as SessionManager
@@ -884,44 +884,48 @@ 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
     AgdaMCP.Types.AgdaListPostulates{file} -> 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

test/AgdaMCP/EditPersistenceSpec.hs

@@ -14,14 +14,15 @@ 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
 import qualified AgdaMCP.SessionManager as SessionManager
-import qualified MCP.Server as MCP
+import MCP.Types (Content, ContentBlock(..), TextContent(..))
 import AgdaMCP.TestUtils (withTempTestFile)
 
 -- | Simple test case type
@@ -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
@@ -103,7 +104,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