diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,26 +2,36 @@ All notable changes to this project will be documented in this file. -The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), -and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). -## v0.2.0 - TBA +## v0.2.6.2.2 - 2023-11-21 -### Fixed +### Changed + +- Bundle Agda-2.6.2.2 +- Versioning scheme: _x.a.b.c.d.y_ where _a.b.c.d_ is the 4-digit Agda version (2.6.2.2), _x_ is 0 but may be bumped for revolutionary changes to the agda-language-server, and _y_ is for patch releases +- Builds with `lsp` < 1.5 on GHC 8.10 (LTS 18.28) and 9.0 (LTS 19.33) + +## v0.2.1 - 2021-10-25 + +No changes. + +## v0.2.0 - 2021-10-22 + +### Fixed - #2: Allow user to supply command-line options via agda-mode ## v0.1.4 - 2021-10-04 -### Fixed +### Fixed - Resume sending HighlightingInfos to agda-mode ## v0.1.3 - 2021-10-04 -### Fixed +### Fixed - Include DLLs in the bundle ## v0.1.2 - 2021-10-03 -### Fixed +### Fixed - #5: Connection Error - diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,13 +1,13 @@ # Agda Language Server -## Installation +## Installation The simplest way of acquiring Agda Language Server is through [agda-mode on VS Code](https://github.com/banacorn/agda-mode-vscode#agda-language-server). Follow the instructions and the language server should be installed within seconds. ### Prebuilt binaries -You can also download prebuilt binaries [from the release page](https://github.com/banacorn/agda-language-server/releases) if you are using other LSP-compatible text editors. +You can also download prebuilt binaries [from the release page](https://github.com/banacorn/agda-language-server/releases) if you are using other LSP-compatible text editors. Supported platforms: **Windows**, **Mac**, and **Ubuntu**. @@ -18,6 +18,11 @@ ``` stack install ``` + +## Versioning + +The version is _x.y.z.w.a.b.c.d_ where _x.y.z.w_ is the version of the Agda Language Server and _a.b.c.d_ the version of Agda it embeds. +It follows the Haskell PVP (package versioning policy). ## Why make it standalone? diff --git a/agda-language-server.cabal b/agda-language-server.cabal --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -1,13 +1,13 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.34.4. +-- This file has been generated from package.yaml by hpack version 0.36.0. -- -- see: https://github.com/sol/hpack name: agda-language-server -version: 0.2.1 +version: 0.2.2.6.2 synopsis: An implementation of language server protocal (LSP) for Agda 2. -description: Please see the README on GitHub at +description: Please see the README on GitHub at category: Development homepage: https://github.com/banacorn/agda-language-server#readme bug-reports: https://github.com/banacorn/agda-language-server/issues @@ -20,8 +20,9 @@ extra-source-files: README.md CHANGELOG.md - stack.yaml package.yaml + stack.yaml + stack-8.10.yaml source-repository head type: git @@ -61,14 +62,15 @@ default-extensions: LambdaCase OverloadedStrings + TypeOperators 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 + Agda ==2.6.2.2 , aeson , base >=4.7 && <5 , bytestring , containers - , lsp <2 + , lsp <1.5 , mtl , network , network-simple @@ -84,15 +86,19 @@ Paths_agda_language_server hs-source-dirs: app + default-extensions: + LambdaCase + OverloadedStrings + TypeOperators 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 + Agda ==2.6.2.2 , aeson , agda-language-server , base >=4.7 && <5 , bytestring , containers - , lsp <2 + , lsp <1.5 , mtl , network , network-simple @@ -139,14 +145,15 @@ default-extensions: LambdaCase OverloadedStrings + TypeOperators 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 + Agda ==2.6.2.2 , aeson , base >=4.7 && <5 , bytestring , containers - , lsp <2 + , lsp <1.5 , mtl , network , network-simple diff --git a/package.yaml b/package.yaml --- a/package.yaml +++ b/package.yaml @@ -1,5 +1,5 @@ name: agda-language-server -version: 0.2.1 +version: 0.2.2.6.2 github: "banacorn/agda-language-server" license: MIT author: "Ting-Gian LUA" @@ -9,25 +9,31 @@ extra-source-files: - README.md - CHANGELOG.md -- stack.yaml - package.yaml +- stack.yaml +- stack-8.10.yaml # Metadata used when publishing your package -synopsis: An implementation of language server protocal (LSP) for Agda 2. +synopsis: An implementation of language server protocal (LSP) for Agda 2. category: Development # To avoid duplicated efforts in documentation and dealing with the # complications of embedding Haddock markup inside cabal files, it is # common to point users to the README.md file. -description: Please see the README on GitHub at +description: Please see the README on GitHub at +default-extensions: +- LambdaCase +- OverloadedStrings +- TypeOperators + dependencies: - base >= 4.7 && < 5 - - Agda == 2.6.2 + - Agda == 2.6.2.2 - aeson - bytestring - containers - - lsp < 2 + - lsp < 1.5 - mtl - network - network-simple @@ -50,9 +56,6 @@ - -Wmissing-signatures - -Werror=incomplete-patterns - -fno-warn-orphans - default-extensions: - - LambdaCase - - OverloadedStrings executables: als: @@ -103,10 +106,6 @@ - -with-rtsopts=-N - -Werror=incomplete-patterns - -fno-warn-orphans - - default-extensions: - - LambdaCase - - OverloadedStrings # tests: # als-test: diff --git a/src/Agda/Convert.hs b/src/Agda/Convert.hs --- a/src/Agda/Convert.hs +++ b/src/Agda/Convert.hs @@ -21,6 +21,7 @@ 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') @@ -129,8 +130,8 @@ indirect = liftIO $ writeToTempFile (BS8.unpack (JSON.encode info)) fromDisplayInfo :: DisplayInfo -> TCM IR.DisplayInfo -fromDisplayInfo info = case info of - Info_CompilationOk ws -> do +fromDisplayInfo = \case + Info_CompilationOk _ ws -> do -- filter let filteredWarnings = filterTCWarnings (tcWarnings ws) let filteredErrors = filterTCWarnings (nonFatalErrors ws) @@ -278,7 +279,7 @@ 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 diff --git a/src/Agda/Position.hs b/src/Agda/Position.hs --- a/src/Agda/Position.hs +++ b/src/Agda/Position.hs @@ -42,7 +42,7 @@ 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) @@ -55,7 +55,7 @@ -- Keeps record of offsets of every line break ("\n", "\r" and "\r\n") -- --- Example text corresponding entry of IntMap +-- Example text corresponding entry of IntMap -- >abc\n (1, 4) -- >def123\r\n (2, 11) -- >ghi\r (3, 15) @@ -97,7 +97,7 @@ -- An IntMap for speeding up Offset => Position convertion -- Keeps record of offsets of every line break ("\n", "\r" and "\r\n") -- --- Example text corresponding entry of IntMap +-- Example text corresponding entry of IntMap -- >abc\n (4, 1) -- >def123\r\n (11, 2) -- >ghi\r (15, 3) @@ -115,11 +115,11 @@ (Accum Nothing 0 0 IntMap.empty) where go :: Accum -> Char -> Accum - -- encountered a "\r\n", update the latest entry + -- encountered a "\r\n", update the latest entry go (Accum (Just '\r') n l table) '\n' = case IntMap.deleteFindMax table of ((offset, lineNo), table') -> Accum (Just '\n') (1 + n) l (IntMap.insert (1 + offset) lineNo table') - -- encountered a line break, add a new entry + -- encountered a line break, add a new entry go (Accum previous n l table) '\n' = Accum (Just '\n') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table) go (Accum previous n l table) '\r' = diff --git a/stack-8.10.yaml b/stack-8.10.yaml new file mode 100644 --- /dev/null +++ b/stack-8.10.yaml @@ -0,0 +1,19 @@ +resolver: lts-18.28 +compiler: ghc-8.10.7 +# Allow a newer minor version of GHC than the snapshot specifies +compiler-check: newer-minor + +packages: +- . + +# Use some newer versions than in the lts-18.28 snapshot +extra-deps: +- Agda-2.6.2.2 +- text-icu-0.8.0.1 +- lsp-1.2.0.1 +- lsp-types-1.3.0.1 + +flags: + Agda: + # optimise-heavily: true + enable-cluster-counting: true diff --git a/stack.yaml b/stack.yaml --- a/stack.yaml +++ b/stack.yaml @@ -1,40 +1,14 @@ -resolver: lts-18.5 +resolver: lts-19.33 +compiler: ghc-9.0.2 # Allow a newer minor version of GHC than the snapshot specifies -compiler-check: match-exact +compiler-check: newer-minor -# User packages to be built. -# Various formats can be used as shown in the example below. -# -# packages: -# - some-directory -# - https://example.com/foo/bar/baz-0.0.2.tar.gz -# subdirs: -# - auto-update -# - wai packages: - . +# Use some newer versions than in the lts-19.33 snapshot extra-deps: - # LSP - - lexer-applicative-2.1.0.2 - - github: haskell/lsp - commit: dce30c9d345f63921cf9cf5045e1dcd753e4fe34 - subdirs: - - lsp - - github: haskell/lsp - commit: dce30c9d345f63921cf9cf5045e1dcd753e4fe34 - subdirs: - - lsp-types - # - some-1.0.1@sha256:26e5bab7276f48b25ea8660d3fd1166c0f20fd497dac879a40f408e23211f93e,2055 - - dependent-map-0.4.0.0@sha256:ca2b131046f4340a1c35d138c5a003fe4a5be96b14efc26291ed35fd08c62221,1657 - - dependent-sum-0.7.1.0@sha256:0e419237f5b86da3659772afff9cab355c0f8d5b3fdb15a5b30e673d8dc83941,2147 - - dependent-sum-template-0.1.0.3@sha256:0bbbacdfbd3abf2a15aaf0cf2c27e5bdd159b519441fec39e1e6f2f54424adde,1682 - - unliftio-core-0.2.0.1@sha256:9b3e44ea9aacacbfc35b3b54015af450091916ac3618a41868ebf6546977659a,1082 - - constraints-extras-0.3.1.0@sha256:12016ebb91ad5ed2c82bf7e48c6bd6947d164d33c9dca5ac3965de1bb6c780c0,1777 - - constraints-0.12@sha256:71c7999d7fa01d8941f08d37d4c107c6b1bcbd0306e234157557b9b096b7f1be,2217 - - - +- text-icu-0.8.0.1 flags: Agda: