WIP: migrate to lsp-2 (does not build yet)

Author: andreasabel

agda-language-server.cabal

@@ -83,8 +83,8 @@ library
     , base >=4.7 && <5
     , bytestring
     , containers
-    , lsp <2
-    , lsp-types <2
+    , lsp
+    , lsp-types
     , mtl
     , network
     , network-simple
@@ -125,8 +125,8 @@ executable als
     , base >=4.7 && <5
     , bytestring
     , containers
-    , lsp <2
-    , lsp-types <2
+    , lsp
+    , lsp-types
     , mtl
     , network
     , network-simple
@@ -194,8 +194,8 @@ test-suite als-test
     , base >=4.7 && <5
     , bytestring
     , containers
-    , lsp <2
-    , lsp-types <2
+    , lsp
+    , lsp-types
     , mtl
     , network
     , network-simple

package.yaml

@@ -55,8 +55,8 @@ dependencies:
   - aeson
   - bytestring
   - containers
-  - lsp-types < 2
-  - lsp < 2
+  - lsp-types
+  - lsp
   - mtl
   - network
   - network-simple

src/Agda/Parser.hs

@@ -18,7 +18,11 @@ import Data.Maybe (fromMaybe)
 import Data.Text (Text, unpack)
 import qualified Data.Text as Text
 import Language.LSP.Server (LspM)
-import qualified Language.LSP.Types as LSP
+#if MIN_VERSION_lsp(2,0,0)
+import qualified Language.LSP.Protocol.Types   as LSP
+#else
+import qualified Language.LSP.Types            as LSP
+#endif
 import Options (Config)
 
 --------------------------------------------------------------------------------

src/Agda/Position.hs

@@ -22,7 +22,11 @@ import qualified Data.Sequence                 as Seq
 import qualified Data.Strict.Maybe             as Strict
 import           Data.Text                      ( Text )
 import qualified Data.Text                     as Text
+#if MIN_VERSION_lsp(2,0,0)
+import qualified Language.LSP.Protocol.Types   as LSP
+#else
 import qualified Language.LSP.Types            as LSP
+#endif
 
 -- Note:  LSP srclocs are 0-base
 --        Agda srclocs are 1-base

src/Monad.hs

@@ -1,4 +1,6 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleContexts #-}
+
 module Monad where
 
 import           Agda.IR
@@ -25,7 +27,11 @@ import           Data.Maybe                     ( isJust )
 import           Language.LSP.Server            ( MonadLsp
                                                 , getConfig
                                                 )
+#if MIN_VERSION_lsp(2,0,0)
+import qualified Language.LSP.Protocol.Types   as LSP
+#else
 import qualified Language.LSP.Types            as LSP
+#endif
 import           Options
 
 --------------------------------------------------------------------------------

src/Server/Handler.hs

@@ -55,7 +55,11 @@ import           Data.Text                      ( Text
 import qualified Data.Text                     as Text
 import           Language.LSP.Server            ( LspM )
 import qualified Language.LSP.Server           as LSP
+#if MIN_VERSION_lsp(2,0,0)
+import qualified Language.LSP.Protocol.Types   as LSP
+#else
 import qualified Language.LSP.Types            as LSP
+#endif
 import qualified Language.LSP.VFS              as VFS
 import           Monad
 import           Options                        ( Config
@@ -140,7 +144,13 @@ onHover uri pos = do
 
 fromHighlightingInfo :: IR.HighlightingInfo -> LSP.SemanticTokenAbsolute
 fromHighlightingInfo (IR.HighlightingInfo start end aspects isTokenBased note defSrc)
-  = LSP.SemanticTokenAbsolute 1 1 3 LSP.SttKeyword []
+  = LSP.SemanticTokenAbsolute 1 1 3 kw []
+  where
+#if MIN_VERSION_lsp_types(2,0,0)
+    kw = LSP.SemanticTokenTypes_Keyword
+#else
+    kw = LSP.SttKeyword
+#endif
 
 -- HighlightingInfo
 --       Int -- starting offset

src/Switchboard.hs

@@ -1,3 +1,11 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE PolyKinds #-}
+
+#if MIN_VERSION_lsp_types(2,0,0)
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeApplications #-}
+#endif
+
 module Switchboard (Switchboard, new, setupLanguageContextEnv, destroy) where
 
 import Monad
@@ -9,7 +17,14 @@ import qualified Agda
 import qualified Data.Aeson as JSON
 import qualified Data.Text.IO as Text
 import Language.LSP.Server
-import Language.LSP.Types hiding (TextDocumentSyncClientCapabilities (..))
+#if MIN_VERSION_lsp(2,0,0)
+import Data.Proxy (Proxy(Proxy))
+import Language.LSP.Protocol.Message
+import Language.LSP.Protocol.Types
+#else
+import Language.LSP.Types
+#endif
+  hiding (TextDocumentSyncClientCapabilities (..))
 import Data.IORef
 import Options (Config)
 
@@ -62,6 +77,13 @@ keepSendindResponse env ctxEnvIORef = forever $ do
       callback <- liftIO $ ResponseController.dispatch (envResponseController env)
 
       let value = JSON.toJSON response
-      sendRequest (SCustomMethod "agda") value $ \_result -> liftIO $ do
+      sendRequest agdaCustomMethod value $ \_result -> liftIO $ do
         -- writeChan (envLogChan env) $ "[Response] >>>> " <> pack (show value)
         callback ()
+
+agdaCustomMethod =
+#if MIN_VERSION_lsp_types(2,0,0)
+  SMethod_CustomMethod (Proxy @"agda")
+#else
+  SCustomMethod "agda"
+#endif

stack-9.2-Agda-2.6.4.yaml

@@ -0,0 +1,15 @@
+resolver: lts-20.26
+compiler: ghc-9.2.8
+# Allow a newer minor version of GHC than the snapshot specifies
+compiler-check: newer-minor
+
+packages:
+- .
+
+extra-deps:
+- Agda-2.6.4
+
+flags:
+  Agda:
+    # optimise-heavily: true
+    enable-cluster-counting: true

stack.yaml

@@ -1,14 +1,11 @@
-resolver: lts-20.26
-compiler: ghc-9.2.8
+resolver: lts-21.22
+compiler: ghc-9.4.8
 # Allow a newer minor version of GHC than the snapshot specifies
 compiler-check: newer-minor
 
 packages:
 - .
 
-extra-deps:
-- Agda-2.6.4
-
 flags:
   Agda:
     # optimise-heavily: true

stack.yaml.lock

@@ -3,17 +3,10 @@
 # For more information, please see the documentation at:
 #   https://docs.haskellstack.org/en/stable/lock_files
 
-packages:
-- completed:
-    hackage: Agda-2.6.4@sha256:298bc3b261ad034bf4ee788834a4d296aa5c2f6ea17ac4bef44e3daea53a7cd8,28443
-    pantry-tree:
-      sha256: 6c811b2ff8aa666ba301666e87d9234993d841dd370d47f8398379cd943e47bb
-      size: 42645
-  original:
-    hackage: Agda-2.6.4
+packages: []
 snapshots:
 - completed:
-    sha256: 5a59b2a405b3aba3c00188453be172b85893cab8ebc352b1ef58b0eae5d248a2
-    size: 650475
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/20/26.yaml
-  original: lts-20.26
+    sha256: afd5ba64ab602cabc2d3942d3d7e7dd6311bc626dcb415b901eaf576cb62f0ea
+    size: 640060
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/21/22.yaml
+  original: lts-21.22