chore: lean --stats gives number of imported bytes

Author: Kha

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);

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));

src/runtime/compact.h

@@ -57,6 +57,7 @@ class LEAN_EXPORT object_compactor {
 };
 
 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 @@ class LEAN_EXPORT compacted_region {
     compacted_region operator=(compacted_region &&) = delete;
     object * read();
     bool is_memory_mapped() const { return m_is_mmap; }
+    size_t size() const { return m_size; }
 };
 }

tests/bench/accumulate_profile.py

@@ -6,7 +6,8 @@
 
 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)
 

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