[ fix agda#3118 ] Add flags: field to .agda-lib file format

src/full/Agda/Interaction/Imports.hs

@@ -98,7 +98,9 @@ sourceInfo (SourceFile f) = Bench.billTo [Bench.Parsing] $ do
                            parseFile moduleParser f $ TL.unpack source
   moduleName            <- moduleName f parsedMod
   let sourceDir = takeDirectory $ filePath f
-  libs <- libToTCM $ getAgdaLibFiles sourceDir
+  useLibs <- optUseLibs <$> commandLineOptions
+  libs <- if | useLibs   -> libToTCM $ getAgdaLibFiles sourceDir
+             | otherwise -> return []
   return SourceInfo
     { siSource     = source
     , siFileType   = fileType
@@ -107,6 +109,13 @@ sourceInfo (SourceFile f) = Bench.billTo [Bench.Parsing] $ do
     , siProjectLibs = libs
     }
 
+sourcePragmas :: SourceInfo -> TCM [OptionsPragma]
+sourcePragmas SourceInfo{..} = do
+  let defaultPragmas = map _libPragmas siProjectLibs
+  let cpragmas = C.modPragmas siModule
+  pragmas <- concreteOptionsToOptionPragmas cpragmas
+  return $ defaultPragmas ++ pragmas
+
 -- | Is the aim to type-check the top-level module, or only to
 -- scope-check it?
 
@@ -397,12 +406,12 @@ getInterface' x isMain msi =
              (unless (includeStateChanges isMain) . (stPragmaOptions `setTCLens`)) $ do
      -- We remember but reset the pragma options locally
      -- For the main interface, we also remember the pragmas from the file
-     let mpragmas = C.modPragmas . siModule <$> msi
      -- Issue #3644 (Abel 2020-05-08): Set approximate range for errors in options
-     currentOptions <- setCurrentRange mpragmas $ do
+     currentOptions <- setCurrentRange (C.modPragmas . siModule <$> msi) $ do
        when (includeStateChanges isMain) $ do
-         let pragmas = fromMaybe __IMPOSSIBLE__ mpragmas
-         mapM_ setOptionsFromPragma =<< concreteOptionsToOptionPragmas pragmas
+         let si = fromMaybe __IMPOSSIBLE__ msi
+         pragmas <- sourcePragmas si
+         mapM_ setOptionsFromPragma pragmas
        currentOptions <- useTC stPragmaOptions
        -- Now reset the options
        setCommandLineOptions . stPersistentOptions . stPersistentState =<< getTC
@@ -870,20 +879,20 @@ createInterface file mname isMain msi =
       reportSLn "import.iface.create" 10 $
         "  visited: " ++ List.intercalate ", " (map prettyShow visited)
 
-    (source, fileType, C.Mod pragmas top) <- do
-      si <- case msi of
-        Nothing -> sourceInfo file
-        Just si -> return si
-      case si of
-        SourceInfo {..} -> return (siSource, siFileType, siModule)
+    si <- case msi of
+      Nothing -> sourceInfo file
+      Just si -> return si
+    let source   = siSource si
+        fileType = siFileType si
+        top      = C.modDecls $ siModule si
 
     modFile       <- useTC stModuleToSource
     fileTokenInfo <- Bench.billTo [Bench.Highlighting] $
                        generateTokenInfoFromSource
                          (srcFilePath file) (TL.unpack source)
     stTokens `setTCLens` fileTokenInfo
 
-    options <- concreteOptionsToOptionPragmas pragmas
+    options <- sourcePragmas si
     mapM_ setOptionsFromPragma options
 
     verboseS "import.iface.create" 15 $ do

src/full/Agda/Interaction/Library/Base.hs

@@ -54,6 +54,7 @@ data AgdaLibFile = AgdaLibFile
   , _libFile     :: FilePath    -- ^ Path to this @.agda-lib@ file (not content of the file).
   , _libIncludes :: [FilePath]  -- ^ Roots where to look for the modules of the library.
   , _libDepends  :: [LibName]   -- ^ Dependencies.
+  , _libPragmas  :: [String]    -- ^ Default pragma options for all files in the library.
   }
   deriving (Show)
 
@@ -63,6 +64,7 @@ emptyLibFile = AgdaLibFile
   , _libFile     = ""
   , _libIncludes = []
   , _libDepends  = []
+  , _libPragmas  = []
   }
 
 -- | Lenses for AgdaLibFile
@@ -79,6 +81,9 @@ libIncludes f a = f (_libIncludes a) <&> \ x -> a { _libIncludes = x }
 libDepends :: Lens' [LibName] AgdaLibFile
 libDepends f a = f (_libDepends a) <&> \ x -> a { _libDepends = x }
 
+libPragmas :: Lens' [String] AgdaLibFile
+libPragmas f a = f (_libPragmas a) <&> \ x -> a { _libPragmas = x }
+
 
 ------------------------------------------------------------------------
 -- * Library warnings and errors

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

@@ -83,6 +83,7 @@ agdaLibFields =
   [ optionalField "name"    parseName                      libName
   , optionalField "include" (pure . concatMap parsePaths)  libIncludes
   , optionalField "depend"  (pure . concatMap splitCommas) libDepends
+  , optionalField "flags"   (pure . concatMap parseFlags)  libPragmas
   ]
   where
     parseName :: [String] -> P LibName
@@ -98,6 +99,9 @@ agdaLibFields =
       go acc (       ' '  :cs) = fixup acc ++ go id cs
       go acc (c           :cs) = go (acc . (c:)) cs
 
+    parseFlags :: String -> [String]
+    parseFlags = words
+
 -- | Parse @.agda-lib@ file.
 --
 -- Sets 'libFile' name and turn mentioned include directories into absolute