v0.2.6.3.0 Build with and embed Agda-2.6.3

This uses CPP, so one can still build with Agda-2.6.2.2 if wanted.

Author: andreasabel

CHANGELOG.md

@@ -4,20 +4,27 @@ 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.3.0 - 2023-11-23
+
+### Changed
+- Bundle Agda-2.6.3.
+- Builds with `lsp` < 1.7 on GHC 8.10 (LTS 18.28), 9.0 (LTS 19.33), and 9.2 (LTS 20.26),
+  and with Cabal also on 9.4 and 9.6.
+
 ## 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)
+  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
 
-- 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)
+- 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
 

agda-language-server.cabal

@@ -5,7 +5,7 @@ cabal-version: 1.12
 -- see: https://github.com/sol/hpack
 
 name:           agda-language-server
-version:        0.2.6.2.2.1
+version:        0.2.6.3.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
@@ -22,8 +22,9 @@ extra-source-files:
     CHANGELOG.md
     package.yaml
     stack.yaml
-    stack-8.10.yaml
-    stack-9.0.yaml
+    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
 
 source-repository head
   type: git
@@ -66,7 +67,7 @@ library
       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.2
+      Agda ==2.6.3
     , aeson
     , base >=4.7 && <5
     , bytestring
@@ -93,7 +94,7 @@ executable als
       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.2
+      Agda ==2.6.3
     , aeson
     , agda-language-server
     , base >=4.7 && <5
@@ -149,7 +150,7 @@ test-suite als-test
       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.2
+      Agda ==2.6.3
     , aeson
     , base >=4.7 && <5
     , bytestring

package.yaml

@@ -1,5 +1,5 @@
 name:                agda-language-server
-version:             0.2.6.2.2.1
+version:             0.2.6.3.0
 github:              "banacorn/agda-language-server"
 license:             MIT
 author:              "Ting-Gian LUA"
@@ -11,8 +11,9 @@ extra-source-files:
 - CHANGELOG.md
 - package.yaml
 - stack.yaml
-- stack-8.10.yaml
-- stack-9.0.yaml
+- 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
 
 # Metadata used when publishing your package
 synopsis:            An implementation of language server protocal (LSP) for Agda 2.
@@ -30,7 +31,7 @@ default-extensions:
 
 dependencies:
   - base >= 4.7 && < 5
-  - Agda == 2.6.2.2
+  - Agda == 2.6.3
   - aeson
   - bytestring
   - containers

src/Agda.hs

