diff --git a/CHANGELOG.md b/CHANGELOG.md index 539faf8..ed29086 100644 --- 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,6 +25,7 @@ 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 @@ -21,6 +33,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - 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 index a7fcbdc..aa1d527 100644 --- 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 index b97f1a9..1bd5d1f 100644 --- 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 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: banacorn@gmail.com -copyright: 2020 Author name here :) +maintainer: banacorn@gmail.com, 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 index 40b9c48..2013361 100644 --- 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: "banacorn@gmail.com" -copyright: "2020 Author name here :)" +maintainer: "banacorn@gmail.com, 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,18 +27,27 @@ description: Please see the README on GitHub at = 4.7 && < 5 @@ -45,7 +55,8 @@ dependencies: - aeson - bytestring - containers - - lsp < 1.7 + - lsp-types < 2 + - lsp < 2 - mtl - network - network-simple @@ -53,6 +64,7 @@ dependencies: - stm - text - process + - prettyprinter default-extensions: - LambdaCase diff --git a/src/Agda.hs b/src/Agda.hs index 375190c..994bc98 100644 --- 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 index dbbe688..152569a 100644 --- a/src/Agda/Convert.hs +++ b/src/Agda/Convert.hs @@ -9,6 +9,7 @@ import qualified Agda.IR as IR import Agda.Interaction.Base import Agda.Interaction.BasicOps as B import Agda.Interaction.EmacsCommand (Lisp) +import Agda.Interaction.EmacsTop (showInfoError) import Agda.Interaction.Highlighting.Common (chooseHighlightingMethod, toAtoms) import Agda.Interaction.Highlighting.Precise (Aspects (..), DefinitionSite (..), HighlightingInfo, TokenBased (..)) import qualified Agda.Interaction.Highlighting.Range as Highlighting @@ -22,6 +23,9 @@ import Agda.Syntax.Internal (alwaysUnblock) import Agda.Syntax.Position (HasRange (getRange), Range, noRange) import Agda.Syntax.Scope.Base import Agda.TypeChecking.Errors (getAllWarningsOfTCErr, prettyError) +#if MIN_VERSION_Agda(2,6,3) +import Agda.TypeChecking.Errors (explainWhyInScope) +#endif import Agda.TypeChecking.Monad hiding (Function) import Agda.TypeChecking.Monad.MetaVars (withInteractionId) import Agda.TypeChecking.Pretty (prettyTCM) @@ -34,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) @@ -259,8 +269,8 @@ fromDisplayInfo = \case <+> 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 + Info_WhyInScope why -> do + doc <- explainWhyInScope why #else Info_WhyInScope s cwd v xs ms -> do doc <- explainWhyInScope s cwd v xs ms @@ -302,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"] @@ -348,38 +363,7 @@ lispifyGoalSpecificDisplayInfo ii kind = localTCState $ -------------------------------------------------------------------------------- --- | Serializing Info_Error -showInfoError :: Info_Error -> TCM String -showInfoError (Info_GenericError err) = do - e <- prettyError err - w <- prettyTCWarnings' =<< getAllWarningsOfTCErr err - - let errorMsg = - if null w - then e - else delimiter "Error" ++ "\n" ++ e - let warningMsg = - List.intercalate "\n" $ - delimiter "Warning(s)" : - filter (not . null) w - return $ - if null w - then errorMsg - else errorMsg ++ "\n\n" ++ warningMsg -showInfoError (Info_CompilationError warnings) = do - s <- prettyTCWarnings warnings - return $ - unlines - [ "You need to fix the following errors before you can compile", - "the module:", - "", - s - ] -showInfoError (Info_HighlightingParseError ii) = - return $ "Highlighting failed to parse expression in " ++ show ii -showInfoError (Info_HighlightingScopeCheckError ii) = - return $ "Highlighting failed to scope check expression in " ++ show ii - +#if !MIN_VERSION_Agda(2,6,3) explainWhyInScope :: String -> FilePath -> @@ -462,6 +446,7 @@ explainWhyInScope s _ v xs ms = TCP.<+> "at" TCP.<+> TCP.prettyTCM (getRange m) TCP.$$ pWhy r w +#endif -- | Pretty-prints the context of the given meta-variable. prettyResponseContexts :: @@ -482,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 @@ -531,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 diff --git a/src/Render/Class.hs b/src/Render/Class.hs index c18e37c..201fe04 100644 --- a/src/Render/Class.hs +++ b/src/Render/Class.hs @@ -1,5 +1,8 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeSynonymInstances #-} + module Render.Class ( Render (..), -- RenderTCM (..), @@ -15,8 +18,13 @@ import qualified Agda.Syntax.Translation.AbstractToConcrete as A import qualified Agda.TypeChecking.Monad.Base as A import Agda.Utils.List1 (List1) import Agda.Utils.List2 (List2) +#if MIN_VERSION_Agda(2,6,4) +import Agda.Syntax.Common.Pretty (Doc) +import qualified Agda.Syntax.Common.Pretty as Doc +#else import Agda.Utils.Pretty (Doc) import qualified Agda.Utils.Pretty as Doc +#endif import Data.Int (Int32) import GHC.Exts ( IsList(toList) ) @@ -46,7 +54,7 @@ renderP = pure . text . Doc.render . Doc.pretty -- | like 'prettyA' renderA :: (Render c, A.ToConcrete a, A.ConOfAbs a ~ c) => a -> A.TCM Inlines -renderA x = render <$> A.abstractToConcrete_ x +renderA x = render <$> A.abstractToConcrete_ x -- | like 'prettyATop' renderATop :: (Render c, A.ToConcrete a, A.ConOfAbs a ~ c) => a -> A.TCM Inlines @@ -76,4 +84,4 @@ instance Render a => Render (List1 a) where render = render . toList instance Render a => Render (List2 a) where - render = render . toList \ No newline at end of file + render = render . toList diff --git a/src/Render/Concrete.hs b/src/Render/Concrete.hs index 61ab0a3..0d84a3d 100644 --- a/src/Render/Concrete.hs +++ b/src/Render/Concrete.hs @@ -125,6 +125,10 @@ instance Render Expr where Equal _ a b -> render a <+> "=" <+> render b Ellipsis _ -> "..." Generalized e -> render e +#if MIN_VERSION_Agda(2,6,4) + KnownIdent _ q -> render q + KnownOpApp _ _ q _ es -> fsep $ renderOpApp q es +#endif where absurd NotHidden = "()" absurd Instance {} = "{{}}" @@ -254,11 +258,19 @@ instance Render RHS where instance Render WhereClause where render NoWhere = mempty +#if MIN_VERSION_Agda(2,6,4) + render (AnyWhere _range [Module _ _ x [] ds]) +#else render (AnyWhere _range [Module _ x [] ds]) +#endif | isNoName (unqualify x) = vcat ["where", vcat $ fmap render ds] render (AnyWhere _range ds) = vcat ["where", vcat $ fmap render ds] +#if MIN_VERSION_Agda(2,6,4) + render (SomeWhere _range _er m a ds) = +#else render (SomeWhere _range m a ds) = +#endif vcat [ hsep $ applyWhen @@ -346,7 +358,11 @@ instance Render Declaration where render rhs, render wh ] +#if MIN_VERSION_Agda(2,6,4) + DataSig _ _er x tel e -> +#else DataSig _ x tel e -> +#endif fsep [ hsep [ "data", @@ -358,7 +374,11 @@ instance Render Declaration where render e ] ] +#if MIN_VERSION_Agda(2,6,4) + Data _ _er x tel e cs -> +#else Data _ x tel e cs -> +#endif fsep [ hsep [ "data", @@ -382,7 +402,11 @@ instance Render Declaration where "where", vcat $ fmap render cs ] +#if MIN_VERSION_Agda(2,6,4) + RecordSig _ _er x tel e -> +#else RecordSig _ x tel e -> +#endif sep [ hsep [ "record", @@ -394,7 +418,11 @@ instance Render Declaration where render e ] ] +#if MIN_VERSION_Agda(2,6,4) + Record _ _er x dir tel e cs -> +#else Record _ x dir tel e cs -> +#endif pRecord x dir tel (Just e) cs RecordDef _ x dir tel cs -> pRecord x dir tel Nothing cs @@ -415,7 +443,11 @@ instance Render Declaration where Postulate _ ds -> namedBlock "postulate" ds Primitive _ ds -> namedBlock "primitive" ds Generalize _ ds -> namedBlock "variable" ds +#if MIN_VERSION_Agda(2,6,4) + Module _ _er x tel ds -> +#else Module _ x tel ds -> +#endif fsep [ hsep [ "module", @@ -425,19 +457,23 @@ instance Render Declaration where ], vcat $ fmap render ds ] - ModuleMacro _ x (SectionApp _ [] e) DoOpen i - | isNoName x -> +#if MIN_VERSION_Agda(2,6,4) + ModuleMacro _ _er x m open i -> case m of +#else + ModuleMacro _ x m open i -> case m of +#endif + (SectionApp _ [] e) | open == DoOpen, isNoName x -> fsep - [ render DoOpen, + [ render open, render e, render i ] - ModuleMacro _ x (SectionApp _ tel e) open i -> + (SectionApp _ tel e) -> fsep [ render open <+> "module" <+> render x <+> fcat (fmap render tel), "=" <+> render e <+> render i ] - ModuleMacro _ x (RecordModuleInstance _ rec) open _ -> + (RecordModuleInstance _ rec) -> fsep [ render open <+> "module" <+> render x, "=" <+> render rec <+> "{{...}}" @@ -456,6 +492,12 @@ instance Render Declaration where #if MIN_VERSION_Agda(2,6,3) UnquoteData _ x xs e -> fsep [ hsep [ "unquoteData", render x, fsep (fmap render xs), "=" ], render e ] +#endif +#if MIN_VERSION_Agda(2,6,4) + Opaque _ ds -> + namedBlock "opaque" ds + Unfolding _ xs -> + fsep ("unfolding" : fmap render xs) #endif where namedBlock s ds = @@ -614,7 +656,11 @@ instance Render e => Render (Named NamedName e) where instance Render Pattern where render = \case +#if MIN_VERSION_Agda(2,6,4) + IdentP _ x -> render x +#else IdentP x -> render x +#endif AppP p1 p2 -> fsep [render p1, render p2] RawAppP _ ps -> fsep $ fmap render (List2.toList ps) OpAppP _ q _ ps -> fsep $ renderOpApp q (fmap (fmap (fmap (NoPlaceholder Strict.Nothing))) ps) diff --git a/src/Render/Interaction.hs b/src/Render/Interaction.hs index 4cc6a60..b35958e 100644 --- a/src/Render/Interaction.hs +++ b/src/Render/Interaction.hs @@ -2,6 +2,8 @@ module Render.Interaction where +import qualified Data.IntMap as IntMap +import qualified Data.Map as Map import qualified Data.Set as Set import Agda.Interaction.Base @@ -107,9 +109,26 @@ instance (Render a, Render b) => Render (OutputConstraint a b) where -- | IPBoundary' instance Render c => Render (IPBoundary' c) where +#if MIN_VERSION_Agda(2,6,4) + render (IPBoundary m) = vcat $ flip fmap (Map.toList m) $ \case + (boundary, rhs) -> + fsep (punctuate "," xs) <+> "⊢" <+> render rhs + where + xs = flip fmap (IntMap.toList boundary) $ \(l, r) -> + text $ concat [ "@", show l, " = ", if r then "i1" else "i0" ] +#else render (IPBoundary eqs val meta over) = do let xs = fmap (\(l, r) -> render l <+> "=" <+> render r) eqs rhs = case over of Overapplied -> "=" <+> render meta NotOverapplied -> mempty fsep (punctuate "," xs) <+> "⊢" <+> render val <+> rhs +#endif + +#if MIN_VERSION_Agda(2,6,4) +instance Render c => Render (IPFace' c) where + render (IPFace' eqs val) = do + let + xs = map (\ (l,r) -> render l <+> "=" <+> render r) eqs + fsep (punctuate "," xs) <+> "⊢" <+> render val +#endif diff --git a/src/Render/Internal.hs b/src/Render/Internal.hs index e64552a..8caf8ca 100644 --- a/src/Render/Internal.hs +++ b/src/Render/Internal.hs @@ -3,14 +3,18 @@ module Render.Internal where +import Control.Monad +import qualified Data.List as List +import qualified Data.Set as Set + import Agda.Syntax.Common (Hiding (..), LensHiding (getHiding), Named (namedThing)) import Agda.Syntax.Internal hiding (telToList) -import qualified Data.List as List +import Agda.Utils.Function (applyWhen) + import Render.Class import Render.Common (renderHiding) import Render.Concrete () import Render.RichText -import qualified Data.Set as Set -------------------------------------------------------------------------------- @@ -129,8 +133,13 @@ instance Render PlusLevel where -- UnreducedLevel v -> renderPrec p v instance Render Sort where - renderPrec p srt = - case srt of + renderPrec p = \case +#if MIN_VERSION_Agda(2,6,4) + Univ u (ClosedLevel n) -> text $ suffix n $ showUniv u + Univ u l -> mparens (p > 9) $ text (showUniv u) <+> renderPrec 10 l + Inf u n -> text $ suffix n $ showUniv u ++ "ω" + LevelUniv -> "LevelUniv" +#else Type (ClosedLevel 0) -> "Set" Type (ClosedLevel n) -> text $ "Set" ++ show n Type l -> mparens (p > 9) $ "Set" <+> renderPrec 10 l @@ -142,6 +151,7 @@ instance Render Sort where Inf IsFibrant n -> text $ "Setω" ++ show n Inf IsStrict n -> text $ "SSetω" ++ show n SSet l -> mparens (p > 9) $ "SSet" <+> renderPrec 10 l +#endif SizeUniv -> "SizeUniv" LockUniv -> "LockUniv" PiSort a _s1 s2 -> @@ -163,6 +173,10 @@ instance Render Sort where #if MIN_VERSION_Agda(2,6,3) IntervalUniv -> "IntervalUniv" #endif +#if MIN_VERSION_Agda(2,6,4) + where + suffix n = applyWhen (n /= 0) (++ show n) +#endif instance Render Type where renderPrec p (El _ a) = renderPrec p a diff --git a/src/Render/Utils.hs b/src/Render/Utils.hs index 39bd700..52246df 100644 --- a/src/Render/Utils.hs +++ b/src/Render/Utils.hs @@ -1,11 +1,16 @@ +{-# LANGUAGE CPP #-} + module Render.Utils where import Agda.Utils.Time ( CPUTime ) +#if MIN_VERSION_Agda(2,6,4) +import Agda.Syntax.Common.Pretty (pretty) +#else import Agda.Utils.Pretty (pretty) +#endif import Render.Class import Render.RichText - instance Render CPUTime where render = text . show . pretty diff --git a/src/Server.hs b/src/Server.hs index f4fccdb..2de1a5a 100644 --- a/src/Server.hs +++ b/src/Server.hs @@ -1,37 +1,37 @@ {-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveGeneric #-} -- entry point of the LSP server module Server - ( run - ) where + ( run, + ) +where import qualified Agda -import Control.Concurrent ( writeChan ) -import Control.Monad ( void ) -import Control.Monad.Reader ( MonadIO(liftIO) ) -import Data.Aeson ( FromJSON - , ToJSON - ) -import qualified Data.Aeson as JSON -import Data.Text ( pack ) -import GHC.IO.IOMode ( IOMode(ReadWriteMode) ) -import Language.LSP.Server hiding ( Options ) -import Language.LSP.Types hiding ( Options(..) - , TextDocumentSyncClientCapabilities(..) - ) -import Monad -import qualified Network.Simple.TCP as TCP -import Network.Socket ( socketToHandle ) +import Control.Concurrent (writeChan) +import Control.Monad (void) +import Control.Monad.Reader (MonadIO (liftIO)) +import Data.Aeson + ( FromJSON, + ToJSON, + ) +import qualified Data.Aeson as JSON +import Data.Text (pack) +import qualified Data.Text as T +import GHC.IO.IOMode (IOMode (ReadWriteMode)) +import Language.LSP.Server hiding (Options) +import qualified Language.LSP.Server as LSP +import Language.LSP.Types hiding + ( Options (..), + TextDocumentSyncClientCapabilities (..), + ) +import Monad +import qualified Network.Simple.TCP as TCP +import Network.Socket (socketToHandle) +import Options +import qualified Server.Handler as Handler +import Switchboard (Switchboard) import qualified Switchboard -import Switchboard ( Switchboard ) - -import qualified Server.Handler as Handler - -import qualified Language.LSP.Server as LSP -import Options - -------------------------------------------------------------------------------- @@ -39,76 +39,83 @@ run :: Options -> IO Int run options = do case optViaTCP options of Just port -> do - void - $ TCP.serve (TCP.Host "127.0.0.1") (show port) - $ \(sock, _remoteAddr) -> do + void $ + TCP.serve (TCP.Host "127.0.0.1") (show port) $ + \(sock, _remoteAddr) -> do -- writeChan (envLogChan env) "[Server] connection established" handle <- socketToHandle sock ReadWriteMode - _ <- runServerWithHandles + _ <- runServerWithHandles #if MIN_VERSION_lsp(1,5,0) - mempty mempty + mempty mempty #endif - handle handle (serverDefn options) + handle handle (serverDefn options) return () -- Switchboard.destroy switchboard return 0 Nothing -> do runServer (serverDefn options) - where - serverDefn :: Options -> ServerDefinition Config - serverDefn options = ServerDefinition - { defaultConfig = initConfig - , onConfigurationChange = \old newRaw -> case JSON.fromJSON newRaw of - JSON.Error s -> Left $ pack $ "Cannot parse server configuration: " <> s - JSON.Success new -> Right new - , doInitialize = \ctxEnv _req -> do - env <- runLspT ctxEnv (createInitEnv options) - switchboard <- Switchboard.new env - Switchboard.setupLanguageContextEnv switchboard ctxEnv - pure $ Right (ctxEnv, env) - , staticHandlers = handlers - , interpretHandler = \(ctxEnv, env) -> - Iso (runLspT ctxEnv . runServerM env) liftIO - , options = lspOptions - } + where + serverDefn :: Options -> ServerDefinition Config + serverDefn options = + ServerDefinition + { defaultConfig = initConfig, + onConfigurationChange = \old newRaw -> case JSON.fromJSON newRaw of + JSON.Error s -> Left $ pack $ "Cannot parse server configuration: " <> s + JSON.Success new -> Right new, + doInitialize = \ctxEnv _req -> do + env <- runLspT ctxEnv (createInitEnv options) + switchboard <- Switchboard.new env + Switchboard.setupLanguageContextEnv switchboard ctxEnv + pure $ Right (ctxEnv, env), + staticHandlers = handlers, + interpretHandler = \(ctxEnv, env) -> + Iso (runLspT ctxEnv . runServerM env) liftIO, + options = lspOptions + } - lspOptions :: LSP.Options - lspOptions = defaultOptions { textDocumentSync = Just syncOptions } + lspOptions :: LSP.Options + lspOptions = defaultOptions {textDocumentSync = Just syncOptions} - -- these `TextDocumentSyncOptions` are essential for receiving notifications from the client - syncOptions :: TextDocumentSyncOptions - syncOptions = TextDocumentSyncOptions { _openClose = Just True -- receive open and close notifications from the client - , _change = Just changeOptions -- receive change notifications from the client - , _willSave = Just False -- receive willSave notifications from the client - , _willSaveWaitUntil = Just False -- receive willSave notifications from the client - , _save = Just $ InR saveOptions - } + -- these `TextDocumentSyncOptions` are essential for receiving notifications from the client + syncOptions :: TextDocumentSyncOptions + syncOptions = + TextDocumentSyncOptions + { _openClose = Just True, -- receive open and close notifications from the client + _change = Just changeOptions, -- receive change notifications from the client + _willSave = Just False, -- receive willSave notifications from the client + _willSaveWaitUntil = Just False, -- receive willSave notifications from the client + _save = Just $ InR saveOptions + } - changeOptions :: TextDocumentSyncKind - changeOptions = TdSyncIncremental + changeOptions :: TextDocumentSyncKind + changeOptions = TdSyncIncremental - -- includes the document content on save, so that we don't have to read it from the disk - saveOptions :: SaveOptions - saveOptions = SaveOptions (Just True) + -- includes the document content on save, so that we don't have to read it from the disk + saveOptions :: SaveOptions + saveOptions = SaveOptions (Just True) -- handlers of the LSP server handlers :: Handlers (ServerM (LspM Config)) -handlers = mconcat - [ -- custom methods, not part of LSP - requestHandler (SCustomMethod "agda") $ \req responder -> do - let RequestMessage _ _i _ params = req - response <- Agda.sendCommand params - responder $ Right response - , - -- hover provider - requestHandler STextDocumentHover $ \req responder -> do - let - RequestMessage _ _ _ (HoverParams (TextDocumentIdentifier uri) pos _workDone) - = req - result <- Handler.onHover uri pos - responder $ Right result - -- -- syntax highlighting - -- , requestHandler STextDocumentSemanticTokensFull $ \req responder -> do - -- result <- Handler.onHighlight (req ^. (params . textDocument . uri)) - -- responder result - ] +handlers = + mconcat + [ -- custom methods, not part of LSP + requestHandler (SCustomMethod "agda") $ \req responder -> do + let RequestMessage _ _i _ params = req + response <- Agda.sendCommand params + responder $ Right response, + -- hover provider + requestHandler STextDocumentHover $ \req responder -> do + let RequestMessage _ _ _ (HoverParams (TextDocumentIdentifier uri) pos _workDone) = + req + result <- Handler.onHover uri pos + responder $ Right result, + notificationHandler SInitialized $ \_not -> pure (), + notificationHandler STextDocumentDidOpen $ \_not -> pure (), + notificationHandler STextDocumentDidSave $ \_not -> pure (), + notificationHandler STextDocumentDidChange $ \_not -> pure (), + notificationHandler SCancelRequest $ \_not -> pure () + -- -- syntax highlighting + -- , requestHandler STextD_cumentSemanticTokensFull $ \req responder -> do + -- result <- Handler.onHighlight (req ^. (params . textDocument . uri)) + -- responder result + ] diff --git a/src/Server/Handler.hs b/src/Server/Handler.hs index 5e02ffd..f47fe1d 100644 --- a/src/Server/Handler.hs +++ b/src/Server/Handler.hs @@ -40,7 +40,11 @@ import Agda.TypeChecking.Monad ( HasOptions(commandLineOptions) , setInteractionOutputCallback ) import Agda.TypeChecking.Warnings ( runPM ) +#if MIN_VERSION_Agda(2,6,4) +import Agda.Syntax.Common.Pretty ( render ) +#else import Agda.Utils.Pretty ( render ) +#endif import Control.Concurrent.STM import Control.Monad.Reader import Control.Monad.State diff --git a/stack-9.2-Agda-2.6.3.yaml b/stack-9.2-Agda-2.6.3.yaml new file mode 100644 index 0000000..c05d880 --- /dev/null +++ b/stack-9.2-Agda-2.6.3.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.3 + +flags: + agda-language-server: + Agda-2-6-3: true + Agda: + # optimise-heavily: true + enable-cluster-counting: true diff --git a/stack.yaml b/stack.yaml index cd6a33c..13c504f 100644 --- a/stack.yaml +++ b/stack.yaml @@ -7,7 +7,7 @@ packages: - . extra-deps: -- Agda-2.6.3 +- Agda-2.6.4 flags: Agda: diff --git a/stack.yaml.lock b/stack.yaml.lock index 7933463..cbf613a 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -5,12 +5,12 @@ packages: - completed: - hackage: Agda-2.6.3@sha256:a668ab56534bd548c682088f595939a6b8732b46b84d7e7d808af966b5d5d4ec,36760 + hackage: Agda-2.6.4@sha256:298bc3b261ad034bf4ee788834a4d296aa5c2f6ea17ac4bef44e3daea53a7cd8,28443 pantry-tree: - sha256: 3c60f373128b663640a90fbc6fcffcb9a5edd57e8dfc4a7b00d2f7771f9210ac - size: 41559 + sha256: 6c811b2ff8aa666ba301666e87d9234993d841dd370d47f8398379cd943e47bb + size: 42645 original: - hackage: Agda-2.6.3 + hackage: Agda-2.6.4 snapshots: - completed: sha256: 5a59b2a405b3aba3c00188453be172b85893cab8ebc352b1ef58b0eae5d248a2