v0.2.6.4.0: Build with and embed Agda-2.6.4

agda · Nov 30, 2023 · b00a86f · b00a86f
1 parent da1d928
commit b00a86f
Show file tree

Hide file tree

Showing 15 changed files with 243 additions and 43 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -4,6 +4,17 @@ 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/).
 
+## v0.2.6.4.0 - unreleased
+
+### Changed
+- Embed Agda-2.6.4.
+- Builds with `lsp` < 1.7 on GHC 9.2 (LTS 20.26),
+  and with Cabal also on 9.4 and 9.6.
+
+### Added
+- Build flag `Agda-2-6-3` to embed Agda-2.6.3 rather than 2.6.4.
+
+
 ## v0.2.6.3.0 - 2023-11-23
 
 ### Changed
@@ -14,13 +25,15 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 ### Added
 - Build flag `Agda-2-6-2-2` to embed Agda-2.6.2.2 rather than 2.6.3.
 
+
 ## v0.2.6.2.2.1 - 2023-11-21
 
 ### Added
 
 - Building with `lsp-1.6`.
   Builds with `lsp` < 1.7 on GHC 8.10 (LTS 18.28), 9.0 (LTS 19.33), and 9.2 (LTS 20.26).
 
+
 ## v0.2.6.2.2 - 2023-11-21
 
 ### Changed
@@ -29,25 +42,30 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - 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
 - Resume sending HighlightingInfos to agda-mode
 
+
 ## v0.1.3 - 2021-10-04
 
 ### Fixed
 - Include DLLs in the bundle
 
+
 ## v0.1.2 - 2021-10-03
 
 ### Fixed

diff --git a/README.md b/README.md
@@ -21,8 +21,7 @@ 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).
+The version is _x.a.b.c.d.y_ where _a.b.c.d_ is the 4-digit Agda version (2.6.4.0), _x_ is 0 but may be bumped for revolutionary changes to the agda-language-server, and _y_ is for patch releases.
 
 ## Why make it standalone?
 

diff --git a/agda-language-server.cabal b/agda-language-server.cabal
@@ -5,15 +5,15 @@ cabal-version: 1.12
 -- see: https://github.com/sol/hpack
 
 name:           agda-language-server
-version:        0.2.6.3.0
+version:        0.2.6.4.0
 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
 author:         Ting-Gian LUA
-maintainer:     [email protected]
-copyright:      2020 Author name here :)
+maintainer:     [email protected], Andreas Abel
+copyright:      2020-23 Ting-Gian LUA, Andreas ABEL
 license:        MIT
 license-file:   LICENSE
 build-type:     Simple
@@ -25,13 +25,19 @@ extra-source-files:
     stack-8.10-Agda-2.6.2.2.yaml
     stack-9.0-Agda-2.6.2.2.yaml
     stack-9.2-Agda-2.6.2.2.yaml
+    stack-9.2-Agda-2.6.3.yaml
 
 source-repository head
   type: git
   location: https://github.com/banacorn/agda-language-server
 
 flag Agda-2-6-2-2
-  description: Embed Agda-2.6.2.2 (rather than 2.6.3)
+  description: Embed Agda-2.6.2.2 (rather than 2.6.4)
+  manual: True
+  default: False
+
+flag Agda-2-6-3
+  description: Embed Agda-2.6.3 (rather than 2.6.4)
   manual: True
   default: False
 
@@ -77,21 +83,29 @@ library
     , base >=4.7 && <5
     , bytestring
     , containers
-    , lsp <1.7
+    , lsp <2
+    , lsp-types <2
     , mtl
     , network
     , network-simple
+    , prettyprinter
     , process
     , stm
     , strict
     , text
   default-language: Haskell2010
-  if flag(Agda-2-6-2-2)
+  if flag(Agda-2-6-2-2) && !flag(Agda-2-6-3)
     build-depends:
         Agda ==2.6.2.2
-  else
+  if !flag(Agda-2-6-2-2) && flag(Agda-2-6-3)
     build-depends:
         Agda ==2.6.3
+  if !flag(Agda-2-6-2-2) && !flag(Agda-2-6-3)
+    build-depends:
+        Agda ==2.6.4
+  if flag(Agda-2-6-2-2) && flag(Agda-2-6-3)
+    build-depends:
+        Agda <0
 
 executable als
   main-is: Main.hs
