Package Details: haskell-agda-language-server 0.2.1-22

Git Clone URL: https://aur.archlinux.org/haskell-agda-language-server.git (read-only, click to copy)
Package Base: haskell-agda-language-server
Description: An implementation of language server protocal (LSP) for Agda 2.
Upstream URL: https://github.com/banacorn/agda-language-server#readme
Licenses: custom: MIT
Submitter: phijor
Maintainer: None
Last Packager: phijor
Votes: 1
Popularity: 0.000000
First Submitted: 2022-03-24 17:29 (UTC)
Last Updated: 2022-08-21 15:11 (UTC)

Latest Comments

grdgkjrpdihe commented on 2026-02-17 18:55 (UTC)

PKGBUILD

# Maintainer: Philipp Joram <mail [at] phijor [dot] me>
# Contributor: mild_sunrise

_hkgname=agda-language-server
_agdaver=2.6.4.3
pkgname=haskell-agda-language-server
pkgver=dev.r6.g57d45f7
pkgrel=1
pkgdesc="An implementation of language server protocal (LSP) for Agda 2."
url="https://github.com/agda/agda-language-server#readme"
license=("custom: MIT")
arch=('x86_64')
depends=('ghc-libs' "agda=$_agdaver" 'haskell-aeson' 'haskell-lsp' 'haskell-network' 'haskell-network-simple' 'haskell-strict')

# FIXME:
# 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' 'haskell-lsp-test')
source=("$_hkgname::git+https://github.com/agda/agda-language-server.git"
        "agda-2.6.2.2.patch")
sha256sums=('SKIP'
            'f67dbad58df6f9737da863a82ef7bfd02c0853b63812a1ce2833f4c0ecd4ddfe')

pkgver() {
  cd $_hkgname
  git describe --long --tags --abbrev=7 | sed 's/\([^-]*-g\)/r\1/;s/-/./g'
}

prepare() {
  cd $_hkgname
  patch --strip=1 --input="${srcdir}/agda-2.6.2.2.patch"
}

build() {
  cd $_hkgname

  runhaskell Setup configure -O --enable-shared --enable-executable-dynamic --disable-library-vanilla \
    --prefix=/usr --docdir=/usr/share/doc/$pkgname --enable-tests \
    --dynlibdir=/usr/lib --libsubdir=\$compiler/site-local/\$pkgid \
    --ghc-option=-optl-Wl\,-z\,relro\,-z\,now \
    --ghc-option='-pie'

  runhaskell Setup build
  runhaskell Setup register --gen-script
  runhaskell Setup unregister --gen-script
  sed -i -r -e "s|ghc-pkg.*update[^ ]* |&'--force' |" register.sh
  sed -i -r -e "s|ghc-pkg.*unregister[^ ]* |&'--force' |" unregister.sh
}

check() {
  cd $_hkgname
  runhaskell Setup test
}

package() {
  cd $_hkgname

  install -D -m744 register.sh "$pkgdir"/usr/share/haskell/register/$pkgname.sh
  install -D -m744 unregister.sh "$pkgdir"/usr/share/haskell/unregister/$pkgname.sh
  runhaskell Setup copy --destdir="$pkgdir"
  install -D -m644 LICENSE -t "$pkgdir"/usr/share/licenses/$pkgname/
  rm -f "$pkgdir"/usr/share/doc/$pkgname/LICENSE
}

agda-2.6.2.2.patch

diff --git a/agda-language-server.cabal b/agda-language-server.cabal
index 378b857..94c6e0e 100644
--- a/agda-language-server.cabal
+++ b/agda-language-server.cabal
@@ -94,7 +94,7 @@ library
     , lsp-types >=2
     , mtl
     , network
-    , network-simple ==0.4.2
+    , network-simple ==0.4.5
     , prettyprinter
     , process
     , stm
@@ -141,7 +141,7 @@ executable als
     , lsp-types >=2
     , mtl
     , network
-    , network-simple ==0.4.2
+    , network-simple ==0.4.5
     , prettyprinter
     , process
     , stm
@@ -219,7 +219,7 @@ test-suite als-test
     , lsp-types >=2
     , mtl
     , network
-    , network-simple ==0.4.2
+    , network-simple ==0.4.5
     , prettyprinter
     , process
     , stm
diff --git a/package.yaml b/package.yaml
index b0fe8d9..f28dfca 100644
--- a/package.yaml
+++ b/package.yaml
@@ -64,7 +64,7 @@ dependencies:
   - lsp >= 2
   - mtl
   - network
-  - network-simple == 0.4.2
+  - network-simple == 0.4.5
   - strict
   - stm
   - text
diff --git a/test/Test/LSP.hs b/test/Test/LSP.hs
index ee7a688..1363e2d 100644
--- a/test/Test/LSP.hs
+++ b/test/Test/LSP.hs
@@ -22,7 +22,7 @@ tests alsPath =
 demo :: FilePath -> IO ()
 demo alsPath = do
   putStrLn $ "Running LSP tests on the server with the following path to the als executable: " ++ alsPath
-  runSession alsPath fullLatestClientCaps "test/data/" $ do
+  runSession alsPath fullCaps "test/data/" $ do
     doc <- openDoc "A.agda" "agda"

     -- hover

check wont pass. but lsp able to be used (didnt occurred any error so far)

AZMCode commented on 2024-07-22 21:04 (UTC)

Hello! Is there any possibility of this package being updated? It seems like the repository upstream has moved from banacorn/agda-language-server into agda/agda-language-server, and now the repository is offering v0.2.6.4.0.3.

Have you all tried repackaging the ubuntu binaries they now offer, instead of building from source?

mild_sunrise commented on 2023-02-15 21:05 (UTC) (edited on 2023-02-15 21:06 (UTC) by mild_sunrise)

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

phijor commented on 2022-08-21 15:13 (UTC)

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 :)

mild_sunrise commented on 2022-08-15 15:24 (UTC)

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)

phijor commented on 2022-07-15 17:51 (UTC)

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

mild_sunrise commented on 2022-07-15 10:16 (UTC)

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