agda-language-server 7 → 8

raw patch · 7 files changed

+112/−8 lines, 7 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

CHANGELOG.md +16/−0
agda-language-server.cabal +6/−4
package.yaml +2/−2
src/Options.hs +5/−1
test/Test.hs +5/−1
test/Test/Smoke.hs +59/−0
test/Test/Version.hs +19/−0

CHANGELOG.md view

@@ -4,6 +4,22 @@  The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). +## v8 - 2026-09-22++### Added+- Automated release pipeline: `publish-release` now publishes each version to GitHub and Hackage automatically on every `master` push, replacing the previous manual tag push and manual Hackage `workflow_dispatch`.+- #6: Bundle ICU libraries into the Linux release artifact, and run Smoke tests (`als --version`, non-ASCII LSP load) against the packaged release artifact on every platform.++### Changed+- Consolidate `create-release`, `upload-stable-release`, and `upload-dev-release` into a single `publish-dev` job.+- `agda-language-server.cabal` is no longer committed; it is generated from `package.yaml` by `hpack` on every build.+- Derive the reported language server version from `package.yaml` instead of a separately hardcoded constant, and add a test guarding against future drift.+- Increase release-artifact retention from 1 day to 7.+- Various CI caching correctness fixes across the native and WASM toolchains.++### Fixed+- #56: Fix `als --version` reporting the wrong language server version by [@chenrui333](https://github.com/chenrui333).+ ## v7 - 2026-09-16  ### Added

agda-language-server.cabal view

@@ -5,12 +5,12 @@ -- see: https://github.com/sol/hpack  name:           agda-language-server-version:        7+version:        8 synopsis:       An implementation of language server protocal (LSP) for Agda 2. description:    Please see the README on GitHub at <https://github.com/agda/agda-language-server#readme> category:       Development-homepage:       https://github.com/banacorn/agda-language-server#readme-bug-reports:    https://github.com/banacorn/agda-language-server/issues+homepage:       https://github.com/agda/agda-language-server#readme+bug-reports:    https://github.com/agda/agda-language-server/issues author:         Ting-Gian LUA maintainer:     banacorn@gmail.com, Andreas Abel copyright:      2020-23 Ting-Gian LUA, Andreas ABEL@@ -28,7 +28,7 @@  source-repository head   type: git-  location: https://github.com/banacorn/agda-language-server+  location: https://github.com/agda/agda-language-server  flag Agda-2-6-4   description: Embed Agda-2.6.4.3@@ -186,7 +186,9 @@   main-is: Test.hs   other-modules:       Test.LSP+      Test.Smoke       Test.SrcLoc+      Test.Version       Test.WASM       Agda       Agda.Convert

package.yaml view

@@ -1,6 +1,6 @@ name:                agda-language-server-version:             7-github:              "banacorn/agda-language-server"+version:             8+github:              "agda/agda-language-server" license:             MIT author:              "Ting-Gian LUA" maintainer:          "banacorn@gmail.com, Andreas Abel"

src/Options.hs view

@@ -16,7 +16,10 @@   ( Options,     defaultOptions,   )+import Data.Maybe (fromMaybe, listToMaybe)+import Data.Version (versionBranch) import GHC.Generics (Generic)+import qualified Paths_agda_language_server as Paths import System.Console.GetOpt import System.Environment (getArgs) import Text.Read (readMaybe)@@ -86,8 +89,9 @@       "print version information and exit"   ] +-- | Defaults to 0 if the version number cannot be parsed from the package version. versionNumber :: Int-versionNumber = 6+versionNumber = fromMaybe 0 (listToMaybe (versionBranch Paths.version))  versionString :: String versionString =

test/Test.hs view