@@ -111,21 +125,29 @@ executable als
     , base >=4.7 && <5
     , bytestring
     , containers
-    , lsp <1.7
+    , lsp <2
+    , lsp-types <2
     , mtl
     , network
     , network-simple
+    , prettyprinter
     , process
     , stm
     , strict
     , text
   default-language: Haskell2010
-  if flag(Agda-2-6-2-2)
+  if flag(Agda-2-6-2-2) && !flag(Agda-2-6-3)
     build-depends:
         Agda ==2.6.2.2
-  else
+  if !flag(Agda-2-6-2-2) && flag(Agda-2-6-3)
     build-depends:
         Agda ==2.6.3
+  if !flag(Agda-2-6-2-2) && !flag(Agda-2-6-3)
+    build-depends:
+        Agda ==2.6.4
+  if flag(Agda-2-6-2-2) && flag(Agda-2-6-3)
+    build-depends:
+        Agda <0
 
 test-suite als-test
   type: exitcode-stdio-1.0
@@ -172,10 +194,12 @@ test-suite als-test
     , base >=4.7 && <5
     , bytestring
     , containers
-    , lsp <1.7
+    , lsp <2
+    , lsp-types <2
     , mtl
     , network
     , network-simple
+    , prettyprinter
     , process
     , stm
     , strict
@@ -185,9 +209,15 @@ test-suite als-test
     , tasty-quickcheck
     , text
   default-language: Haskell2010
-  if flag(Agda-2-6-2-2)
+  if flag(Agda-2-6-2-2) && !flag(Agda-2-6-3)
     build-depends:
         Agda ==2.6.2.2
-  else
+  if !flag(Agda-2-6-2-2) && flag(Agda-2-6-3)
     build-depends:
         Agda ==2.6.3
+  if !flag(Agda-2-6-2-2) && !flag(Agda-2-6-3)
+    build-depends:
+        Agda ==2.6.4
+  if flag(Agda-2-6-2-2) && flag(Agda-2-6-3)
+    build-depends:
+        Agda <0
diff --git a/package.yaml b/package.yaml
@@ -1,10 +1,10 @@
 name:                agda-language-server
-version:             0.2.6.3.0
+version:             0.2.6.4.0
 github:              "banacorn/agda-language-server"
 license:             MIT
 author:              "Ting-Gian LUA"
-maintainer:          "[email protected]"
-copyright:           "2020 Author name here :)"
+maintainer:          "[email protected], Andreas Abel"
+copyright:           "2020-23 Ting-Gian LUA, Andreas ABEL"
 
 extra-source-files:
 - README.md
@@ -14,6 +14,7 @@ extra-source-files:
 - stack-8.10-Agda-2.6.2.2.yaml
 - stack-9.0-Agda-2.6.2.2.yaml
 - stack-9.2-Agda-2.6.2.2.yaml
+- stack-9.2-Agda-2.6.3.yaml
 
 # Metadata used when publishing your package
 synopsis:            An implementation of language server protocal (LSP) for Agda 2.
@@ -26,33 +27,44 @@ description:         Please see the README on GitHub at <https://github.com/agda
 
 flags:
   Agda-2-6-2-2:
-    description: Embed Agda-2.6.2.2 (rather than 2.6.3)
+    description: Embed Agda-2.6.2.2 (rather than 2.6.4)
+    manual: true
+    default: false
+  Agda-2-6-3:
+    description: Embed Agda-2.6.3 (rather than 2.6.4)
     manual: true
     default: false
 
 when:
-- condition: flag(Agda-2-6-2-2)
-  then:
-    dependencies:
+- condition: "flag(Agda-2-6-2-2) && !flag(Agda-2-6-3)"
+  dependencies:
     - Agda == 2.6.2.2
-  else:
-    dependencies:
+- condition: "!flag(Agda-2-6-2-2) && flag(Agda-2-6-3)"
+  dependencies:
     - Agda == 2.6.3