@@ -1,4 +1,6 @@
 {-# OPTIONS_GHC -Wno-missing-methods #-}
+
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveGeneric #-}
 
 module Agda
@@ -17,6 +19,9 @@ import           Agda.Interaction.Base          ( Command
                                                 , CommandState(optionsOnReload)
                                                 , IOTCM
                                                 , initCommandState
+#if MIN_VERSION_Agda(2,6,3)
+                                                , parseIOTCM
+#endif
                                                 )
 import           Agda.Interaction.InteractionTop
                                                 ( initialiseCommandQueue
@@ -52,6 +57,7 @@ import           Agda.VersionCommit             ( versionWithCommitInfo )
 import           Control.Exception              ( SomeException
                                                 , catch
                                                 )
+import           Control.Monad
 import           Control.Monad.Except
 import           Control.Monad.Reader
 import           Control.Monad.State
@@ -88,7 +94,7 @@ start = do
     -- keep reading command
     commands <- liftIO $ initialiseCommandQueue (readCommand env)
 
-    -- get command line options 
+    -- get command line options
     options  <- getCommandLineOptions
 
     -- start the loop
@@ -159,31 +165,37 @@ handleCommandReq (CmdReq cmd) = do
       provideCommand iotcm
       return $ CmdRes Nothing
 
+#if !MIN_VERSION_Agda(2,6,3)
 parseIOTCM :: String -> Either String IOTCM
 parseIOTCM raw = case listToMaybe $ reads raw of
   Just (x, ""     ) -> Right x
   Just (_, remnent) -> Left $ "not consumed: " ++ remnent
   _                 -> Left $ "cannot read: " ++ raw
+#endif
 
 --------------------------------------------------------------------------------
 
 getCommandLineOptions
   :: (HasOptions m, MonadIO m) => ServerM m CommandLineOptions
 getCommandLineOptions = do
-  -- command line options from ARGV 
+  -- command line options from ARGV
   argv   <- asks (optRawAgdaOptions . envOptions)
   -- command line options from agda-mode
   config <- asks (configRawAgdaOptions . envConfig)
-  -- concatenate both 
+  -- concatenate both
   let merged = argv <> config
 
   result <- runExceptT $ do
-    (bs, opts) <- ExceptT $ runOptM $ parseBackendOptions builtinBackends
-                                                          merged
-                                                          defaultOptions
+    let p = parseBackendOptions builtinBackends merged defaultOptions
+#if MIN_VERSION_Agda(2,6,3)
+    let (r, _warns) = runOptM p
+    (bs, opts) <- ExceptT $ pure r
+#else
+    (bs, opts) <- ExceptT $ runOptM p
+#endif
     return opts
   case result of
-    -- something bad happened, use the default options instead 
+    -- something bad happened, use the default options instead
     Left  _    -> commandLineOptions
     Right opts -> return opts
 

src/Agda/Convert.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE CPP #-}
+
 module Agda.Convert where
 
 import Render ( Block(..), Inlines, renderATop, Render(..) )
@@ -33,10 +35,11 @@ import Agda.Utils.Impossible (__IMPOSSIBLE__)
 import Agda.Utils.Maybe (catMaybes)
 import Agda.Utils.Null (empty)
 import Agda.Utils.Pretty hiding (render)
-import Agda.Utils.RangeMap ( IsBasicRangeMap(toList) ) 
+import Agda.Utils.RangeMap ( IsBasicRangeMap(toList) )
 import Agda.Utils.String (delimiter)
 import Agda.Utils.Time (CPUTime)
 import Agda.VersionCommit (versionWithCommitInfo)
+import Control.Monad
 import Control.Monad.State hiding (state)
 import qualified Data.Aeson as JSON
 import qualified Data.ByteString.Lazy.Char8 as BS8
@@ -130,7 +133,7 @@ fromHighlightingInfo h remove method modFile =
     indirect = liftIO $ writeToTempFile (BS8.unpack (JSON.encode info))
 
 fromDisplayInfo :: DisplayInfo -> TCM IR.DisplayInfo
-fromDisplayInfo = \case 
+fromDisplayInfo = \case
   Info_CompilationOk _ ws -> do
     -- filter
     let filteredWarnings = filterTCWarnings (tcWarnings ws)
@@ -255,8 +258,13 @@ fromDisplayInfo = \case
           "Definitions about"
             <+> text (List.intercalate ", " $ words names) $$ nest 2 (align 10 hitDocs)
     return $ IR.DisplayInfoGeneric "Search About" [Unlabeled (Render.text $ show doc) Nothing Nothing]
+#if MIN_VERSION_Agda(2,6,3)
+  Info_WhyInScope (WhyInScopeData q cwd v xs ms) -> do
+    doc <- explainWhyInScope (prettyShow q) cwd v xs ms
+#else
   Info_WhyInScope s cwd v xs ms -> do
     doc <- explainWhyInScope s cwd v xs ms
+#endif
     return $ IR.DisplayInfoGeneric "Scope Info" [Unlabeled (Render.text $ show doc) Nothing Nothing]
   Info_Context ii ctx -> do
     doc <- localTCState (prettyResponseContexts ii False ctx)
@@ -373,8 +381,8 @@ showInfoError (Info_HighlightingScopeCheckError ii) =
   return $ "Highlighting failed to scope check expression in " ++ show ii
 
 explainWhyInScope ::
-  FilePath ->
   String ->
+  FilePath ->
   Maybe LocalVar ->
   [AbstractName] ->
   [AbstractModule] ->
@@ -577,12 +585,12 @@ renderResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = wit
     -- raw
     rawExpr <- prettyATop expr
     let rawType = show $ align 10 [(rawAttribute ++ rawCtxName, ":" <+> rawExpr <+> parenSep extras)]
-    -- rendered  
+    -- rendered
     renderedExpr <- renderATop expr
     let renderedType = (renderedCtxName <> renderedAttribute) Render.<+> ":" Render.<+> renderedExpr Render.<+> parenSep2 extras2
       -- (Render.fsep $ Render.punctuate "," extras)
 
-    -- result 
+    -- result
     let typeItem = Unlabeled renderedType (Just rawType) Nothing
 
     valueItem <- case letv of

src/Agda/Parser.hs

@@ -1,10 +1,15 @@
+{-# LANGUAGE CPP #-}
+
 module Agda.Parser where
 
 --------------------------------------------------------------------------------
 
 import Agda.Syntax.Parser (parseFile, runPMIO, tokensParser)
 import Agda.Syntax.Parser.Tokens (Token)
 import Agda.Syntax.Position (Position' (posPos), PositionWithoutFile, Range, getRange, rEnd', rStart')
+#if MIN_VERSION_Agda(2,6,3)
+import Agda.Syntax.Position (RangeFile(RangeFile))
+#endif
 import Agda.Utils.FileName (mkAbsolute)
 import Monad ( ServerM )
 import Control.Monad.State
@@ -22,10 +27,22 @@ tokenAt :: LSP.Uri -> Text -> PositionWithoutFile -> ServerM (LspM Config) (Mayb
 tokenAt uri source position = case LSP.uriToFilePath uri of
   Nothing -> return Nothing
   Just filepath -> do
+    let file =
+#if MIN_VERSION_Agda(2,6,3)
+          RangeFile (mkAbsolute filepath) Nothing
+#else
+          mkAbsolute filepath
+#endif
     (result, _warnings) <- liftIO $
       runPMIO $ do
         -- parse the file and get all tokens
-        (tokens, _fileType) <- parseFile tokensParser (mkAbsolute filepath) (unpack source)
+        (r, _fileType) <- parseFile tokensParser file (unpack source)
+        let tokens =
+#if MIN_VERSION_Agda(2,6,3)
+              fst r
+#else
+              r
+#endif
         -- find the token at the position
         return $ find (pointedBy position) tokens
     case result of
@@ -54,4 +71,4 @@ tokenAt uri source position = case LSP.uriToFilePath uri of
     tokenOffsets :: Token -> Maybe (Int, Int)
     tokenOffsets token = do
       (start, end) <- startAndEnd (getRange token)
-      return (fromIntegral (posPos start), fromIntegral (posPos end))
+      return (fromIntegral (posPos start), fromIntegral (posPos end))

src/Agda/Position.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE CPP #-}
+
 module Agda.Position
   ( ToOffset(..)
   , makeToOffset
@@ -31,12 +33,17 @@ import qualified Language.LSP.Types            as LSP
 -- | LSP Range -> Agda Range
 toAgdaRange :: ToOffset -> Text -> LSP.Range -> Range
 toAgdaRange table path (LSP.Range start end) = Range
-  (Strict.Just (AbsolutePath path))
+  (Strict.Just $ mkRangeFile $ AbsolutePath path)
   (Seq.singleton interval)
  where
   interval :: IntervalWithoutFile
   interval = Interval (toAgdaPositionWithoutFile table start)
                       (toAgdaPositionWithoutFile table end)
+#if MIN_VERSION_Agda(2,6,3)
+  mkRangeFile path = RangeFile path Nothing
+#else
+  mkRangeFile = id
+#endif
 
 -- | LSP Position -> Agda PositionWithoutFile
 toAgdaPositionWithoutFile :: ToOffset -> LSP.Position -> PositionWithoutFile

src/Render/Common.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE CPP #-}
+
 module Render.Common where
 
 import Agda.Syntax.Common
@@ -30,7 +32,11 @@ instance Render NameId where
 
 -- | MetaId
 instance Render MetaId where
+#if MIN_VERSION_Agda(2,6,3)
+  render (MetaId n m) = text $ "_" ++ show n ++ "@" ++ show m
+#else
   render (MetaId n) = text $ "_" ++ show n
+#endif
 
 -- | Relevance
 instance Render Relevance where