@@ -3,7 +3,9 @@ import Data.Proxy (Proxy (..)) import Data.Typeable (Typeable) import qualified Test.LSP as LSP+import qualified Test.Smoke as Smoke import qualified Test.SrcLoc as SrcLoc+import qualified Test.Version as Version #if defined(wasm32_HOST_ARCH) import qualified Test.WASM as WASM #endif@@ -31,7 +33,9 @@   testGroup     "Tests"     [ SrcLoc.tests,-      LSP.tests alsPath+      Version.tests,+      LSP.tests alsPath,+      Smoke.tests alsPath #if defined(wasm32_HOST_ARCH)     , WASM.tests alsPath #endif

+ test/Test/Smoke.hs view

@@ -0,0 +1,59 @@+module Test.Smoke (tests) where++import Agda+import Control.Monad.IO.Class (liftIO)+import qualified Data.Aeson as JSON+import Language.LSP.Protocol.Message (SMethod (..), TResponseMessage (..))+import Language.LSP.Protocol.Types (HoverParams (..), Position (..))+import Language.LSP.Test (fullLatestClientCaps, openDoc, request, runSession)+import Switchboard (agdaCustomMethod)+import System.Exit (ExitCode (..))+import System.Process (readProcessWithExitCode)+import Test.Tasty+import Test.Tasty.HUnit++-- | Smoke tests against a given 'als' executable. Point '--als-path' at+-- a packaged release artifact (not the in-place '.stack-work' build) to+-- catch packaging bugs -- like #6, where the Linux release ships no+-- bundled ICU libs -- that the rest of the suite can't see, since it+-- runs against a binary on the very machine that built it, where the+-- system ICU version trivially matches by construction.+tests :: FilePath -> TestTree+tests alsPath =+  testGroup+    "Smoke"+    [ testCase "als --version" (testVersion alsPath),+      testCase "open a non-ASCII .agda file over LSP" (testUnicodeFile alsPath)+    ]++testVersion :: FilePath -> IO ()+testVersion alsPath = do+  (code, out, err) <- readProcessWithExitCode alsPath ["--version"] ""+  case code of+    ExitSuccess -> pure ()+    ExitFailure n ->+      assertFailure $+        "'" ++ alsPath ++ " --version' exited with code " ++ show n+          ++ "\nstdout: " ++ out+          ++ "\nstderr: " ++ err++-- | Opens a fixture with non-ASCII identifiers, hovers over a real+-- symbol (mirrors Test.LSP's "load" test; a position with no symbol+-- under it, e.g. (0,0), never gets a response at all), then asks the+-- server to load it via the custom agda-mode protocol. If the process+-- can't even start (e.g. the dynamic-linking failure in #6), 'runSession'+-- itself throws before either request below is reached.+testUnicodeFile :: FilePath -> IO ()+testUnicodeFile alsPath =+  runSession alsPath fullLatestClientCaps "test/data/" $ do+    doc <- openDoc "Unicode.agda" "agda"+    -- hover over "double" on its type-signature line+    _ <- request SMethod_TextDocumentHover (HoverParams doc (Position 6 2) Nothing)+    TResponseMessage _ _ rsp <-+      request agdaCustomMethod $+        JSON.toJSON $+          -- The outer IOTCM path intentionally doesn't match the real+          -- file, mirroring Test.LSP's "load" test (which uses+          -- "A.agdaa" for the same field).+          CmdReq "IOTCM \"test/data/Unicode.agdaa\" NonInteractive Direct( Cmd_load \"test/data/Unicode.agda\" [] )"+    liftIO $ rsp @?= Right (JSON.toJSON (CmdRes Nothing))

+ test/Test/Version.hs view

@@ -0,0 +1,19 @@+module Test.Version (tests) where++import Data.Version (Version (..))+import Options (versionNumber)+import qualified Paths_agda_language_server as Paths+import Test.Tasty+import Test.Tasty.HUnit++-- | Guards against the two version numbers drifting apart again, as+-- happened before #56: 'package.yaml' was bumped without updating+-- 'versionNumber' in "Options", so the reported LSP/CLI version fell+-- behind the package version.+tests :: TestTree+tests =+  testGroup+    "Version"+    [ testCase "versionNumber matches package.yaml's version" $+        Version [versionNumber] [] @?= Paths.version+    ]