+- condition: "!flag(Agda-2-6-2-2) && !flag(Agda-2-6-3)"
+  dependencies:
+    - Agda == 2.6.4
+- condition: "flag(Agda-2-6-2-2) && flag(Agda-2-6-3)"
+  dependencies:
+    - Agda < 0
 
 dependencies:
   - base >= 4.7 && < 5
   - Agda
   - aeson
   - bytestring
   - containers
-  - lsp < 1.7
+  - lsp-types < 2
+  - lsp < 2
   - mtl
   - network
   - network-simple
   - strict
   - stm
   - text
   - process
+  - prettyprinter
 
 default-extensions:
 - LambdaCase

diff --git a/src/Agda.hs b/src/Agda.hs
@@ -10,6 +10,8 @@ module Agda
   , getCommandLineOptions
   ) where
 
+import           Prelude                        hiding ( null )
+
 import           Agda.Compiler.Backend          ( parseBackendOptions )
 import           Agda.Compiler.Builtin          ( builtinBackends )
 import           Agda.Convert                   ( fromResponse )
@@ -23,6 +25,9 @@ import           Agda.Interaction.Base          ( Command
                                                 , parseIOTCM
 #endif
                                                 )
+#if MIN_VERSION_Agda(2,6,4)
+import           Agda.Syntax.Common.Pretty      ( render, vcat )
+#endif
 import           Agda.Interaction.InteractionTop
                                                 ( initialiseCommandQueue
                                                 , maybeAbort
@@ -53,6 +58,7 @@ import           Agda.Utils.Impossible          ( CatchImpossible
                                                   )
                                                 , Impossible
                                                 )
+import           Agda.Utils.Null                ( null )
 import           Agda.VersionCommit             ( versionWithCommitInfo )
 import           Control.Exception              ( SomeException
                                                 , catch
@@ -218,7 +224,11 @@ runAgda p = do
     s2s <- prettyTCWarnings' =<< getAllWarningsOfTCErr err
     s1  <- prettyError err
     let ss       = filter (not . null) $ s2s ++ [s1]
+#if MIN_VERSION_Agda(2,6,4)
+    let errorMsg = render $ vcat ss
+#else
     let errorMsg = unlines ss
+#endif
     return (Left errorMsg)
 
   handleImpossible :: Impossible -> TCM (Either String a)

diff --git a/src/Agda/Convert.hs b/src/Agda/Convert.hs
@@ -38,7 +38,13 @@ import Agda.Utils.IO.TempFile (writeToTempFile)
 import Agda.Utils.Impossible (__IMPOSSIBLE__)
 import Agda.Utils.Maybe (catMaybes)
 import Agda.Utils.Null (empty)
+#if MIN_VERSION_Agda(2,6,4)
+import Agda.Syntax.Common.Pretty hiding (render)
+-- import Prettyprinter hiding (Doc)
+import qualified Prettyprinter
+#else
 import Agda.Utils.Pretty hiding (render)
+#endif
 import Agda.Utils.RangeMap ( IsBasicRangeMap(toList) )
 import Agda.Utils.String (delimiter)
 import Agda.Utils.Time (CPUTime)
@@ -306,7 +312,12 @@ lispifyGoalSpecificDisplayInfo ii kind = localTCState $
 
         auxSect <- case aux of
           GoalOnly -> return []
+#if MIN_VERSION_Agda(2,6,4)
+          GoalAndHave expr bndry -> do
+            -- TODO: render bndry
+#else
           GoalAndHave expr -> do
+#endif
             rendered <- renderATop expr
             raw <- show <$> prettyATop expr
             return [Labeled rendered (Just raw) Nothing "Have" "special"]
@@ -456,7 +467,11 @@ prettyResponseContext ::
   ResponseContextEntry ->
   TCM [(String, Doc)]
 prettyResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = withInteractionId ii $ do
+#if MIN_VERSION_Agda(2,6,4)
+  modality <- currentModality
+#else
   modality <- asksTC getModality
+#endif
   do
     let prettyCtxName :: String
         prettyCtxName
@@ -505,7 +520,11 @@ renderResponseContext ::
   ResponseContextEntry ->
   TCM [Block]
 renderResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = withInteractionId ii $ do
+#if MIN_VERSION_Agda(2,6,4)
+  modality <- currentModality
+#else
   modality <- asksTC getModality
+#endif
   do
     let
         rawCtxName :: String