Arch Linux User Repository

hi! sorry, I forgot to turn on notifications and didn't see the last comment. since upstream is lagging so much, I think I would appreciate being a co-maintainer :)

in the meantime, temporary lsp-1.5.patch to add (in addition to the one I last sent) for changes to lsp 1.5 / 1.6:

diff --git a/agda-language-server.cabal b/agda-language-server.cabal
index c0c682b..25ad27c 100644
--- a/agda-language-server.cabal
+++ b/agda-language-server.cabal
@@ -67,11 +67,13 @@ library
     , aeson
     , base >=4.7 && <5
     , bytestring
+    , co-log-core
     , containers
     , lsp <2
     , mtl
     , network
     , network-simple
+    , prettyprinter
     , process
     , stm
     , strict
@@ -145,12 +147,14 @@ test-suite als-test
     , aeson
     , base >=4.7 && <5
     , bytestring
+    , co-log-core
     , containers
     , lsp <2
     , mtl
     , network
     , network-simple
     , process
+    , prettyprinter
     , stm
     , strict
     , tasty
diff --git a/src/Agda/Position.hs b/src/Agda/Position.hs
index 2f21210..5771313 100644
--- a/src/Agda/Position.hs
+++ b/src/Agda/Position.hs
@@ -42,7 +42,7 @@ toAgdaRange table path (LSP.Range start end) = Range
 toAgdaPositionWithoutFile :: ToOffset -> LSP.Position -> PositionWithoutFile
 toAgdaPositionWithoutFile table (LSP.Position line col) = Pn
   ()
-  (fromIntegral (toOffset table (line, col)) + 1)
+  (fromIntegral (toOffset table (fromIntegral line, fromIntegral col)) + 1)
   (fromIntegral line + 1)
   (fromIntegral col + 1)

diff --git a/src/Server.hs b/src/Server.hs
index f26d0bb..5b1ff45 100644
--- a/src/Server.hs
+++ b/src/Server.hs
@@ -6,6 +6,9 @@ module Server
   ( run
   ) where

+import qualified Colog.Core as L
+import           Colog.Core (LogAction (..), WithSeverity (..), Severity (..), (<&))
+
 import qualified Agda
 import           Control.Concurrent             ( writeChan )
 import           Control.Monad.Reader           ( MonadIO(liftIO)
@@ -24,12 +27,15 @@ import           Language.LSP.Types      hiding ( Options(..)
 import           Monad
 import qualified Network.Simple.TCP            as TCP
 import           Network.Socket                 ( socketToHandle )
+import           Prettyprinter                  ( pretty
+                                                , viaShow )
 import qualified Switchboard
 import           Switchboard                    ( Switchboard )

 import qualified Server.Handler                as Handler

 import qualified Language.LSP.Server           as LSP
+import           Language.LSP.Logging           ( defaultClientLogger )
 import           Options


@@ -44,7 +50,7 @@ run options = do
         $ \(sock, _remoteAddr) -> do
             -- writeChan (envLogChan env) "[Server] connection established"
             handle <- socketToHandle sock ReadWriteMode
-            _      <- runServerWithHandles handle handle (serverDefn options)
+            _      <- runServerWithHandles ioLogger lspLogger handle handle (serverDefn options)
             return ()
       -- Switchboard.destroy switchboard
       return 0
@@ -87,6 +93,15 @@ run options = do
   saveOptions :: SaveOptions
   saveOptions = SaveOptions (Just True)

+  -- loggers copied from runServer for now
+  prettyMsg l = "[" <> viaShow (L.getSeverity l) <> "] " <> pretty (L.getMsg l)
+  ioLogger :: LogAction IO (WithSeverity LspServerLog)
+  ioLogger = L.cmap (show . prettyMsg) L.logStringStderr
+  lspLogger :: LogAction (LspM Config) (WithSeverity LspServerLog)
+  lspLogger =
+    let clientLogger = L.cmap (fmap (pack . show . pretty)) defaultClientLogger
+    in clientLogger <> L.hoistLogAction liftIO ioLogger
+
 -- handlers of the LSP server
 handlers :: Handlers (ServerM (LspM Config))
 handlers = mconcat

Thanks a lot, mild_sunrise! I can add you as a co-maintainer of this package, so you don't have to wait for me to apply fixes. Please tell me if that is something you would want :)

temporary patch until upstream updates to Agda 2.6.2.2:

diff --git a/PKGBUILD b/PKGBUILD
index 64b0843..0b20873 100644
--- a/PKGBUILD
+++ b/PKGBUILD
@@ -1,7 +1,7 @@
 # Maintainer: Philipp Joram <mail [at] phijor [dot] me>

 _hkgname=agda-language-server
-_agdaver=2.6.2.1
+_agdaver=2.6.2.2
 pkgname=haskell-agda-language-server
 pkgver=0.2.1
 pkgrel=21
@@ -15,8 +15,15 @@ depends=('ghc-libs' "agda=$_agdaver" 'haskell-aeson' 'haskell-lsp' 'haskell-netw
 # Remove git dependency and revert to downloading from hackage once upstream
 # provides a release compatible with Agda v2.6.2.1.
 makedepends=('git' 'ghc' 'haskell-tasty' 'haskell-tasty-golden' 'haskell-tasty-hunit' 'haskell-tasty-quickcheck')
-source=("$_hkgname-$pkgver::git+https://github.com/banacorn/agda-language-server.git#branch=2.6.2.1")
-sha256sums=('SKIP')
+source=("$_hkgname-$pkgver::git+https://github.com/banacorn/agda-language-server.git"
+        "agda-2.6.2.2.patch")
+sha256sums=('SKIP'
+            '293de4aaff865f1f9babf0b6107fc8b0e0bdaf538597981afaa9cfcf402e8b79')
+
+prepare() {
+  cd $_hkgname-$pkgver
+  patch --strip=1 --input="${srcdir}/agda-2.6.2.2.patch"
+}

 build() {
   cd $_hkgname-$pkgver
diff --git a/agda-2.6.2.2.patch b/agda-2.6.2.2.patch
new file mode 100644
index 0000000..c397cdc
--- /dev/null
+++ b/agda-2.6.2.2.patch
@@ -0,0 +1,65 @@
+diff --git a/agda-language-server.cabal b/agda-language-server.cabal
+index c0c682b..7b6cb0d 100644
+--- a/agda-language-server.cabal
++++ b/agda-language-server.cabal
+@@ -63,7 +63,7 @@ library
+       OverloadedStrings
+   ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -Werror=incomplete-patterns -fno-warn-orphans
+   build-depends:
+-      Agda ==2.6.2.1
++      Agda ==2.6.2.2
+     , aeson
+     , base >=4.7 && <5
+     , bytestring
+@@ -86,7 +86,7 @@ executable als
+       app
+   ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -threaded -rtsopts -with-rtsopts=-N -Werror=incomplete-patterns -fno-warn-orphans
+   build-depends:
+-      Agda ==2.6.2.1
++      Agda ==2.6.2.2
+     , aeson
+     , agda-language-server
+     , base >=4.7 && <5
+@@ -141,7 +141,7 @@ test-suite als-test
+       OverloadedStrings
+   ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -threaded -rtsopts -with-rtsopts=-N -Werror=incomplete-patterns -fno-warn-orphans
+   build-depends:
+-      Agda ==2.6.2.1
++      Agda ==2.6.2.2
+     , aeson
+     , base >=4.7 && <5
+     , bytestring
+diff --git a/package.yaml b/package.yaml
+index 6f35310..2a31014 100644
+--- a/package.yaml
++++ b/package.yaml
+@@ -23,7 +23,7 @@ description:         Please see the README on GitHub at <https://github.com/bana
+ 
+ dependencies:
+   - base >= 4.7 && < 5
+-  - Agda == 2.6.2.1
++  - Agda == 2.6.2.2
+   - aeson
+   - bytestring
+   - containers
+diff --git a/src/Agda/Convert.hs b/src/Agda/Convert.hs
+index 51c0adb..eb552ef 100644
+--- a/src/Agda/Convert.hs
++++ b/src/Agda/Convert.hs
+@@ -21,6 +21,7 @@ import Agda.Syntax.Position (HasRange (getRange), Range, noRange)
+ import Agda.Syntax.Scope.Base
+ import Agda.TypeChecking.Errors (getAllWarningsOfTCErr, prettyError)
+ import Agda.TypeChecking.Monad hiding (Function)
++import Agda.TypeChecking.Monad.MetaVars (withInteractionId)
+ import Agda.TypeChecking.Pretty (prettyTCM)
+ import qualified Agda.TypeChecking.Pretty as TCP
+ import Agda.TypeChecking.Pretty.Warning (filterTCWarnings, prettyTCWarnings, prettyTCWarnings')
+@@ -278,7 +279,7 @@ fromDisplayInfo = \case
+ 
+ lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM IR.DisplayInfo
+ lispifyGoalSpecificDisplayInfo ii kind = localTCState $
+-  B.withInteractionId ii $
++  withInteractionId ii $
+     case kind of
+       Goal_HelperFunction helperType -> do
+         doc <- inTopContext $ prettyATop helperType

(I've submitted a PR with this patch but it's still incomplete for upstream to accept)

Thank you for the fix, @mild_sunrise! I updated the package, let's wait for a new upstream release.

quick fix to get it working until upstream releases updated version for Agda 2.6.2.1:

diff --git a/PKGBUILD b/PKGBUILD
index 7ffeb56..16dfd4d 100644
--- a/PKGBUILD
+++ b/PKGBUILD
@@ -1,7 +1,7 @@
 # Maintainer: Philipp Joram <mail [at] phijor [dot] me>

 _hkgname=agda-language-server
-_agdaver=2.6.2
+_agdaver=2.6.2.1
 pkgname=haskell-agda-language-server
 pkgver=0.2.1
 pkgrel=20
@@ -11,8 +11,8 @@ license=("custom: MIT")
 arch=('x86_64')
 depends=('ghc-libs' "agda=$_agdaver" 'haskell-aeson' 'haskell-lsp' 'haskell-network' 'haskell-network-simple' 'haskell-strict')
 makedepends=('ghc' 'haskell-tasty' 'haskell-tasty-golden' 'haskell-tasty-hunit' 'haskell-tasty-quickcheck')
-source=("https://hackage.haskell.org/packages/archive/$_hkgname/$pkgver/$_hkgname-$pkgver.tar.gz")
-sha256sums=('20ec24dfd7d7f6f74942615bd5edbbc6641648dc5a41820bc9fdef24cb87fda7')
+source=("$_hkgname-$pkgver::git+https://github.com/banacorn/agda-language-server.git#branch=2.6.2.1")
+sha256sums=('SKIP')

 build() {
   cd $_hkgname-$pkgver