agda-language-server 8 → 9

raw patch · 5 files changed

+37/−11 lines, 5 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

CHANGELOG.md +13/−0
agda-language-server.cabal +1/−1
app/Main.hs +8/−8
package.yaml +1/−1
test/Test/Smoke.hs +14/−1

CHANGELOG.md view

@@ -4,6 +4,19 @@  The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). +## v9 - 2026-10-27++### Changed+- Move artifact-level checks off `build-and-test` onto a separate `verify-native-artifact` matrix that consumes the packaged release artifacts, and run it for every artifact that built, even if another build failed.+- Run `build-wasm` on every trigger `build-and-test` runs on.+- Check on every platform that the packaged `als` completes a load and loads only libraries from its own archive or the OS.+- Build the arm64 macOS artifact on `macos-15`.++### Fixed+- #30: Resolve the bundled data directory relative to the executable's directory, not the executable itself.+- #64: Bundle ICU's MinGW runtime DLLs into the Windows release artifact.+- Let every Agda matrix entry write its own WASM cabal store cache.+ ## v8 - 2026-09-22  ### Added

agda-language-server.cabal view

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           agda-language-server-version:        8+version:        9 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

app/Main.hs view

@@ -8,7 +8,7 @@ import System.Console.GetOpt import System.Directory (doesDirectoryExist) import System.Environment-import System.FilePath ((</>))+import System.FilePath (takeDirectory, (</>)) import System.IO import Text.Read (readMaybe) @@ -26,14 +26,14 @@  -- getExecutablePath returns argv[0] in WASM, which is useless #ifndef wasm32_HOST_ARCH-  -- The GitHub CI-built executable lacks the correct data directory path.-  -- If there's directory named "data" in the executable's directory,-  -- then we assume that the executable is built by GitHub CI-  -- and we should set the $Agda_datadir environment variable to the correct directory.+  -- A release bundle ships a "data" directory next to the executable+  -- (not inside a directory named after it). If that sibling directory+  -- exists, point $Agda_datadir at it instead of Agda's compiled-in+  -- builder path.   executablePath <- getExecutablePath-  let dataDir = executablePath </> "data"-  isBuiltByCI <- doesDirectoryExist dataDir-  when isBuiltByCI $ do+  let dataDir = takeDirectory executablePath </> "data"+  hasBundledDataDir <- doesDirectoryExist dataDir+  when hasBundledDataDir $ do     setEnv "Agda_datadir" dataDir #endif

package.yaml view

@@ -1,5 +1,5 @@ name:                agda-language-server-version:             8+version:             9 github:              "agda/agda-language-server" license:             MIT author:              "Ting-Gian LUA"

test/Test/Smoke.hs view

@@ -18,12 +18,18 @@ -- 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.+--+-- This does not cover release portability of the bundled Agda data+-- directory: it always runs on the builder, where the compiled-in+-- Stack snapshot path still resolves. See '.github/scripts/check-artifact-lsp.py'+-- for the standalone probe that verifies a completed load against a+-- packaged artifact on a machine other than the one that built it. tests :: FilePath -> TestTree tests alsPath =   testGroup     "Smoke"     [ testCase "als --version" (testVersion alsPath),-      testCase "open a non-ASCII .agda file over LSP" (testUnicodeFile alsPath)+      testCase "accept and enqueue a Cmd_load request over LSP for a non-ASCII file" (testUnicodeFile alsPath)     ]  testVersion :: FilePath -> IO ()@@ -43,6 +49,13 @@ -- 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.+--+-- The 'Cmd_load' assertion below only checks 'CmdRes Nothing', the+-- immediate acknowledgement that the request was accepted and enqueued.+-- The Agda load itself runs asynchronously and can still fail after+-- this test has already passed; this test does not wait for or assert+-- on that outcome. See '.github/scripts/check-artifact-lsp.py' for the+-- probe that waits for the completed load. testUnicodeFile :: FilePath -> IO () testUnicodeFile alsPath =   runSession alsPath fullLatestClientCaps "test/data/" $ do