[ #4457 ] Added the flag --compact-regions.

By default compact regions are not used.

The compact region code is now enabled starting from GHC 8.2.

Agda.cabal

@@ -253,7 +253,7 @@ library
   if impl(ghc < 8.4)
     build-depends: transformers == 0.5.2.0
 
-  if impl(ghc >= 8.6)
+  if impl(ghc >= 8.2)
     build-depends: ghc-compact == 0.1.*
 
   -- We don't write upper bounds for Alex nor Happy because the

CHANGELOG.md

@@ -80,6 +80,18 @@ Pragmas and options
 * Pragma `{-# ETA <record name> #-}` is no longer considered `--safe`.
   See [Issue [#4450](https://github.com/agda/agda/issues/4450)].
 
+* The new option `--compact-regions` tells Agda to use "compact
+  regions" to perhaps make garbage collection faster, at the cost of
+  some extra processing to create the compact regions
+  [Issue [#4457](https://github.com/agda/agda/issues/4457)].
+
+  This is an experimental feature. Perhaps the feature will be removed
+  in a future version of Agda, and perhaps it will be activated
+  unconditionally and the option removed.
+
+  Nothing happens if Agda was compiled using a version of GHC prior to
+  8.2.
+
 Language
 --------
 

doc/user-manual/tools/command-line-options.rst

@@ -49,6 +49,21 @@ General options
      Only scope-check the top-level module, do not type-check it (see
      :ref:`quickLaTeX`).
 
+.. option:: --compact-regions
+
+     .. versionadded:: 2.6.1
+
+     Use "compact regions" to perhaps make garbage collection faster,
+     at the cost of some extra processing to create the compact
+     regions.
+
+     This is an experimental feature. Perhaps the feature will be
+     removed in a future version of Agda, and perhaps it will be
+     activated unconditionally and the option removed.
+
+     Nothing happens if Agda was compiled using a version of GHC prior
+     to 8.2.
+
 .. option:: --version, -V
 
      Show version number.

src/full/Agda/Interaction/Options.hs

@@ -119,6 +119,8 @@ data CommandLineOptions = Options
   , optIgnoreInterfaces :: Bool
   , optIgnoreAllInterfaces :: Bool
   , optLocalInterfaces     :: Bool
+  , optCompactRegions      :: Bool
+    -- ^ Use compact regions?
   , optPragmaOptions    :: PragmaOptions
   , optOnlyScopeChecking :: Bool
     -- ^ Should the top-level module only be scope-checked, and not
@@ -239,6 +241,7 @@ defaultOptions = Options
   , optIgnoreInterfaces = False
   , optIgnoreAllInterfaces = False
   , optLocalInterfaces     = False
+  , optCompactRegions      = False
   , optPragmaOptions    = defaultPragmaOptions
   , optOnlyScopeChecking = False
   , optWithCompiler      = Nothing
@@ -536,6 +539,9 @@ ignoreAllInterfacesFlag o = return $ o { optIgnoreAllInterfaces = True }
 localInterfacesFlag :: Flag CommandLineOptions
 localInterfacesFlag o = return $ o { optLocalInterfaces = True }
 
+compactRegionsFlag :: Flag CommandLineOptions
+compactRegionsFlag o = return $ o { optCompactRegions = True }
+
 allowUnsolvedFlag :: Flag PragmaOptions
 allowUnsolvedFlag o = do
   let upd = over warningSet (Set.\\ unsolvedWarnings)
@@ -861,6 +867,8 @@ standardOptions =
                     "ignore interface files (re-type check everything)"
     , Option []     ["local-interfaces"] (NoArg localInterfacesFlag)
                     "put interface files next to the Agda files they correspond to"
+    , Option []     ["compact-regions"] (NoArg compactRegionsFlag)
+                    "use compact regions (if Agda was built with GHC 8.2 or newer)"
     , Option ['i']  ["include-path"] (ReqArg includeFlag "DIR")
                     "look for imports in DIR"
     , Option ['l']  ["library"] (ReqArg libraryFlag "LIB")

src/full/Agda/TypeChecking/Serialise.hs

@@ -46,10 +46,12 @@ import Data.Function
 
 import qualified Codec.Compression.GZip as G
 
-#if __GLASGOW_HASKELL__ >= 806
+#if __GLASGOW_HASKELL__ >= 802
 import GHC.Compact as C
 #endif
 
+import Agda.Interaction.Options
+
 import qualified Agda.TypeChecking.Monad.Benchmark as Bench
 
 import Agda.TypeChecking.Serialise.Base
@@ -61,6 +63,7 @@ import Agda.Utils.Hash
 import Agda.Utils.IORef
 
 import Agda.Utils.Except
+import Agda.Utils.Monad
 
 -- Note that the Binary instance for Int writes 64 bits, but throws
 -- away the 32 high bits when reading (at the time of writing, on
@@ -184,15 +187,15 @@ decode s = do
     Just mf -> stModuleToSource `setTCLens` mf
 
   case r of
-    Right x ->
-#if __GLASGOW_HASKELL__ < 806
-      return (Just x)
-#else
-      -- "Compact" the interfaces (without breaking sharing) to reduce
-      -- the amount of memory that is traversed by the garbage
-      -- collector.
-      liftIO (Just . C.getCompact <$> C.compactWithSharing x)
+    Right x -> do
+#if __GLASGOW_HASKELL__ >= 802
+      ifM (optCompactRegions <$> commandLineOptions)
+        -- "Compact" the interfaces (without breaking sharing) to
+        -- reduce the amount of memory that is traversed by the
+        -- garbage collector.
+        (liftIO (Just . C.getCompact <$> C.compactWithSharing x))
 #endif
+        (return (Just x))
     Left err -> do
       reportSLn "import.iface" 5 $ "Error when decoding interface file"
       -- Andreas, 2014-06-11 deactivated debug printing

test/Succeed/Issue4457.agda

@@ -0,0 +1,3 @@
+-- A test case for the --compact-regions flag. Nothing is imported, so
+-- no compaction actually takes place, it is just the flag that is
+-- tested.

test/Succeed/Issue4457.flags

@@ -0,0 +1 @@
+--compact-regions