[ #4457 ] Added a separate benchmarking "phase" for compaction.

agda · Feb 20, 2020 · 24d7750 · 24d7750
1 parent 693bd11
commit 24d7750
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/src/full/Agda/Benchmarking.hs b/src/full/Agda/Benchmarking.hs
@@ -60,6 +60,8 @@ data Phase
     -- ^ Subphase for 'Termination'.
   | ModuleName
     -- ^ Subphase for 'Import'.
+  | Compaction
+    -- ^ Subphase for 'Deserialization': compacting interfaces.
   | BuildInterface
     -- ^ Subphase for 'Serialization'.
   | Sort

diff --git a/src/full/Agda/TypeChecking/Serialise.hs b/src/full/Agda/TypeChecking/Serialise.hs
@@ -193,7 +193,8 @@ decode s = do
         -- "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))
+        (Bench.billTo [Bench.Deserialization, Bench.Compaction] $
+           liftIO (Just . C.getCompact <$> C.compactWithSharing x))
 #endif
         (return (Just x))
     Left err -> do