diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,20 +4,30 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). +## v0.2.6.3.0 - 2023-11-23 + +### Changed +- Embed 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. + +### 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) + 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) +- Embed 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 diff --git a/agda-language-server.cabal b/agda-language-server.cabal --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -5,7 +5,7 @@ -- 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 category: Development @@ -22,13 +22,19 @@ 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 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) + manual: True + default: False + library exposed-modules: Agda @@ -66,7 +72,7 @@ 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 , aeson , base >=4.7 && <5 , bytestring @@ -80,6 +86,12 @@ , strict , text default-language: Haskell2010 + if flag(Agda-2-6-2-2) + build-depends: + Agda ==2.6.2.2 + else + build-depends: + Agda ==2.6.3 executable als main-is: Main.hs @@ -93,7 +105,7 @@ 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 , aeson , agda-language-server , base >=4.7 && <5 @@ -108,6 +120,12 @@ , strict , text default-language: Haskell2010 + if flag(Agda-2-6-2-2) + build-depends: + Agda ==2.6.2.2 + else + build-depends: + Agda ==2.6.3 test-suite als-test type: exitcode-stdio-1.0 @@ -149,7 +167,7 @@ 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 , aeson , base >=4.7 && <5 , bytestring @@ -167,3 +185,9 @@ , tasty-quickcheck , text default-language: Haskell2010 + if flag(Agda-2-6-2-2) + build-depends: + Agda ==2.6.2.2 + else + build-depends: + Agda ==2.6.3 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.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 @@ - 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. @@ -23,14 +24,24 @@ # common to point users to the README.md file. description: Please see the README on GitHub at -default-extensions: -- LambdaCase -- OverloadedStrings -- TypeOperators +flags: + Agda-2-6-2-2: + description: Embed Agda-2.6.2.2 (rather than 2.6.3) + manual: true + default: false +when: +- condition: flag(Agda-2-6-2-2) + then: + dependencies: + - Agda == 2.6.2.2 + else: + dependencies: + - Agda == 2.6.3 + dependencies: - base >= 4.7 && < 5 - - Agda == 2.6.2.2 + - Agda - aeson - bytestring - containers @@ -42,6 +53,11 @@ - stm - text - process + +default-extensions: +- LambdaCase +- OverloadedStrings +- TypeOperators library: source-dirs: src diff --git a/src/Agda.hs b/src/Agda.hs --- a/src/Agda.hs +++ b/src/Agda.hs @@ -1,4 +1,6 @@ {-# OPTIONS_GHC -Wno-missing-methods #-} + +{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveGeneric #-} module Agda @@ -17,6 +19,9 @@ , CommandState(optionsOnReload) , IOTCM , initCommandState +#if MIN_VERSION_Agda(2,6,3) + , parseIOTCM +#endif ) import Agda.Interaction.InteractionTop ( initialiseCommandQueue @@ -52,6 +57,7 @@ import Control.Exception ( SomeException , catch ) +import Control.Monad import Control.Monad.Except import Control.Monad.Reader import Control.Monad.State @@ -88,7 +94,7 @@ -- 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 @@ 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 diff --git a/src/Agda/Convert.hs b/src/Agda/Convert.hs --- a/src/Agda/Convert.hs +++ b/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.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 @@ 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 @@ "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 @@ return $ "Highlighting failed to scope check expression in " ++ show ii explainWhyInScope :: - FilePath -> String -> + FilePath -> Maybe LocalVar -> [AbstractName] -> [AbstractModule] -> @@ -577,12 +585,12 @@ -- 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 diff --git a/src/Agda/Parser.hs b/src/Agda/Parser.hs --- a/src/Agda/Parser.hs +++ b/src/Agda/Parser.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE CPP #-} + module Agda.Parser where -------------------------------------------------------------------------------- @@ -5,6 +7,9 @@ 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 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 diff --git a/src/Agda/Position.hs b/src/Agda/Position.hs --- a/src/Agda/Position.hs +++ b/src/Agda/Position.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE CPP #-} + module Agda.Position ( ToOffset(..) , makeToOffset @@ -31,12 +33,17 @@ -- | 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 diff --git a/src/Render/Common.hs b/src/Render/Common.hs --- a/src/Render/Common.hs +++ b/src/Render/Common.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE CPP #-} + module Render.Common where import Agda.Syntax.Common @@ -30,7 +32,11 @@ -- | 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 diff --git a/src/Render/Concrete.hs b/src/Render/Concrete.hs --- a/src/Render/Concrete.hs +++ b/src/Render/Concrete.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE RankNTypes #-} @@ -12,7 +13,7 @@ import Agda.Syntax.Concrete import Agda.Syntax.Concrete.Pretty (NamedBinding (..), Tel (..), isLabeled) --import Agda.Syntax.Position (noRange) -import Agda.Utils.List1 as List1 (toList, fromList) +import Agda.Utils.List1 as List1 (toList, fromList) import qualified Agda.Utils.List1 as List1 import qualified Agda.Utils.List2 as List2 import Agda.Utils.Float (toStringWithoutDotZero) @@ -29,6 +30,9 @@ -------------------------------------------------------------------------------- +instance Render a => Render (Ranged a) where + render = render . rangedThing + instance Render a => Render (WithHiding a) where render w = renderHiding w id $ render $ dget w @@ -108,8 +112,10 @@ Rec _ xs -> sep ["record", bracesAndSemicolons (fmap render xs)] RecUpdate _ e xs -> sep ["record" <+> render e, bracesAndSemicolons (fmap render xs)] +#if !MIN_VERSION_Agda(2,6,3) ETel [] -> "()" ETel tel -> fsep $ fmap render tel +#endif Quote _ -> "quote" QuoteTerm _ -> "quoteTerm" Unquote _ -> "unquote" @@ -447,6 +453,10 @@ UnquoteDef _ xs t -> fsep ["unquoteDef" <+> fsep (fmap render xs) <+> "=", render t] Pragma pr -> sep ["{-#" <+> render pr, "#-}"] +#if MIN_VERSION_Agda(2,6,3) + UnquoteData _ x xs e -> + fsep [ hsep [ "unquoteData", render x, fsep (fmap render xs), "=" ], render e ] +#endif where namedBlock s ds = fsep @@ -459,11 +469,11 @@ YesEta -> "eta-equality" NoEta () -> "no-eta-equality" -pRecordDirective :: +pRecordDirective :: RecordDirective -> Inlines pRecordDirective = \case - Induction ind -> render (rangedThing ind) + Induction ind -> render ind Constructor n inst -> hsep [ pInst, "constructor", render n ] where pInst = case inst of InstanceDef{} -> "instance" @@ -551,6 +561,10 @@ render (PolarityPragma _ q occs) = hsep ("POLARITY" : render q : fmap render occs) render (NoUniverseCheckPragma _) = "NO_UNIVERSE_CHECK" +#if MIN_VERSION_Agda(2,6,3) + render (NotProjectionLikePragma _ q) = + hsep [ "NOT_PROJECTION_LIKE", render q ] +#endif instance Render Fixity where render (Fixity _ Unrelated _) = __IMPOSSIBLE__ @@ -561,11 +575,20 @@ RightAssoc -> "infixr" NonAssoc -> "infix" +#if MIN_VERSION_Agda(2,6,3) +instance Render NotationPart where + render = \case + IdPart x -> text $ rangedThing x + HolePart{} -> "_" + VarPart {} -> "_" + WildPart{} -> "_" +#else instance Render GenPart where render (IdPart x) = text $ rangedThing x render BindHole {} = "_" render NormalHole {} = "_" render WildHole {} = "_" +#endif instance Render Fixity' where render (Fixity' fix nota _) diff --git a/src/Render/Interaction.hs b/src/Render/Interaction.hs --- a/src/Render/Interaction.hs +++ b/src/Render/Interaction.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE CPP #-} + module Render.Interaction where import qualified Data.Set as Set @@ -98,6 +100,10 @@ "Check lock" <+> render lk <+> "allows" <+> render t render (UsableAtMod modality t) = "Is usable at" <+> render modality <+> render t +#if MIN_VERSION_Agda(2,6,3) + render (DataSort _name expr) = + fsep [ "Sort", render expr, "allows data/record definitions" ] +#endif -- | IPBoundary' instance Render c => Render (IPBoundary' c) where diff --git a/src/Render/Internal.hs b/src/Render/Internal.hs --- a/src/Render/Internal.hs +++ b/src/Render/Internal.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} module Render.Internal where @@ -20,7 +21,12 @@ IdS -> "idS" EmptyS _ -> "emptyS" t :# rho -> mparens (p > 2) $ sep [pr 2 rho <> ",", renderPrec 3 t] - Strengthen _ rho -> mparens (p > 9) $ "strS" <+> pr 10 rho +#if MIN_VERSION_Agda(2,6,3) + Strengthen _ _ rho -> +#else + Strengthen _ rho -> +#endif + mparens (p > 9) $ "strS" <+> pr 10 rho Wk n rho -> mparens (p > 9) $ text ("wkS " ++ show n) <+> pr 10 rho Lift n rho -> mparens (p > 9) $ text ("liftS " ++ show n) <+> pr 10 rho @@ -154,6 +160,9 @@ MetaS x es -> renderPrec p $ MetaV x es DefS d es -> renderPrec p $ Def d es DummyS s -> parens $ text s +#if MIN_VERSION_Agda(2,6,3) + IntervalUniv -> "IntervalUniv" +#endif instance Render Type where renderPrec p (El _ a) = renderPrec p a @@ -200,3 +209,6 @@ render (UnblockOnAny us) = "any" <> parens (fsep $ punctuate "," $ map render $ Set.toList us) render (UnblockOnMeta m) = render m render (UnblockOnProblem pid) = "problem" <+> render pid +#if MIN_VERSION_Agda(2,6,3) + render (UnblockOnDef q) = "definition" <+> render q +#endif diff --git a/src/Render/Position.hs b/src/Render/Position.hs --- a/src/Render/Position.hs +++ b/src/Render/Position.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} module Render.Position where @@ -11,6 +12,11 @@ instance Render AbsolutePath where render = text . filePath +#if MIN_VERSION_Agda(2,6,3) +instance Render RangeFile where + render = render . rangeFilePath -- TODO rangeFileName ? +#endif + -------------------------------------------------------------------------------- instance Render a => Render (Position' (Strict.Maybe a)) where @@ -19,7 +25,7 @@ render f <> ":" <> render l <> "," <> render c instance Render PositionWithoutFile where - render p = render (p {srcFile = Strict.Nothing} :: Position) + render (Pn () _ l c) = render l <> "," <> render c instance Render IntervalWithoutFile where render (Interval s e) = start <> "-" <> end diff --git a/src/Render/RichText.hs b/src/Render/RichText.hs --- a/src/Render/RichText.hs +++ b/src/Render/RichText.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleInstances #-} @@ -56,13 +57,13 @@ -------------------------------------------------------------------------------- -- | Block elements -data Block +data Block -- for blocks like "Goal" & "Have" - = Labeled Inlines (Maybe String) (Maybe Agda.Range) String String + = Labeled Inlines (Maybe String) (Maybe Agda.Range) String String -- for ordinary goals & context | Unlabeled Inlines (Maybe String) (Maybe Agda.Range) -- headers - | Header String + | Header String deriving (Generic) instance ToJSON Block @@ -85,7 +86,7 @@ cons :: Inline -> Seq Inline -> Seq Inline cons (Text s c) (Text t d :<| xs) -- merge 2 adjacent Text if they have the same classnames - | c == d = Text (s <> t) c :<| xs + | c == d = Text (s <> t) c :<| xs | otherwise = Text s c :<| Text t d :<| xs cons (Text s c) (Horz [] :<| xs) = cons (Text s c) xs cons (Text s c) (Horz (Inlines t:ts) :<| xs) @@ -118,7 +119,7 @@ elemIsEmpty (Parn _) = False elemIsEmpty (PrHz _) = False -infixr 6 <+> +infixr 6 <+> (<+>) :: Inlines -> Inlines -> Inlines x <+> y @@ -168,7 +169,7 @@ Vert [Inlines] | -- | Parenthese Parn Inlines - | -- | Parenthese around a Horizontal, special case + | -- | Parenthese around a Horizontal, special case PrHz [Inlines] deriving (Generic) @@ -181,8 +182,8 @@ show (Hole i) = "?" ++ show i show (Horz xs) = unwords (map show $ toList xs) show (Vert xs) = unlines (map show $ toList xs) - show (Parn x) = "(" <> show x <> ")" - show (PrHz xs) = "(" <> unwords (map show $ toList xs) <> ")" + show (Parn x) = "(" <> show x <> ")" + show (PrHz xs) = "(" <> unwords (map show $ toList xs) <> ")" -------------------------------------------------------------------------------- @@ -202,6 +203,11 @@ instance ToJSON Agda.AbsolutePath where toJSON (Agda.AbsolutePath path) = toJSON path +#if MIN_VERSION_Agda(2,6,3) +instance ToJSON Agda.RangeFile where + toJSON (Agda.RangeFile path _maybeTopLevelModuleName) = toJSON path +#endif + -------------------------------------------------------------------------------- -- | Utilities / Combinators @@ -290,7 +296,7 @@ showIndex = map toSubscriptDigit . show -------------------------------------------------------------------------------- --- +-- -- | Picking the appropriate set of special characters depending on -- whether we are allowed to use unicode or have to limit ourselves -- to ascii. diff --git a/src/Render/TypeChecking.hs b/src/Render/TypeChecking.hs --- a/src/Render/TypeChecking.hs +++ b/src/Render/TypeChecking.hs @@ -4,12 +4,13 @@ import Agda.TypeChecking.Monad.Base import Agda.TypeChecking.Positivity.Occurrence import Render.Class +import Render.Common import Render.RichText instance Render NamedMeta where - render (NamedMeta "" (MetaId x)) = render x - render (NamedMeta "_" (MetaId x)) = render x - render (NamedMeta s (MetaId x)) = "_" <> text s <> render x + render (NamedMeta "" x) = render x + render (NamedMeta "_" x) = render x + render (NamedMeta s x) = "_" <> text s <> render x instance Render Occurrence where render = diff --git a/src/Server.hs b/src/Server.hs --- a/src/Server.hs +++ b/src/Server.hs @@ -9,9 +9,8 @@ import qualified Agda import Control.Concurrent ( writeChan ) -import Control.Monad.Reader ( MonadIO(liftIO) - , void - ) +import Control.Monad ( void ) +import Control.Monad.Reader ( MonadIO(liftIO) ) import Data.Aeson ( FromJSON , ToJSON ) diff --git a/src/Server/Handler.hs b/src/Server/Handler.hs --- a/src/Server/Handler.hs +++ b/src/Server/Handler.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE CPP #-} + module Server.Handler where import Agda ( getCommandLineOptions @@ -63,7 +65,7 @@ runCommandM program = do env <- ask runAgda $ do - -- get command line options + -- get command line options options <- getCommandLineOptions -- we need to set InteractionOutputCallback else it would panic @@ -86,7 +88,12 @@ let norm = AsIs -- localStateCommandM: restore TC state afterwards, do we need this here? typ <- localStateCommandM $ do - e <- lift $ runPM $ parse exprParser (unpack text) +#if MIN_VERSION_Agda(2,6,3) + (e, _attrs) +#else + e +#endif + <- lift $ runPM $ parse exprParser (unpack text) lift $ atTopLevel $ do concreteToAbstract_ e >>= typeInCurrent norm diff --git a/src/Switchboard.hs b/src/Switchboard.hs --- a/src/Switchboard.hs +++ b/src/Switchboard.hs @@ -3,6 +3,7 @@ import Monad import Control.Concurrent import qualified Server.ResponseController as ResponseController +import Control.Monad import Control.Monad.Reader import qualified Agda import qualified Data.Aeson as JSON @@ -12,7 +13,7 @@ import Data.IORef import Options (Config) -data Switchboard = Switchboard +data Switchboard = Switchboard { sbPrintLog :: ThreadId , sbSendResponse :: ThreadId , sbRunAgda :: ThreadId @@ -21,7 +22,7 @@ -- | All channels go in and out from here new :: Env -> IO Switchboard -new env = do +new env = do ctxEnvIORef <- newIORef Nothing Switchboard <$> forkIO (keepPrintingLog env) @@ -29,9 +30,9 @@ <*> forkIO (runReaderT Agda.start env) <*> pure ctxEnvIORef --- | For sending reactions to the client +-- | For sending reactions to the client setupLanguageContextEnv :: Switchboard -> LanguageContextEnv Config -> IO () -setupLanguageContextEnv switchboard ctxEnv = do +setupLanguageContextEnv switchboard ctxEnv = do writeIORef (sbLanguageContextEnv switchboard) (Just ctxEnv) destroy :: Switchboard -> IO () @@ -56,7 +57,7 @@ response <- readChan (envResponseChan env) result <- readIORef ctxEnvIORef - forM_ result $ \ctxEnv -> do + forM_ result $ \ctxEnv -> do runLspT ctxEnv $ do callback <- liftIO $ ResponseController.dispatch (envResponseController env) diff --git a/stack-8.10-Agda-2.6.2.2.yaml b/stack-8.10-Agda-2.6.2.2.yaml new file mode 100644 --- /dev/null +++ b/stack-8.10-Agda-2.6.2.2.yaml @@ -0,0 +1,21 @@ +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-language-server: + Agda-2-6-2-2: true + Agda: + # optimise-heavily: true + enable-cluster-counting: true diff --git a/stack-8.10.yaml b/stack-8.10.yaml deleted file mode 100644 --- a/stack-8.10.yaml +++ /dev/null @@ -1,19 +0,0 @@ -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-9.0-Agda-2.6.2.2.yaml b/stack-9.0-Agda-2.6.2.2.yaml new file mode 100644 --- /dev/null +++ b/stack-9.0-Agda-2.6.2.2.yaml @@ -0,0 +1,19 @@ +resolver: lts-19.33 +compiler: ghc-9.0.2 +# Allow a newer minor version of GHC than the snapshot specifies +compiler-check: newer-minor + +packages: +- . + +# Use some newer versions than in the lts-19.33 snapshot +extra-deps: +- text-icu-0.8.0.1 +# - Agda-2.6.2.2 # This is the lts-19.33 version of Agda + +flags: + agda-language-server: + Agda-2-6-2-2: true + Agda: + # optimise-heavily: true + enable-cluster-counting: true diff --git a/stack-9.0.yaml b/stack-9.0.yaml deleted file mode 100644 --- a/stack-9.0.yaml +++ /dev/null @@ -1,16 +0,0 @@ -resolver: lts-19.33 -compiler: ghc-9.0.2 -# Allow a newer minor version of GHC than the snapshot specifies -compiler-check: newer-minor - -packages: -- . - -# Use some newer versions than in the lts-19.33 snapshot -extra-deps: -- text-icu-0.8.0.1 - -flags: - Agda: - # optimise-heavily: true - enable-cluster-counting: true diff --git a/stack-9.2-Agda-2.6.2.2.yaml b/stack-9.2-Agda-2.6.2.2.yaml new file mode 100644 --- /dev/null +++ b/stack-9.2-Agda-2.6.2.2.yaml @@ -0,0 +1,17 @@ +resolver: lts-20.26 +compiler: ghc-9.2.8 +# Allow a newer minor version of GHC than the snapshot specifies +compiler-check: newer-minor + +packages: +- . + +extra-deps: +- Agda-2.6.2.2 + +flags: + agda-language-server: + Agda-2-6-2-2: true + Agda: + # optimise-heavily: true + enable-cluster-counting: true diff --git a/stack.yaml b/stack.yaml --- a/stack.yaml +++ b/stack.yaml @@ -6,6 +6,9 @@ packages: - . +extra-deps: +- Agda-2.6.3 + flags: Agda: # optimise-heavily: true