Now works cross Agda version

Author: nvarner

src/Agda/Interaction/Library/Parse/More.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE RecordWildCards #-}
@@ -82,12 +83,20 @@ agdaLibFields =
   -- Andreas, 2017-08-23, issue #2708, field "name" is optional.
   [ optionalField "name" (\_ -> parseName) libName,
     optionalField "include" (\_ -> pure . concatMap parsePaths) libIncludes,
+#if MIN_VERSION_Agda(2,8,0)
     optionalField "depend" (\_ -> pure . map parseLibName . concatMap splitCommas) libDepends,
+#else
+    optionalField "depend" (\_ -> pure . concatMap splitCommas) libDepends,
+#endif
     optionalField "flags" (\r -> pure . foldMap (parseFlags r)) libPragmas
   ]
   where
     parseName :: [String] -> P LibName
+#if MIN_VERSION_Agda(2,8,0)
     parseName [s] | [name] <- words s = pure $ parseLibName name
+#else
+    parseName [s] | [name] <- words s = pure name
+#endif
     parseName ls = throwError $ BadLibraryName $ unwords ls
 
     parsePaths :: String -> [FilePath]

src/Server/Filesystem.hs

@@ -28,9 +28,9 @@ import Agda.Utils.IO (catchIO)
 import Agda.Utils.IO.UTF8 (ReadException, readTextFile)
 import Agda.Utils.List (nubM)
 import Agda.Utils.Maybe (fromMaybe, maybe)
-import Agda.Utils.Monad (foldM, forM)
 import Control.Exception (try, tryJust)
 import qualified Control.Exception as E
+import Control.Monad (foldM, forM)
 import Control.Monad.IO.Class (MonadIO (liftIO))
 import qualified Data.Strict as Strict
 import Data.Text (Text)

src/Server/Model/AgdaLib.hs

@@ -39,7 +39,7 @@ import Agda.Syntax.Common.Pretty (Pretty, pretty, vcat, prettyAssign, text, psho
 import qualified Text.URI as ParsedUri
 import qualified Data.Text as Text
 import qualified Server.Filesystem as FS
-import Agda.Utils.Monad (forM)
+import Control.Monad (forM)
 
 data AgdaLibOrigin = FromFile !FS.FileId | Defaulted
   deriving (Show, Eq)

test/Test/AgdaLibResolution.hs

@@ -1,6 +1,10 @@
+{-# LANGUAGE CPP #-}
+
 module Test.AgdaLibResolution (tests) where
 
+#if MIN_VERSION_Agda(2,8,0)
 import Agda.Interaction.Library (parseLibName)
+#endif
 import Agda.Syntax.Common.Pretty (prettyShow)
 import Agda.Utils.Lens ((^.))
 import Control.Monad.IO.Class (liftIO)
@@ -49,7 +53,11 @@ tests =
           runServerT env $ do
             lib <- findAgdaLib absConstPath
 
+#if MIN_VERSION_Agda(2,8,0)
             liftIO $ lib ^. agdaLibName @?= parseLibName "no-deps"
+#else
+            liftIO $ lib ^. agdaLibName @?= "no-deps"
+#endif
             liftIO $ lib ^. agdaLibOrigin @?= FromFile (FS.LocalFilePath absAgdaLibPath)
             liftIO $ lib ^. agdaLibIncludes @?= [FS.LocalFilePath absSrcPath]
     ]