diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 7c48ea8334..74549680bb 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -103,6 +103,10 @@ def CompactedRegion := USize
 @[extern "lean_compacted_region_is_memory_mapped"]
 opaque CompactedRegion.isMemoryMapped : CompactedRegion → Bool
 
+/-- Size in bytes. -/
+@[extern "lean_compacted_region_size"]
+opaque CompactedRegion.size : CompactedRegion → USize
+
 /-- Free a compacted region and its contents. No live references to the contents may exist at the time of invocation. -/
 @[extern "lean_compacted_region_free"]
 unsafe opaque CompactedRegion.free : CompactedRegion → IO Unit
@@ -2178,6 +2182,7 @@ def displayStats (env : Environment) : IO Unit := do
   IO.println ("direct imports:                        " ++ toString env.header.imports);
   IO.println ("number of imported modules:            " ++ toString env.header.regions.size);
   IO.println ("number of memory-mapped modules:       " ++ toString (env.header.regions.filter (·.isMemoryMapped) |>.size));
+  IO.println ("number of imported bytes:              " ++ toString (env.header.regions.map (·.size) |>.sum));
   IO.println ("number of imported consts:             " ++ toString env.constants.map₁.size);
   IO.println ("number of buckets for imported consts: " ++ toString env.constants.numBuckets);
   IO.println ("trust level:                           " ++ toString env.header.trustLevel);
diff --git a/src/runtime/compact.cpp b/src/runtime/compact.cpp
index 786eca5d06..faf3965ecb 100644
--- a/src/runtime/compact.cpp
+++ b/src/runtime/compact.cpp
@@ -379,6 +379,7 @@ void object_compactor::operator()(object * o) {
 }
 
 compacted_region::compacted_region(size_t sz, void * data, void * base_addr, bool is_mmap, std::function<void()> free_data):
+    m_size(sz),
     m_base_addr(base_addr),
     m_is_mmap(is_mmap),
     m_free_data(free_data),
@@ -502,6 +503,10 @@ extern "C" LEAN_EXPORT uint8 lean_compacted_region_is_memory_mapped(usize region
     return reinterpret_cast<compacted_region *>(region)->is_memory_mapped();
 }
 
+extern "C" LEAN_EXPORT usize lean_compacted_region_size(usize region) {
+    return reinterpret_cast<compacted_region *>(region)->size();
+}
+
 extern "C" LEAN_EXPORT obj_res lean_compacted_region_free(usize region, object *) {
     delete reinterpret_cast<compacted_region *>(region);
     return lean_io_result_mk_ok(lean_box(0));
diff --git a/src/runtime/compact.h b/src/runtime/compact.h
index 911e2670a2..4284d3b48e 100644
--- a/src/runtime/compact.h
+++ b/src/runtime/compact.h
@@ -57,6 +57,7 @@ public:
 };
 
 class LEAN_EXPORT compacted_region {
+    size_t m_size;
     // see `object_compactor::m_base_addr`
     void * m_base_addr;
     bool m_is_mmap;
@@ -88,5 +89,6 @@ public:
     compacted_region operator=(compacted_region &&) = delete;
     object * read();
     bool is_memory_mapped() const { return m_is_mmap; }
+    size_t size() const { return m_size; }
 };
 }
diff --git a/tests/bench/accumulate_profile.py b/tests/bench/accumulate_profile.py
index a018f83d0f..1a21ff947d 100755
--- a/tests/bench/accumulate_profile.py
+++ b/tests/bench/accumulate_profile.py
@@ -6,7 +6,8 @@ import sys
 
 cats = collections.defaultdict(lambda: 0)
 for line in sys.stdin:
-    if m := re.match("(.+?) ([\d.]+)(m?)s", line):
+    if m := re.match(r"(.+?) ([\d.]+)(m?)s", line) or \
+            re.match(r"\s*(number of imported bytes|number of imported consts|number of imported entries):\s+(\d+)()", line):
         cats[m[1].strip()] += float(m[2]) * (1e-3 if m[3] else 1)
     sys.stderr.write(line)
 
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
index 11db80fa7b..3d5e3b4780 100644
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -18,7 +18,7 @@
   run_config:
     <<: *time
     cmd: |
-      bash -c 'set -eo pipefail; touch ../../src/Init/Prelude.lean; make LEAN_OPTS="-Dprofiler=true -Dprofiler.threshold=9999" -C ${BUILD:-../../build/release}/stage2 --output-sync -j$(nproc) 2>&1 | ./accumulate_profile.py'
+      bash -c 'set -eo pipefail; touch ../../src/Init/Prelude.lean; make LEAN_OPTS="-Dprofiler=true -Dprofiler.threshold=99999 --stats" -C ${BUILD:-../../build/release}/stage2 --output-sync -j$(nproc) 2>&1 | ./accumulate_profile.py'
     max_runs: 2
     parse_output: true
   # initialize stage2 cmake + warmup