agda-language-server 0.2.1 → 0.2.2.6.2
raw patch · 8 files changed
+87/−72 lines, 8 filesdep ~Agdadep ~lspnew-uploaderPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: Agda, lsp
API changes (from Hackage documentation)
- Render.Class: instance Render.Class.Render GHC.Integer.Type.Integer
+ Render.Class: instance Render.Class.Render GHC.Num.Integer.Integer
Files
- CHANGELOG.md +18/−8
- README.md +7/−2
- agda-language-server.cabal +17/−10
- package.yaml +12/−13
- src/Agda/Convert.hs +4/−3
- src/Agda/Position.hs +5/−5
- stack-8.10.yaml +19/−0
- stack.yaml +5/−31
CHANGELOG.md view
@@ -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-
README.md view
@@ -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?
agda-language-server.cabal view
@@ -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 <https://github.com/banacorn/agda-language-server#readme>+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@@ -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
package.yaml view
@@ -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 <https://github.com/banacorn/agda-language-server#readme>+description: Please see the README on GitHub at <https://github.com/agda/agda-language-server#readme> +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:
src/Agda/Convert.hs view
@@ -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
src/Agda/Position.hs view
@@ -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' =
+ stack-8.10.yaml view
@@ -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
stack.yaml view
@@ -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: